Theorem: Imo1962P4.finding_zeros (Compfiles/Imo1962P4.lean)

State before:
x : ℝ
⊢ altFormula x = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
simp only [altFormula, mul_assoc, mul_eq_zero, sub_eq_zero]
State after:
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

State before:
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 ↔ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
constructor
State after:
case mp
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

case mpr
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

State before:
case mp
x : ℝ
⊢ x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
rintro (h1 | h2)
State after:
case mp.inl
x : ℝ
h1 : x.cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

case mp.inr
x : ℝ
h2 : x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0

State before:
case mp.inl
x : ℝ
h1 : x.cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
right
State after:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ (3 * x).cos = 0

State before:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ (3 * x).cos = 0
Tactic:
rw [cos_three_mul, h1]
State after:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ 4 * 0 ^ 3 - 3 * 0 = 0

State before:
case mp.inl.h
x : ℝ
h1 : x.cos = 0
⊢ 4 * 0 ^ 3 - 3 * 0 = 0
Tactic:
ring
State after:
no goals

State before:
case mp.inr
x : ℝ
h2 : x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
exact h2
State after:
no goals

State before:
case mpr
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0 → x.cos = 0 ∨ x.cos ^ 2 = 1 / 2 ∨ (3 * x).cos = 0
Tactic:
exact Or.inr
State after:
no goals