Analysis
A.6. Some examples of proofs and quantifiers

Imports

import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Analysis I, Appendix A.6: Some examples of proofs and quantifiers

Some examples of proofs and quantifiers in Lean

              /-- Proposition A.6.1 -/
example : ∀ ε > (0:ℝ), ∃ δ > 0, 2 * δ < ε := by⊢ ∀ ε > 0, ∃ δ > 0, 2 * δ < ε
  intro ε hεε:ℝhε:ε > 0⊢ ∃ δ > 0, 2 * δ < ε
  use ε / 3hε:ℝhε:ε > 0⊢ ε / 3 > 0 ∧ 2 * (ε / 3) < ε
  constructorh.leftε:ℝhε:ε > 0⊢ ε / 3 > 0h.rightε:ℝhε:ε > 0⊢ 2 * (ε / 3) < ε
  .h.leftε:ℝhε:ε > 0⊢ ε / 3 > 0 positivityAll goals completed! 🐙
  .h.rightε:ℝhε:ε > 0⊢ 2 * (ε / 3) < ε linarithAll goals completed! 🐙declaration uses `sorry`example : ¬ ∃ δ > 0, ∀ ε > (0:ℝ), 2 * δ < ε := by⊢ ¬∃ δ > 0, ∀ ε > 0, 2 * δ < ε
  sorryAll goals completed! 🐙open Real in
/-- Proposition A.6.2.  The proof below is somewhat non-idiomatic for Lean, but illustrates how to implement a "let ε be a quantity to be chosen later" type of proof. -/
example : ∃ ε > 0, ∀ x, 0 < x ∧ x < ε → sin x > x / 2 := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2
  use ?epsh⊢ ?eps > 0 ∧ ∀ (x : ℝ), 0 < x ∧ x < ?eps → sin x > x / 2eps⊢ ℝ  -- we will choose this later
  constructorh.left⊢ ?eps > 0h.right⊢ ∀ (x : ℝ), 0 < x ∧ x < ?eps → sin x > x / 2eps⊢ ℝ
  swaph.right⊢ ∀ (x : ℝ), 0 < x ∧ x < ?eps → sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ -- defer the checking of positivity until later
  rintro x ⟨hpos, hx⟩h.rightx:ℝhpos:0 < xhx:x < ?eps⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ
  have hderiv : deriv sin = cos := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2
    ext xhx✝:ℝhpos:0 < xhx:x < ?epsx:ℝ⊢ deriv sin x = cos x
    apply HasDerivAt.derivh.hx✝:ℝhpos:0 < xhx:x < ?epsx:ℝ⊢ HasDerivAt sin (cos x) x
    apply hasDerivAt_sinAll goals completed! 🐙
  have := exists_deriv_eq_slope sin hpos (byx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cos⊢ ContinuousOn sin (Set.Icc 0 x) fun_propAll goals completed! 🐙) (byx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cos⊢ DifferentiableOn ℝ sin (Set.Ioo 0 x) fun_propAll goals completed! 🐙)
  simp [hderiv] at thish.rightx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = costhis:∃ c, (0 < c ∧ c < x) ∧ cos c = sin x / x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ
  obtain ⟨ y, ⟨ hy1, hy2 ⟩, hy3 ⟩ := thish.rightx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ
  suffices hcosy : cos y > 1/2h.rightx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:cos y > 1 / 2⊢ sin x > x / 2hcosyx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ cos y > 1 / 2h.left⊢ ?eps > 0eps⊢ ℝ
  .h.rightx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:cos y > 1 / 2⊢ sin x > x / 2 rw [hy3, gt_iff_lt, ←(mul_lt_mul_iff_right₀ hpos)] at hcosyh.rightx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x > x / 2
    rw [gt_iff_lt]h.rightx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 < sin x
    convert hcosy using 1h.e'_3x:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2)h.e'_4x:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x = x * (sin x / x)
    .h.e'_3x:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2) ringAll goals completed! 🐙
    field_simpAll goals completed! 🐙
  suffices ybound : y < π/3hcosyx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ cos y > 1 / 2yboundx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ y < π / 3h.left⊢ ?eps > 0eps⊢ ℝ
  .hcosyx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ cos y > 1 / 2 have := cos_lt_cos_of_nonneg_of_le_pi (le_of_lt hy1) (byx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ π / 3 ≤ π linarithAll goals completed! 🐙) ybound
    simp only [cos_pi_div_three, ←gt_iff_lt] at thishcosyx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3this:cos y > 1 / 2⊢ cos y > 1 / 2
    exact thisAll goals completed! 🐙
  have : y < ?eps := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2
    exact hy2.trans hxAll goals completed! 🐙
  pick_goal 3eps⊢ ℝyboundx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xthis:y < ?eps⊢ y < π / 3h.left⊢ ?eps > 0  -- Now it is time to pick ε
  .eps⊢ ℝ exact π/3All goals completed! 🐙
  .yboundx:ℝhpos:0 < xhx:x < ?epshderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xthis:y < ?eps⊢ y < π / 3 exact thisAll goals completed! 🐙
  positivityAll goals completed! 🐙open Real in
/-- Proposition A.6.2: a more idiomatic proof -/
example : ∃ ε > 0, ∀ x, 0 < x ∧ x < ε → sin x > x / 2 := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2
  use π/3, by⊢ π / 3 > 0 positivityAll goals completed! 🐙
  intro x ⟨ hpos, hx ⟩rightx:ℝhpos:0 < xhx:x < π / 3⊢ sin x > x / 2
  have hderiv : deriv sin = cos := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2
    ext xhx✝:ℝhpos:0 < xhx:x < π / 3x:ℝ⊢ deriv sin x = cos x
    apply HasDerivAt.derivh.hx✝:ℝhpos:0 < xhx:x < π / 3x:ℝ⊢ HasDerivAt sin (cos x) x
    apply hasDerivAt_sinAll goals completed! 🐙
  have := exists_deriv_eq_slope sin hpos (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cos⊢ ContinuousOn sin (Set.Icc 0 x) fun_propAll goals completed! 🐙) (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cos⊢ DifferentiableOn ℝ sin (Set.Ioo 0 x) fun_propAll goals completed! 🐙)
  simp [hderiv] at thisrightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = costhis:∃ c, (0 < c ∧ c < x) ∧ cos c = sin x / x⊢ sin x > x / 2
  obtain ⟨ y, ⟨ hy1, hy2 ⟩, hy3 ⟩ := thisrightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ sin x > x / 2
  have ybound : y < π/3 := by⊢ ∃ ε > 0, ∀ (x : ℝ), 0 < x ∧ x < ε → sin x > x / 2 linarithAll goals completed! 🐙
  have hcosy := cos_lt_cos_of_nonneg_of_le_pi (le_of_lt hy1) (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ π / 3 ≤ π linarithAll goals completed! 🐙) ybound
  simp only [cos_pi_div_three, ←gt_iff_lt] at hcosyrightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:cos y > 1 / 2⊢ sin x > x / 2
  rw [hy3, gt_iff_lt, ←(mul_lt_mul_iff_right₀ hpos)] at hcosyrightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x > x / 2
  rw [gt_iff_lt]rightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 < sin x
  convert hcosy using 1h.e'_3x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2)h.e'_4x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x = x * (sin x / x)
  .h.e'_3x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv sin = cosy:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2) ringAll goals completed! 🐙
  field_simpAll goals completed! 🐙