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.right.introx:ℝ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 < x✝hx:x✝ < ?epsx:ℝ⊢ deriv sin x = cos x
    apply HasDerivAt.derivh.hx✝:ℝhpos:0 < x✝hx: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 Real.sin = Real.cos := funext fun x => HasDerivAt.deriv (Real.hasDerivAt_sin x)⊢ ContinuousOn sin (Set.Icc 0 x) fun_propAll goals completed! 🐙) (byx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := funext fun x => HasDerivAt.deriv (Real.hasDerivAt_sin x)⊢ DifferentiableOn ℝ sin (Set.Ioo 0 x) fun_propAll goals completed! 🐙)
  simp [hderiv] at thish.right.introx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478this:∃ c, (0 < c ∧ c < x) ∧ cos c = sin x / x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ
  obtain ⟨ y, ⟨ hy1, hy2 ⟩, hy3 ⟩ := thish.right.intro.intro.intro.introx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ sin x > x / 2h.left⊢ ?eps > 0eps⊢ ℝ
  suffices hcosy : cos y > 1/2h.right.intro.intro.intro.introx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xhcosy:cos y > 1 / 2⊢ sin x > x / 2hcosyx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ cos y > 1 / 2h.left⊢ ?eps > 0eps⊢ ℝ
  .h.right.intro.intro.intro.introx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝ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_left hpos)] at hcosyh.right.intro.intro.intro.introx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝ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.right.intro.intro.intro.introx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝ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 Real.sin = Real.cos := ?_mvar.3478y:ℝ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 Real.sin = Real.cos := ?_mvar.3478y:ℝ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 Real.sin = Real.cos := ?_mvar.3478y:ℝ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 Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:y < π / 3⊢ cos y > 1 / 2yboundx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < x⊢ y < π / 3h.left⊢ ?eps > 0eps⊢ ℝ
  .hcosyx:ℝhpos:0 < xhx:x < ?epshderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝ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 Real.sin = Real.cos := funext fun x => HasDerivAt.deriv (Real.hasDerivAt_sin x)y:ℝ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 Real.sin = Real.cos := ?_mvar.3478y:ℝ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 Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xthis:_fvar.9778 < ?_mvar.2936 := ?_mvar.15012⊢ y < π / 3h.left⊢ ?eps > 0  -- Now it is time to pick ε
  .eps⊢ ℝ exact π/3All goals completed! 🐙
  .yboundx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.3478y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xthis:_fvar.9778 < ?_mvar.2936 := ?_mvar.15012⊢ 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 < x✝hx:x✝ < π / 3x:ℝ⊢ deriv sin x = cos x
    apply HasDerivAt.derivh.hx✝:ℝhpos:0 < x✝hx: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 Real.sin = Real.cos := funext fun x => HasDerivAt.deriv (Real.hasDerivAt_sin x)⊢ ContinuousOn sin (Set.Icc 0 x) fun_propAll goals completed! 🐙) (byx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := funext fun x => HasDerivAt.deriv (Real.hasDerivAt_sin x)⊢ DifferentiableOn ℝ sin (Set.Ioo 0 x) fun_propAll goals completed! 🐙)
  simp [hderiv] at thisrightx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149this:∃ c, (0 < c ∧ c < x) ∧ cos c = sin x / x⊢ sin x > x / 2
  obtain ⟨ y, ⟨ hy1, hy2 ⟩, hy3 ⟩ := thisright.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝ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 Real.sin = Real.cos := funext fun x => HasDerivAt.deriv (Real.hasDerivAt_sin x)y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := 
  lt_of_not_ge fun a =>
    Mathlib.Tactic.Linarith.lt_irrefl
      (Eq.mp
        (congrArg (fun _a => _a < 0)
          (Mathlib.Tactic.Ring.of_eq
            (Mathlib.Tactic.Ring.add_congr
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.mul_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
                    (Mathlib.Tactic.Ring.atom_pf _fvar.16622)
                    (Mathlib.Tactic.Ring.add_mul
                      (Mathlib.Tactic.Ring.mul_add
                        (Mathlib.Tactic.Ring.mul_pf_right _fvar.16622 (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3)))
                        (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.16622 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0)))
                      (Mathlib.Tactic.Ring.zero_mul (_fvar.16622 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                      (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.16622 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0))))
                  (Mathlib.Tactic.Ring.mul_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                    (Mathlib.Tactic.Ring.atom_pf Real.pi)
                    (Mathlib.Tactic.Ring.add_mul
                      (Mathlib.Tactic.Ring.mul_add
                        (Mathlib.Tactic.Ring.mul_pf_right Real.pi (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                        (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
                      (Mathlib.Tactic.Ring.zero_mul (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                      (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul Real.pi (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.16622 ^ Nat.rawCast 1 * Nat.rawCast 3)
                      (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.mul_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
                  (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.23449)
                    (Mathlib.Tactic.Ring.atom_pf _fvar.16622)
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_mul _fvar.16622 (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.neg_one_mul
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                (Eq.refl (Int.negOfNat 1))))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.16622 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_mul
                    (Mathlib.Tactic.Ring.mul_add
                      (Mathlib.Tactic.Ring.mul_pf_right _fvar.16622 (Nat.rawCast 1)
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 3)))))
                      (Mathlib.Tactic.Ring.mul_add
                        (Mathlib.Tactic.Ring.mul_pf_right _fvar.23449 (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3)))
                        (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0)))
                      (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.16622 ^ Nat.rawCast 1 * (Int.negOfNat 3).rawCast)
                        (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0))))
                    (Mathlib.Tactic.Ring.zero_mul
                      (_fvar.16622 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast +
                        (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
                    (Mathlib.Tactic.Ring.add_pf_add_zero
                      (_fvar.16622 ^ Nat.rawCast 1 * (Int.negOfNat 3).rawCast +
                        (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.16622 (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0)))))
              (Mathlib.Tactic.Ring.sub_congr
                (Mathlib.Tactic.Ring.mul_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                  (Mathlib.Tactic.Ring.atom_pf Real.pi)
                  (Mathlib.Tactic.Ring.add_mul
                    (Mathlib.Tactic.Ring.mul_add
                      (Mathlib.Tactic.Ring.mul_pf_right Real.pi (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                      (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
                      (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
                    (Mathlib.Tactic.Ring.zero_mul (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                    (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.mul_congr
                  (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
                  (Mathlib.Tactic.Ring.atom_pf _fvar.23449)
                  (Mathlib.Tactic.Ring.add_mul
                    (Mathlib.Tactic.Ring.mul_add
                      (Mathlib.Tactic.Ring.mul_pf_right _fvar.23449 (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3)))
                      (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3))
                      (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0)))
                    (Mathlib.Tactic.Ring.zero_mul (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
                    (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.23449 ^ Nat.rawCast 1 * Nat.rawCast 3 + 0))))
                (Mathlib.Tactic.Ring.sub_pf
                  (Mathlib.Tactic.Ring.neg_add
                    (Mathlib.Tactic.Ring.neg_mul _fvar.23449 (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
                            (Eq.refl (Int.negOfNat 3))))))
                    Mathlib.Tactic.Ring.neg_zero)
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1)
                    (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.23449 ^ Nat.rawCast 1 * (Int.negOfNat 3).rawCast + 0)))))
              (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                (Mathlib.Tactic.Ring.add_overlap_pf_zero Real.pi (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                      (Eq.refl (Int.ofNat 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.23449 (Nat.rawCast 1)
                    (Mathlib.Meta.NormNum.IsInt.to_isNat
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 0)))))
                  (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))))
        (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
          (Mathlib.Tactic.Linarith.add_neg
            (Eq.mp
              (congrArg (fun _a => _a < 0)
                (CancelDenoms.sub_subst rfl
                  (CancelDenoms.div_subst rfl
                    (Mathlib.Meta.NormNum.isNat_eq_true
                      (Mathlib.Meta.NormNum.IsNNRat.to_isNat
                        (Mathlib.Meta.NormNum.isNNRat_div
                          (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                            (Mathlib.Meta.NormNum.IsNNRat.to_isNat
                              (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
                                (Mathlib.Meta.NormNum.isNNRat_inv_pos
                                  (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                                    (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))))
                                (Eq.refl (Nat.mul 3 1)) (Eq.refl 3))))))
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                    (Mathlib.Meta.NormNum.isNat_eq_true
                      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
                        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))
                        (Eq.refl 3))
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))))))
              (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.16650)
                (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
                  (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))))
            (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt _fvar.23490)
              (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
                (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))))
          (Eq.mp
            (congrArg (fun _a => _a ≤ 0)
              (CancelDenoms.sub_subst
                (CancelDenoms.div_subst rfl
                  (Mathlib.Meta.NormNum.isNat_eq_true
                    (Mathlib.Meta.NormNum.IsNNRat.to_isNat
                      (Mathlib.Meta.NormNum.isNNRat_div
                        (Mathlib.Meta.NormNum.IsNat.to_isNNRat
                          (Mathlib.Meta.NormNum.IsNNRat.to_isNat
                            (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)))
                              (Mathlib.Meta.NormNum.isNNRat_inv_pos
                                (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))))
                              (Eq.refl (Nat.mul 3 1)) (Eq.refl 3))))))
                    (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                  (Mathlib.Meta.NormNum.isNat_eq_true
                    (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl 3))
                    (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))))
                rfl))
            (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)
              (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
                (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))))))⊢ π / 3 ≤ π linarithAll goals completed! 🐙) ybound
  simp only [cos_pi_div_three, ←gt_iff_lt] at hcosyright.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := ?_mvar.23598hcosy:cos y > 1 / 2⊢ sin x > x / 2
  rw [hy3, gt_iff_lt, ←(mul_lt_mul_left hpos)] at hcosyright.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := ?_mvar.23598hcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x > x / 2
  rw [gt_iff_lt]right.intro.intro.introx:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := ?_mvar.23598hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 < sin x
  convert hcosy using 1h.e'_3x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := ?_mvar.23598hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2)h.e'_4x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := ?_mvar.23598hcosy:x * (1 / 2) < x * (sin x / x)⊢ sin x = x * (sin x / x)
  .h.e'_3x:ℝhpos:0 < xhx:x < π / 3hderiv:deriv Real.sin = Real.cos := ?_mvar.17149y:ℝhy3:cos y = sin x / xhy1:0 < yhy2:y < xybound:_fvar.23449 < Real.pi / 3 := ?_mvar.23598hcosy:x * (1 / 2) < x * (sin x / x)⊢ x / 2 = x * (1 / 2) ringAll goals completed! 🐙
  field_simpAll goals completed! 🐙