Analysis I, Appendix A.2: Implication

An introduction to implications. Showcases some basic tactics and Lean syntax.

example {X Y: Prop} (hX: X) : (X → Y) ↔ Y := X:PropY:ProphX:X⊢ X → Y ↔ Y All goals completed! 🐙example {X Y: Prop} (hX: ¬X) : X → Y := X:PropY:ProphX:¬X⊢ X → Y X:PropY:ProphX:¬XhX':X⊢ Y All goals completed! 🐙example {X Y: Prop} (hXY: X → Y) (hX: X) : Y := X:PropY:ProphXY:X → YhX:X⊢ Y All goals completed! 🐙example {X Y: Prop} (hXY: X → Y) (hX: X) : Y := hXY hXexample {X Y: Prop} (hXY: X → Y) (hY: ¬ Y) : ¬ X := X:PropY:ProphXY:X → YhY:¬Y⊢ ¬X X:PropY:ProphXY:X → YhY:X⊢ Y All goals completed! 🐙theorem example_A_2_1 (x:ℤ) : x = 2 → x^2 = 4 := x:ℤ⊢ x = 2 → x ^ 2 = 4 x:ℤh:x = 2⊢ x ^ 2 = 4 x:ℤh:x = 2⊢ 2 ^ 2 = 4 All goals completed! 🐙example : (2:ℤ) = 2 → (2:ℤ)^2 = 4 := example_A_2_1 2example : (3:ℤ) = 2 → (3:ℤ)^2 = 4 := example_A_2_1 3example : (-2:ℤ) = 2 → (-2:ℤ)^2 = 4 := example_A_2_1 (-2)
_root_.not_imp {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b
example : ¬ ((2+2=4) → (4+4)=2) := ⊢ ¬(2 + 2 = 4 → 4 + 4 = 2) ⊢ 2 + 2 = 4 ∧ ¬4 + 4 = 2 ⊢ 2 + 2 = 4⊢ ¬4 + 4 = 2 ⊢ 2 + 2 = 4 All goals completed! 🐙 All goals completed! 🐙example {X Y: Prop} : (X → Y) ↔ (Y ≥ X) := X:PropY:Prop⊢ X → Y ↔ Y ≥ X All goals completed! 🐙example {X Y: Prop} : (X → Y) ↔ ((¬X) ≥ ¬Y) := X:PropY:Prop⊢ X → Y ↔ (¬X) ≥ ¬Y X:PropY:Prop⊢ X → Y ↔ ¬Y → ¬X; All goals completed! 🐙example {John_left_at_five John_here_now:Prop} (h1: John_left_at_five → John_here_now) (h2: ¬ John_here_now) : ¬ John_left_at_five := John_left_at_five:PropJohn_here_now:Proph1:John_left_at_five → John_here_nowh2:¬John_here_now⊢ ¬John_left_at_five John_left_at_five:PropJohn_here_now:Proph1:John_left_at_five → John_here_nowh2:John_left_at_five⊢ John_here_now All goals completed! 🐙example {Washington_capital_US:Prop} (h: Washington_capital_US) : (1+1=2) → Washington_capital_US := Washington_capital_US:Proph:Washington_capital_US⊢ 1 + 1 = 2 → Washington_capital_US Washington_capital_US:Proph:Washington_capital_USh':1 + 1 = 2⊢ Washington_capital_US All goals completed! 🐙example {NYC_capital_US:Prop} : (2+2=3) → NYC_capital_US := NYC_capital_US:Prop⊢ 2 + 2 = 3 → NYC_capital_US NYC_capital_US:Proph:2 + 2 = 3⊢ NYC_capital_US All goals completed! 🐙

Proposition A.2.2

example : ((2+2:ℤ)=5) → (4=(10-4:ℤ)) := ⊢ 2 + 2 = 5 → 4 = 10 - 4 h:2 + 2 = 5⊢ 4 = 10 - 4 have : (4 + 4:ℤ) = 10 := ⊢ 2 + 2 = 5 → 4 = 10 - 4 h:2 * (2 + 2) = 2 * 5 := id (congrArg (HMul.hMul 2) _fvar.8078)⊢ 4 + 4 = 10 All goals completed! 🐙 rwa [←eq_sub_iff_add_eqh:2 + 2 = 5this:4 = 10 - 4⊢ 4 = 10 - 4 at this

Theorem A.2.4

theorem theorem_A_2_4 (n:ℤ) : Even (n * (n+1)) := n:ℤ⊢ Even (n * (n + 1)) n:ℤthis:Even n ∨ Odd n := Int.even_or_odd n⊢ Even (n * (n + 1)) n:ℤheven:Even n⊢ Even (n * (n + 1))n:ℤhodd:Odd n⊢ Even (n * (n + 1)) -- can also use `rcases this with heven | hodd` n:ℤheven:Even n⊢ Even (n * (n + 1)) All goals completed! 🐙 n:ℤhodd:Odd nthis:Even (n + 1) := Odd.add_one hodd⊢ Even (n * (n + 1)) All goals completed! 🐙

Corollary A.2.5

example : let n:ℤ := (253+142)*123-(423+198)^342+538-213 Even (n * (n+1)) := theorem_A_2_4 _
example : ∀ x:ℝ, x = 2 → x^2 = 4 := ⊢ ∀ (x : ℝ), x = 2 → x ^ 2 = 4 intro x x:ℝh:x = 2⊢ x ^ 2 = 4 x:ℝh:x = 2⊢ 2 ^ 2 = 4 All goals completed! 🐙example : ¬ ∀ x:ℝ, x^2 = 4 → x = 2 := ⊢ ¬∀ (x : ℝ), x ^ 2 = 4 → x = 2 ⊢ ∃ x, x ^ 2 = 4 ∧ ¬x = 2 ⊢ (-2) ^ 2 = 4 ∧ ¬-2 = 2 All goals completed! 🐙example {X Y : Prop} : (X ↔ Y) = ((X → Y) ∧ (Y → X)) := X:PropY:Prop⊢ (X ↔ Y) = ((X → Y) ∧ (Y → X)) X:PropY:Prop⊢ (X ↔ Y) ↔ (X → Y) ∧ (Y → X); All goals completed! 🐙example (x:ℝ) : x = 2 ↔ 2*x = 4 := x:ℝ⊢ x = 2 ↔ 2 * x = 4 x:ℝ⊢ x = 2 → 2 * x = 4x:ℝ⊢ 2 * x = 4 → x = 2 x:ℝ⊢ x = 2 → 2 * x = 4 x:ℝh:x = 2⊢ 2 * x = 4 All goals completed! 🐙 x:ℝh:2 * x = 4⊢ x = 2 All goals completed! 🐙example {X Y :Prop} : (X ↔ Y) = (X = Y) := X:PropY:Prop⊢ (X ↔ Y) = (X = Y) All goals completed! 🐙example : (3 = 2) → (6 = 4) := ⊢ 3 = 2 → 6 = 4 All goals completed! 🐙example : ∃ (X Y:Prop), (X → Y) ≠ (Y → X) := ⊢ ∃ X Y, (X → Y) ≠ (Y → X) x:ℤ := -2⊢ ∃ X Y, (X → Y) ≠ (Y → X) x:ℤ := -2⊢ (x = 2 → x ^ 2 = 4) ≠ (x ^ 2 = 4 → x = 2) All goals completed! 🐙theorem contrapositive {X Y: Prop} (hXY: X → Y) : ¬ Y → ¬ X := X:PropY:ProphXY:X → Y⊢ ¬Y → ¬X X:PropY:ProphXY:X → YhY:¬Y⊢ ¬X X:PropY:ProphXY:X → YhY:¬YhX:X⊢ False X:PropY:ProphXY:X → YhY:¬YhX:Xthis:Y := hXY hX⊢ False All goals completed! 🐙theorem imp_example (x:ℝ) : (x = 2) → (x^2 = 4) := x:ℝ⊢ x = 2 → x ^ 2 = 4 x:ℝh:x = 2⊢ x ^ 2 = 4 x:ℝh:x = 2⊢ 2 ^ 2 = 4 All goals completed! 🐙theorem imp_contrapositive (x:ℝ) : (x^2 ≠ 4) → (x ≠ 2) := x:ℝ⊢ x ^ 2 ≠ 4 → x ≠ 2 All goals completed! 🐙

Proposition A.2.6

example {x:ℝ} (h:x>0) (hsin: Real.sin x = 1) : x ≥ Real.pi / 2 := x:ℝh:x > 0hsin:Real.sin x = 1⊢ x ≥ Real.pi / 2 x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ False have h1 : Real.sin 0 < Real.sin x := x:ℝh:x > 0hsin:Real.sin x = 1⊢ x ≥ Real.pi / 2 x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ -(Real.pi / 2) ≤ 0x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ x ≤ Real.pi / 2 x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2⊢ -(Real.pi / 2) ≤ 0 x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2this:Real.pi > 0 := Real.pi_pos⊢ -(Real.pi / 2) ≤ 0 All goals completed! 🐙 All goals completed! 🐙 have h2 : Real.sin x < Real.sin (Real.pi / 2) := x:ℝh:x > 0hsin:Real.sin x = 1⊢ x ≥ Real.pi / 2 -- the <;> tactic applies the next tactic to all currently visible goals. x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x := Real.sin_lt_sin_of_lt_of_le_pi_div_two (have this := Real.pi_pos; le_of_not_gt 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.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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_zero_add (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.neg_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.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.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.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 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_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.CancelDenoms.neg_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) (le_of_not_gt 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.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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 ℝ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 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_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl)) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) h⊢ -(Real.pi / 2) ≤ xx:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x := Real.sin_lt_sin_of_lt_of_le_pi_div_two (have this := Real.pi_pos; le_of_not_gt 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.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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_zero_add (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.neg_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.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.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.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 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_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.CancelDenoms.neg_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) (le_of_not_gt 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.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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 ℝ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 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_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl)) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) h⊢ Real.pi / 2 ≤ Real.pi / 2 x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x := Real.sin_lt_sin_of_lt_of_le_pi_div_two (have this := Real.pi_pos; le_of_not_gt 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.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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_zero_add (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.neg_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.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.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.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 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_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.CancelDenoms.neg_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) (le_of_not_gt 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.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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 ℝ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 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_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl)) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) h⊢ -(Real.pi / 2) ≤ xx:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:Real.sin 0 < Real.sin x := Real.sin_lt_sin_of_lt_of_le_pi_div_two (have this := Real.pi_pos; le_of_not_gt 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.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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_zero_add (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.zero_mul 0) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.neg_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.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.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.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 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_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.CancelDenoms.neg_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) (le_of_not_gt 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.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 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 (x ^ Nat.rawCast 1 * Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add (Real.pi ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 2))) (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul x (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 ℝ 2)) (Eq.refl (Int.negOfNat 2)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (x ^ Nat.rawCast 1 * (Int.negOfNat 2).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (Real.pi ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero x (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 ℝ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 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_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst rfl (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))))) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt h') (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.CancelDenoms.sub_subst (Mathlib.Tactic.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 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (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 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl)) (Mathlib.Tactic.Linarith.mul_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))))))) h⊢ Real.pi / 2 ≤ Real.pi / 2 All goals completed! 🐙 x:ℝh:x > 0hsin:Real.sin x = 1h':x < Real.pi / 2h1:0 < Real.sin xh2:Real.sin x < 1⊢ False All goals completed! 🐙