/-
  # Introduction to Lean: Formalizing Mathematics with Mathlib
  Summer school "Proof assistants and applications"
  IRMA, Université de Strasbourg, August 31 – September 4, 2026
  Xavier Roblot (Université Claude Bernard Lyon I)

  ## Part 2 — Algebraic structures, analysis and topology — SOLUTIONS

  (This file mirrors `Part2.lean`: one solution per `sorry`
   exercise, in the same order and the same sections.)
-/
import Mathlib.Analysis.Calculus.FDeriv.Defs
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

noncomputable section

/- # Types, coercions and subtypes -/

-- Casts commute with multiplication
example (n m : ℕ) : ((n * m : ℕ) : ℝ) = (n : ℝ) * (m : ℝ) := by
  push_cast
  ring

-- With a hypothesis, subtraction survives the cast
-- (`Nat.cast_sub h` also does it in one rewrite)
example (n : ℕ) (h : 5 ≤ n) : ((n - 5 : ℕ) : ℤ) = (n : ℤ) - 5 := by
  push_cast [h]
  ring

-- A function cannot distinguish two proofs of the same proposition:
-- by proof irrelevance the two arguments are definitionally equal
example (p : Prop) (f : p → ℕ) (h₁ h₂ : p) : f h₁ = f h₂ := by rfl

/- # Algebraic structures -/

/- ## Groups -/

-- Trivial kernel if injective
example {G H : Type*} [Group G] [Group H] (f : G →* H)
    (hf : Function.Injective f) (a : G) (h : f a = 1) : a = 1 := by
  apply hf
  rw [h, map_one f]

-- (ab)^n = a^n * b^n in a commutative monoid
-- The converse: a morphism with trivial kernel is injective
example {G H : Type*} [Group G] [Group H] (f : G →* H)
    (h : ∀ a : G, f a = 1 → a = 1) : Function.Injective f := by
  intro a b hab
  have key : f (a * b⁻¹) = 1 := by rw [map_mul, map_inv, hab, mul_inv_cancel]
  have h2 := h _ key
  rw [mul_inv_eq_one] at h2
  exact h2

example {M : Type*} [CommMonoid M] (a b : M) (n : ℕ) :
    (a * b) ^ n = a ^ n * b ^ n := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ (a * b), ih, pow_succ a, pow_succ b]
    exact mul_mul_mul_comm (a ^ n) (b ^ n) a b

-- The preimage of a subgroup preserves inclusion
example {G H : Type*} [Group G] [Group H] (φ : G →* H)
    (S T : Subgroup H) (hST : S ≤ T) : S.comap φ ≤ T.comap φ := by
  intro x hx
  rw [Subgroup.mem_comap] at hx ⊢
  exact hST hx

/- ## Rings and fields -/

-- Factorization of a³ - b³
example {R : Type*} [CommRing R] (a b : R) :
    a ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2) := by ring

-- Cancellation in a field
theorem cancel_left {K : Type*} [Field K] {a b c : K} (ha : a ≠ 0)
    (h : a * b = a * c) : b = c := by
  have key : a⁻¹ * (a * b) = a⁻¹ * (a * c) := congr_arg (a⁻¹ * ·) h
  rw [← mul_assoc, ← mul_assoc, inv_mul_cancel₀ ha, one_mul,
    one_mul] at key
  exact key

-- (a⁻¹)⁻¹ = a for a ≠ 0
example {K : Type*} [Field K] (a : K) (ha : a ≠ 0) : (a⁻¹)⁻¹ = a := by
  apply cancel_left (inv_ne_zero ha)
  rw [mul_inv_cancel₀ (inv_ne_zero ha), inv_mul_cancel₀ ha]

-- Cancellation by a unit, in any monoid
example {M : Type*} [Monoid M] {a c d : M} (ha : IsUnit a)
    (h : a * c = a * d) : c = d := by
  obtain ⟨u, rfl⟩ := ha
  have key := congr_arg ((↑u⁻¹ : M) * ·) h
  rw [← mul_assoc, ← mul_assoc, Units.inv_mul, one_mul, one_mul] at key
  exact key

/- # Analysis and topology -/

/- ## Continuity -/

example : Continuous (fun x : ℝ ↦ Real.cos x + x ^ 2) :=
  Continuous.add Real.continuous_cos (continuous_pow 2)

example {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
    Continuous (fun x ↦ f x * g x) :=
  Continuous.mul hf hg

example : Continuous (Real.sin ∘ Real.exp) := by
  exact Continuous.comp Real.continuous_sin Real.continuous_exp

/- ## Derivatives -/

-- A sum of differentiable functions is differentiable
-- (`fun_prop` also works)
example : Differentiable ℝ (fun x : ℝ ↦ x ^ 3 + x) :=
  Differentiable.add (differentiable_pow 3) differentiable_id

example : deriv (fun x : ℝ ↦ x ^ 2) = fun x ↦ 2 * x := by
  ext x
  simp

/- ## Automating it: fun_prop -/

example : ContinuousAt (fun x : ℝ ↦ Real.exp x * (1 + x ^ 2)) 0 := by fun_prop

-- fun_prop cannot prove `1 + Real.exp x ≠ 0`, so we supply it
example : Continuous (fun x : ℝ ↦ 1 / (1 + Real.exp x)) := by
  apply Continuous.div₀
  · fun_prop
  · fun_prop
  · intro x
    positivity

/- ## Topology -/

example {f : ℝ → ℝ} (hf : Continuous f) {s : Set ℝ}
    (hs : IsClosed s) : IsClosed (f ⁻¹' s) :=
  IsClosed.preimage hf hs

example {f : ℝ → ℝ} (hf : Continuous f) {s : Set ℝ}
    (hs : IsCompact s) : IsCompact (f '' s) :=
  IsCompact.image hs hf

-- A continuous function that changes sign on [0, 1] has a zero there
example (f : ℝ → ℝ) (hf : Continuous f) (h0 : f 0 < 0)
    (h1 : 0 < f 1) : ∃ x ∈ Set.Icc (0 : ℝ) 1, f x = 0 := by
  -- the IVT: [f 0, f 1] is contained in the image of [0, 1]
  have hsub := intermediate_value_Icc (by norm_num : (0 : ℝ) ≤ 1)
    (Continuous.continuousOn hf)
  -- 0 lies in [f 0, f 1] since f 0 < 0 < f 1
  have h0mem : (0 : ℝ) ∈ Set.Icc (f 0) (f 1) :=
    ⟨le_of_lt h0, le_of_lt h1⟩
  -- so 0 is in the image: extract a preimage point
  obtain ⟨x, hx, hfx⟩ := hsub h0mem
  exact ⟨x, hx, hfx⟩