/-
  # 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

  Types and coercions, algebraic structures, analysis and topology.

  The keyboard shortcuts, a tour of the Lean syntax and the notes on
  how to work on these files are at the top of `Part1.lean`.

  References:
  * Formalising Mathematics 2024, K. Buzzard
  * Theorem Proving in Lean 4, J. Avigad et al.
  * Mathematics in Lean, J. Avigad & P. Massot
  * M2 Lyon 2024-25, S. Morel, F. A. E. Nuccio, X. Roblot
-/
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Analysis.Calculus.FDeriv.Defs
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

noncomputable section

/-
  # Types, coercions and subtypes

  Everything in Lean has exactly one type, and Lean is strict about it.
  This section collects what surprises newcomers most: how a numeral
  gets its type, how Lean moves between `ℕ`, `ℤ` and `ℝ`, the two
  coercion arrows, and how one carries a property around with an
  element.
-/

/-
  ## Strict typing and elaboration

  A numeral such as `2` has no intrinsic type: Lean *elaborates* it,
  that is, it decides the type from the context. With no constraint
  at all, the default is `ℕ`.
-/

#check 2            -- ℕ
#check (2 : ℝ)      -- ℝ
#check (2 : ℤ)      -- ℤ

-- This matters, because ℕ-subtraction is *truncated* at zero (the
-- reason why is the section "Total functions and junk values" below).
-- The type ascription `(e : T)` is how you force a choice, and here it
-- changes the *statement*, not merely its display:
example : (2 - 5 : ℕ) = 0 := by norm_num
example : (2 - 5 : ℤ) = -3 := by norm_num

/-
  ## Coercions: the `↑` arrow

  Lean does not silently identify `ℕ` with `ℝ`. Instead it inserts a
  *coercion*, displayed `↑n` (here `Nat.cast n`). If `n : ℕ` and
  `x : ℝ`, the expression `x + n` is really `x + ↑n`.
-/

example (n : ℕ) (x : ℝ) : ℝ := x + n     -- really `x + ↑n`

-- Recall `fun x ↦ e`, the function sending `x` to `e`
#check fun (n : ℕ) ↦ (n : ℝ)            -- ℕ → ℝ, i.e. `Nat.cast`

/-
  Two tactics do the bookkeeping:
  * `push_cast` pushes coercions *towards the leaves*
    (`↑(a + b)` becomes `↑a + ↑b`);
  * `norm_cast` normalises them and tries to close the goal;
    `exact_mod_cast h` is `exact h` up to coercions.
-/

example (n m : ℕ) : ((n + m : ℕ) : ℝ) = (n : ℝ) + (m : ℝ) := by
  push_cast
  rfl

-- ⚠ Coercion does *not* commute with ℕ-subtraction without a hypothesis:
-- `↑(n - m) = ↑n - ↑m` is false in general (take n = 2, m = 5).

-- The subtraction is computed in ℕ first, and only then cast
example : ((2 - 5 : ℕ) : ℤ) = 0 := by norm_num

-- When no truncation occurs, the cast does commute with the subtraction
example : ((5 - 2 : ℕ) : ℤ) = (5 : ℤ) - 2 := by norm_num

/-
  ## Total functions and junk values

  Truncated subtraction is one case of something more general. The
  domain of a function in Lean is a **type**: `f : α → β` must produce
  an element of `β` from *every* element of `α`, since that is what its
  own type says. Nothing lets you declare a function on part of a type,
  so every function is **total**. Restricting a domain means changing
  it, to a subtype `{x : α // p x}`, and that changes the type of the
  function.

  Division has type `ℝ → ℝ → ℝ`, so `1 / 0` has to be some real number,
  and Mathlib has to pick one. The usual choices are

    x / 0 = 0        (0 : ℝ)⁻¹ = 0
    Real.sqrt (-3) = 0     Real.log 0 = 0     (2 : ℕ) - 5 = 0

  These are **junk values**. They have no mathematical meaning and no
  theorem depends on them. The alternative would be to make division a
  partial function, taking a proof of `y ≠ 0` as an argument, and then
  every statement about a quotient would have to carry that proof
  around. Mathlib chose the other way: the operations are total, and
  the hypotheses appear only in the lemmas that actually need them,
  such as `div_mul_cancel₀`, which assumes `b ≠ 0`.

  The price is that you must read statements carefully. `x / y` is not
  "the quotient of x by y" unless you know `y ≠ 0`, and a theorem
  proved about `x / y` says nothing you expect when `y = 0`.

  **An example of what this costs.** Mathlib defines the Riemann zeta
  function on all of ℂ, and it agrees with the classical one outside
  `s = 1`, where the classical function has a pole. So `riemannZeta 1`
  is some complex number, fixed by the definition rather than by
  mathematics. When the Riemann hypothesis was added to the library,

    def RiemannHypothesis : Prop :=
      ∀ (s : ℂ), riemannZeta s = 0 → (¬∃ (n : ℕ), s = -2 * (n + 1)) →
        s ≠ 1 → s.re = 1 / 2

  Kevin Buzzard pointed out that the statement would be *false*, for
  reasons having nothing to do with number theory, if that value
  happened to be `0`: `s = 1` would be a zero, it is not one of the
  trivial zeros, and its real part is not `1 / 2`. Hence the `s ≠ 1`
  in the statement, and hence the lemma `riemannZeta_one_ne_zero`,
  proved to settle the question.
-/

/-
  ## Subtypes

  Let `α` be a type and `p : α → Prop` a predicate on `α`. Then
  `{x : α // p x}` is the type of the elements of `α` satisfying `p`.
  One of its terms is a *pair*: a value and a proof.
  * `x.val` (also written `↑x`) is the underlying element;
  * `x.property` is the proof that it satisfies `p`.
-/

-- The positive naturals
#check ({ n : ℕ // 0 < n })

example (x : { n : ℕ // 0 < n }) : 0 < x.val := x.property

-- Building a term: give the value and the proof
example : { n : ℕ // 0 < n } := ⟨1, Nat.one_pos⟩

/-
  ## Proof irrelevance

  In Lean, any two proofs of the same proposition are *equal*, and
  equal by definition, so `rfl` proves it.
-/

example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := by rfl

/-
  This is exactly what makes subtypes usable: to prove that two terms
  of `{x : α // p x}` are equal, only the values matter, since the
  proof components are automatically equal. That is `Subtype.ext`.
-/

example (x y : { n : ℕ // 0 < n }) (h : x.val = y.val) : x = y :=
  Subtype.ext h

/- TODO -/

-- Casts commute with multiplication.
-- Hint: push the coercions towards the leaves, then finish with `ring`
example (n m : ℕ) : ((n * m : ℕ) : ℝ) = (n : ℝ) * (m : ℝ) := by
  sorry

-- With an extra hypothesis, the cast commutes with subtraction.
-- Hint: ℕ-subtraction is truncated, so `h` has to be used. Like
--   `simp`, `push_cast` accepts extra facts in brackets: `push_cast [h]`
example (n : ℕ) (h : 5 ≤ n) : ((n - 5 : ℕ) : ℤ) = (n : ℤ) - 5 := by
  sorry

-- A function cannot distinguish two proofs of the same proposition.
-- Hint: no lemma needed here
example (p : Prop) (f : p → ℕ) (h₁ h₂ : p) : f h₁ = f h₂ := by
  sorry

/- END TODO -/

/-
  # Algebraic structures

  Mathlib describes algebraic structures with **type classes**. We start
  with how that machinery works: it is what makes one lemma about
  commutative multiplication apply to ℕ, to ℂ, to functions into a ring
  and to permutation groups, without anyone restating it.
-/

/-
  ## Reading a Mathlib statement

  Three kinds of brackets appear in a signature, and they decide what
  *you* must supply and what Lean works out on its own.

  | Notation        | Meaning                                          |
  |-----------------|--------------------------------------------------|
  | `(a b : G)`     | **explicit** — you write them                    |
  | `{G : Type*}`   | **implicit** — Lean infers them from the context |
  | `[CommMagma G]` | **instance** — Lean looks it up in its database  |

  Instance brackets are the mechanism behind the generality just
  described: `[Group G]` reads "G is equipped with a group structure",
  and Lean finds that structure by itself. Prefixing a name with `@`
  makes everything explicit, which is useful when Lean infers the
  wrong argument.
-/

-- The signature already shows the three kinds of brackets
#check mul_comm

-- In everyday use you only write the explicit ones
example (a b : ℤ) : a * b = b * a := mul_comm a b

-- The same proof with every argument spelled out.
-- `_` asks Lean to fill in the instance itself
example (a b : ℤ) : a * b = b * a := @mul_comm ℤ _ a b

-- Implicit arguments are recovered from the *other* arguments:
-- in `hab : f a = f b`, Lean reads off `α`, `β`, `f`, `a` and `b`
example {α β : Type} {f : α → β} (hf : Function.Injective f)
    {a b : α} (hab : f a = f b) : a = b := hf hab

/-
  ## What a type class is

  `Group G` is a *structure*, bundling the data (`*`, `1`, `⁻¹`) with
  their axioms. What makes it a **class** is that its inhabitants are
  recorded in a database Lean may consult by itself, which is why, in
  `mul_comm` above, you supply `a` and `b` and Lean supplies
  `[CommMagma G]`.

  The hierarchy is the expected one, each level extending the previous:
    Monoid → Group → CommGroup
    Ring → CommRing → Field
    AddCommGroup + scalars → Module (generalizes vector space)
  The real hierarchy is far finer: `mul_comm` above needs only
  `CommMagma`, a class that does not even appear in this sketch.

  ## Instance synthesis

  An entry is added with `instance`; finding one is **instance
  synthesis**. `#synth C α` runs that search and shows what it found.
-/

#synth CommRing ℤ                    -- Int.instCommRing
#synth Field ℝ                       -- Real.instField

/-
  Instances are not entries in a table: there are infinitely many
  types, so a table is not possible. They are **rules**, some of them with
  hypotheses: `Pi.commRing` says "if each `f i` is a commutative ring,
  so are the functions into them". Lean treats the instance it needs as
  a *goal* and chains such rules, exactly as `apply` does. The composite
  names it returns show the chain. Two mechanisms do the work.

  **Instances are inherited along the hierarchy.** A group is a monoid:
-/

#synth Monoid (Equiv.Perm (Fin 3))   -- Equiv.Perm.permGroup.toMonoid

/-
  Read the answer: Lean found `permGroup`, since permutations form a
  group, then walked down with `.toMonoid`.

  **A rule may itself require an instance.** "If `R` is a commutative
  ring, so are the functions into `R`" is such a rule, so the search
  composes:
-/

#synth CommRing (ℕ → ℝ)              -- Pi.commRing

/-
  This is what the search buys you. `mul_comm` is stated once, for any
  `[CommMagma G]`, and it applies to every type for which Lean can
  build such an instance, whether by a single rule or by a chain of
  them.
-/

example (a b : ℕ) : a * b = b * a := mul_comm a b
example (a b : ℂ) : a * b = b * a := mul_comm a b
example (f g : ℕ → ℝ) : f * g = g * f := mul_comm f g
example (a b : ZMod 7) : a * b = b * a := mul_comm a b

/-
  Hence a rule for stating your own results: assume the weakest
  structure that makes the statement true. And when something fails to
  typecheck for no visible reason, the problem often comes from
  instance search: `#synth` says whether the instance exists,
  `inferInstance` asks for it inside a term.
-/

example : Monoid ℝ := inferInstance

/-
  ## Rewriting with `rw`

  `rw [h]` rewrites with an equality `h`, from left to right. `rw [← h]`
  goes from right to left, and `rw [h1, h2]` applies both in turn.

  An equivalence works too: `rw` treats `h : p ↔ q` as a rewriting rule
  on propositions, replacing `p` by `q`. This is how most `iff` lemmas
  in Mathlib are used.

  By default `rw` acts on the goal. To act on a hypothesis instead, add
  `at`: `rw [h] at h'` rewrites inside `h'`. The goal is named `⊢`, so
  `rw [h] at h' ⊢` does both at once. Most tactics that transform
  something accept the same `at` clause.

  `rw` transforms a goal or a hypothesis. To build a *new* equality
  from an old one, two lemmas do the opposite job:
  * `congr_arg f h : f a = f b` from `h : a = b`, applying the same
    function to both sides;
  * `congr_fun h a : f a = g a` from `h : f = g`, applying both sides
    to the same argument.

  The notation `(c * ·)` used below is the function `fun x ↦ c * x`,
  the dot marking where the argument goes. And `Eq.symm h` is `h` with
  its two sides exchanged.
-/

-- Left to right, on the goal
example (a b c : ℕ) (h : a = b) : a + c = b + c := by
  rw [h]

-- Right to left
example (a b c : ℕ) (h : a = b) : b + c = a + c := by
  rw [← h]

-- On a hypothesis rather than the goal
example (a b c : ℕ) (h : a = b) (h' : a + c = 5) : b + c = 5 := by
  rw [h] at h'
  exact h'

-- With an equivalence: the goal `p` becomes `q`
example (p q : Prop) (h : p ↔ q) (hq : q) : p := by
  rw [h]
  exact hq

-- Applying a function to both sides of an equality
example (a b c : ℕ) (h : a = b) : c * a = c * b := congr_arg (c * ·) h

-- Applying both sides of an equality between functions
example (f g : ℕ → ℕ) (h : f = g) (a : ℕ) : f a = g a := congr_fun h a

/-
  ## Groups

  A group morphism `f : G →* H` satisfies `f (a * b) = f a * f b`.
  Mathlib derives the other laws from it and provides them as lemmas:
  `map_one`, `map_inv`. We nevertheless prove one of them below by
  hand, as an application of `rw`, not because it is missing.
-/

#check MonoidHom.map_one
#check MonoidHom.map_mul

-- f(1_G) = 1_H
example {G H : Type*} [Group G] [Group H] (f : G →* H) : f 1 = 1 :=
  map_one f

#check eq_inv_of_mul_eq_one_left

-- f(a⁻¹) = f(a)⁻¹
-- Idea: show f(a) * f(a⁻¹) = 1, then conclude with
--   `eq_inv_of_mul_eq_one_left`
example {G H : Type*} [Group G] [Group H] (f : G →* H) (a : G) :
    f a⁻¹ = (f a)⁻¹ := by
  apply eq_inv_of_mul_eq_one_left
  rw [← map_mul f, inv_mul_cancel, map_one f]

-- The `group` tactic proves identities valid in *any* group
-- (analogue of `ring`)
example {G : Type*} [Group G] (x y z : G) :
    x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by group

-- The `abel` tactic does the same in an abelian group
-- (written additively)
example {G : Type*} [AddCommGroup G] (x y z : G) :
    z + x + (y - z - x) = y := by abel

/- TODO -/

-- If f is injective, then: f(a) = 1 → a = 1
example {G H : Type*} [Group G] [Group H] (f : G →* H)
    (hf : Function.Injective f) (a : G) (h : f a = 1) : a = 1 := by
  sorry

-- The converse: a morphism with trivial kernel is injective
-- Idea: to compare `a` and `b`, apply the hypothesis to `a * b⁻¹`.
-- Hint: `map_mul` and `map_inv` compute `f (a * b⁻¹)`
-- Secondary hint: `mul_inv_eq_one : a * b⁻¹ = 1 ↔ a = b`, which `rw`
--   can use like any equality
example {G H : Type*} [Group G] [Group H] (f : G →* H)
    (h : ∀ a : G, f a = 1 → a = 1) : Function.Injective f := by
  sorry

-- In a commutative monoid, (a * b) ^ n = a ^ n * b ^ n
-- Hint: `pow_succ x n : x ^ (n + 1) = x ^ n * x`
--   and `mul_mul_mul_comm`
--
-- `simp` simplifies the goal with a database of lemmas; `simp?` shows
-- which ones it used.
--
-- Skeleton of the induction:
--   induction n with
--   | zero   => simp        -- base case: (a * b) ^ 0 = 1 = 1 * 1
--   | succ n ih => ...
example {M : Type*} [CommMonoid M] (a b : M) (n : ℕ) :
    (a * b) ^ n = a ^ n * b ^ n := by
  sorry

-- The preimage of a subgroup under a morphism preserves inclusion
-- `S.comap φ` is the preimage of S under φ (a subgroup of G)
-- Secondary hint: `Subgroup.mem_comap` : `a ∈ S.comap φ ↔ φ a ∈ S`
example {G H : Type*} [Group G] [Group H] (φ : G →* H)
    (S T : Subgroup H) (hST : S ≤ T) : S.comap φ ≤ T.comap φ := by
  sorry

/- END TODO -/

/-
  ## Rings and fields

  `Ring R` does not assume commutativity: that assumption is `CommRing`,
  and a lemma stated for `CommRing` does not apply to a ring of
  matrices. The `ring` tactic proves the identities valid in every
  commutative ring, and requires `CommRing` for the same reason.

  A ring morphism is written `f : R →+* S`, an arrow recording what is
  preserved: `map_add`, `map_mul`, `map_one`.

  `Field K` is a `CommRing` in which every nonzero element is
  invertible. Inversion being total, `0⁻¹ = 0` is the junk value seen
  above, and the lemmas about `a⁻¹` carry a hypothesis `a ≠ 0`. That is
  what the `₀` marks in `mul_inv_cancel₀`.

  Outside a field, invertibility is a property of the element. `Mˣ` is
  the type of units of a monoid `M`: a term of it bundles an element
  with an inverse and the two proofs that they cancel, and `↑u : M` is
  the underlying element. `IsUnit a` says that `a` is one of them, by
  definition `∃ u : Mˣ, ↑u = a`. So `obtain ⟨u, rfl⟩ := ha` replaces
  `a` by `↑u` everywhere and hands you `u⁻¹` to work with.
-/

-- Commutativity is an assumption, not a theorem: `Ring` ≠ `CommRing`
example {R : Type*} [CommRing R] (a b : R) :
    a * b = b * a := mul_comm a b

-- `ring` proves polynomial identities in a `CommRing`
example {R : Type*} [CommRing R] (a b : R) :
    (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by ring

-- A ring morphism preserves powers and sums
example {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (a b : R) : f (a ^ 2 + b ^ 2) = f a ^ 2 + f b ^ 2 := by
  rw [map_add, map_pow, map_pow]

-- In a field, a zero product implies a zero factor
example {K : Type*} [Field K] (a b : K) (h : a * b = 0) :
    a = 0 ∨ b = 0 :=
  Iff.mp mul_eq_zero h

/- TODO -/

-- Factorization of a³ - b³ (use `ring`)
-- The same statement is false in a noncommutative `Ring`:
-- `ring` requires `CommRing`
example {R : Type*} [CommRing R] (a b : R) :
    a ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2) := by
  sorry

-- Left cancellation in a field: a ≠ 0, a * b = a * c → b = c
-- This one is named, so that the next exercise can use it
-- Hint: `congr_arg` to multiply both sides by `a⁻¹` on the left,
--   then `mul_assoc` and `inv_mul_cancel₀`
theorem cancel_left {K : Type*} [Field K] {a b c : K} (ha : a ≠ 0)
    (h : a * b = a * c) : b = c := by
  sorry

-- The inverse of the inverse is the element itself (for a ≠ 0)
-- Use `cancel_left` above (it is `mul_left_cancel₀` in Mathlib)
-- Hint: also `inv_ne_zero`, `mul_inv_cancel₀`, `inv_mul_cancel₀`
example {K : Type*} [Field K] (a : K) (ha : a ≠ 0) : (a⁻¹)⁻¹ = a := by
  sorry

-- Cancellation by a unit, in any monoid. `cancel_left` above assumed a
-- field, but being a unit is all the proof really uses
-- Hint: `obtain ⟨u, rfl⟩ := ha`, then `congr_arg` to multiply by `↑u⁻¹`
--   on the left, and `mul_assoc`, `Units.inv_mul`
#check Units.inv_mul     -- ↑u⁻¹ * ↑u = 1
example {M : Type*} [Monoid M] {a c d : M} (ha : IsUnit a)
    (h : a * c = a * d) : c = d := by
  sorry

/- END TODO -/

/-
  # Analysis and topology

  This part of the library is organised around type classes such as
  `TopologicalSpace`, `MetricSpace` and `NormedField`, and all limiting
  behaviour is expressed with **filters**. `𝓝 x` is the filter of
  neighbourhoods of `x`, and `Filter.Tendsto f (𝓝 a) (𝓝 b)` says
  `f x → b` as `x → a`. Other filters in the same phrase give "as
  x → +∞", "as n → ∞" for a sequence, or "from the left of a": one
  notion instead of several parallel theories.

  Hence the definitions are not the usual ones. Continuity is not ε-δ,
  and compactness is not "every open cover has a finite subcover".
  Those are *theorems*, available where they make sense.
-/

/-
  ## Continuity

  `Continuous f`      : f is continuous everywhere
  `ContinuousAt f x`  : f is continuous at x
  `ContinuousOn f s`  : f is continuous on the set s

  `ContinuousAt f x` is *by definition* `Tendsto f (𝓝 x) (𝓝 (f x))`,
  that is "f x' is near f x whenever x' is near x". The familiar
  characterisations are lemmas, not definitions.
-/

#check continuous_def         -- preimages of open sets are open
#check Metric.continuous_iff  -- the ε-δ criterion, in a metric space

/-
  A continuity proof is built by combining lemmas. Mathlib provides one
  for each basic function (the identity, the constants, `x ↦ x ^ n`,
  `sin`, `exp`) and one for each construction: a sum, a product or a
  composition of continuous functions is continuous.
-/

#check continuous_id        -- the identity
#check continuous_const     -- constants
#check continuous_pow       -- x ↦ x ^ n
#check Continuous.add       -- a sum of continuous functions
#check Continuous.mul       -- a product
#check Continuous.comp      -- a composition

-- Assembled by hand: x ↦ x ^ 2 + 1 is a sum of two known pieces
example : Continuous (fun x : ℝ ↦ x ^ 2 + 1) :=
  Continuous.add (continuous_pow 2) continuous_const

-- The composition of two continuous functions is continuous.
-- ⚠ Note the order: `Continuous.comp` takes the proof for the *outer*
--   function first, so `hg` comes before `hf` for `g ∘ f`
example {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := Continuous.comp hg hf

-- `Continuous` coincides with the classical ε-δ definition
-- (in a metric space)
example {f : ℝ → ℝ} : Continuous f ↔
    ∀ x, ∀ ε > 0, ∃ δ > 0,
      ∀ x', dist x' x < δ → dist (f x') (f x) < ε :=
  Metric.continuous_iff

/- TODO -/

-- x ↦ cos x + x ^ 2 is continuous
-- Hint: `Real.continuous_cos`, and a sum of continuous functions
example : Continuous (fun x : ℝ ↦ Real.cos x + x ^ 2) := by
  sorry

-- If f and g are continuous, x ↦ f x * g x is continuous
example {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
    Continuous (fun x ↦ f x * g x) := by
  sorry

-- sin ∘ exp is continuous
example : Continuous (Real.sin ∘ Real.exp) := by
  sorry

/- END TODO -/

/-
  ## Derivatives

  `HasDerivAt f f' x`   : f is differentiable at x, with derivative f'
  `deriv f x`           : the derivative of f at x
  `Differentiable ℝ f`  : f is differentiable everywhere

  **Why two notions?** `deriv` is a function, so it can be written down
  and manipulated: `deriv Real.sin = Real.cos` below is an equality
  between functions, and an integrand can be `deriv f`. `HasDerivAt`
  only states a relation, it never gives an object.

  But `deriv f x` must return a real number even where `f` has no
  derivative, and there it returns the junk value `0`. So as a
  hypothesis it says little: assume `HasDerivAt f c x`, which gives the
  differentiability along with the value. `HasDerivAt.deriv` below
  converts one into the other.
-/

#check deriv_zero_of_not_differentiableAt  -- ¬DifferentiableAt → deriv = 0
#check HasDerivAt.deriv                    -- HasDerivAt f c x → deriv f x = c

-- Derivatives of the usual functions. Mathlib states them as equalities
-- of functions, so the lemma is the statement:
example : deriv Real.sin = Real.cos := Real.deriv_sin

example : deriv Real.exp = Real.exp := Real.deriv_exp

-- `simp` can also compute the derivative of simple functions
-- at a point
example : deriv (fun x : ℝ ↦ x ^ 5) 6 = 5 * 6 ^ 4 := by simp

-- Two theorems of differential calculus
#check exists_deriv_eq_zero        -- Rolle's theorem
#check exists_hasDerivAt_eq_slope  -- Mean value theorem

/- TODO -/

-- x ↦ x ^ 3 + x is differentiable
-- Hint: `differentiable_pow` and `differentiable_id` for the two
--   pieces; the lemma that combines them is named as in the
--   continuity section
example : Differentiable ℝ (fun x : ℝ ↦ x ^ 3 + x) := by
  sorry

-- The derivative of x ↦ x ^ 2 is x ↦ 2 * x
-- Here no ready-made lemma applies, so the equality of functions has to
-- be proved pointwise: two functions are equal when they agree at every
-- point. Hint: start with `ext x` (as in Part 1, but on functions
--   rather than sets).
example : deriv (fun x : ℝ ↦ x ^ 2) = fun x ↦ 2 * x := by
  sorry

/- END TODO -/

/-
  ## Automating it: the `fun_prop` tactic

  Those proofs were all assembled the same way: recognise the basic
  functions, apply the lemma for each construction. `fun_prop` does that
  for you: continuity, differentiability, and likewise measurability
  and integrability. It stops as soon as the function is not built from
  things it knows, or as soon as a lemma it needs has a side condition
  it cannot discharge. Read its message: it names the assumption that
  stopped it.
-/

example : Continuous (fun x : ℝ ↦ x ^ 2 + 1) := by fun_prop
example : Continuous (fun x : ℝ ↦ Real.sin (Real.exp x)) := by fun_prop

example : Differentiable ℝ
    (fun x : ℝ ↦ Real.cos (Real.sin x) * Real.exp x) := by fun_prop

-- Where it stops. The statement is true, since `1 + exp x > 0`, but
-- `Continuous.div₀` needs the denominator to be nonzero and `fun_prop`
-- has no way to prove it. Uncomment to read the message:

#check Continuous.div₀
-- example : Continuous (fun x : ℝ ↦ 1 / (1 + Real.exp x)) := by fun_prop

/- TODO -/

-- Continuity at a single point
-- Hint: `fun_prop` also proves `ContinuousAt` goals
example : ContinuousAt (fun x : ℝ ↦ Real.exp x * (1 + x ^ 2)) 0 := by
  sorry

-- The example above that `fun_prop` could not finish. Supply the
-- missing fact by hand.
-- Hint: start with `apply Continuous.div₀`, which leaves three goals.
--   The last one is closed by `intro x` and `positivity`, a tactic
--   proving goals of the form `0 < e`, `0 ≤ e` and `e ≠ 0` from the
--   shape of `e`.
example : Continuous (fun x : ℝ ↦ 1 / (1 + Real.exp x)) := by
  sorry

/- END TODO -/

/-
  ## Topology

  `IsOpen s`    : s is open
  `IsClosed s`  : s is closed
  `IsCompact s` : s is compact

  `IsCompact s` is defined with filters: every nontrivial filter
  containing `s` has a cluster point in `s`. The familiar
  characterisation by open covers is a lemma:
-/

#check isCompact_iff_finite_subcover

-- Examples of open and closed sets
example : IsOpen (Set.Ioo (0 : ℝ) 1) := isOpen_Ioo
example : IsClosed (Set.Icc (0 : ℝ) 1) := isClosed_Icc

-- Compactness of a segment: Heine-Borel is available as a lemma
example : IsCompact (Set.Icc (0 : ℝ) 1) := isCompact_Icc

-- The preimage of an open set under a continuous function is open
example {f : ℝ → ℝ} (hf : Continuous f) {s : Set ℝ} (hs : IsOpen s) :
    IsOpen (f ⁻¹' s) := IsOpen.preimage hf hs

-- Intermediate value theorem, used in the last exercise below
#check intermediate_value_Icc

/- TODO -/

-- The preimage of a closed set under a continuous function is closed
example {f : ℝ → ℝ} (hf : Continuous f) {s : Set ℝ}
    (hs : IsClosed s) : IsClosed (f ⁻¹' s) := by
  sorry

-- The image of a compact set under a continuous function is compact
example {f : ℝ → ℝ} (hf : Continuous f) {s : Set ℝ}
    (hs : IsCompact s) : IsCompact (f '' s) := by
  sorry

-- A continuous function that changes sign on [0, 1] has a zero there
-- (a longer proof, in several steps)
-- Hint: use the intermediate value theorem (cf. the `#check` above)
--   to place `0` in the image of `Set.Icc 0 1`.
-- Secondary hints, if you get stuck: `Continuous.continuousOn` turns
--   `hf` into the hypothesis the theorem wants; membership in a
--   `Set.Icc` is a conjunction (use `constructor`).
example (f : ℝ → ℝ) (hf : Continuous f) (h0 : f 0 < 0)
    (h1 : 0 < f 1) : ∃ x ∈ Set.Icc (0 : ℝ) 1, f x = 0 := by
  sorry

/- END TODO -/

-- Extreme value theorem: a continuous function on a nonempty
-- compact attains its minimum
#check IsCompact.exists_isMinOn

-- Heine-Cantor: continuous on a compact → uniformly continuous
#check IsCompact.uniformContinuousOn_of_continuous

-- Heine-Borel: compact ↔ closed and bounded (in ℝⁿ)
#check Metric.isCompact_iff_isClosed_bounded