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

State before:
x : ℝ
⊢ x.cos ^ 2 = 1 / 2 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
rw [cos_sq]
State after:
x : ℝ
⊢ 1 / 2 + (2 * x).cos / 2 = 1 / 2 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4

State before:
x : ℝ
⊢ 1 / 2 + (2 * x).cos / 2 = 1 / 2 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
simp only [add_right_eq_self, div_eq_zero_iff]
State after:
x : ℝ
⊢ (2 * x).cos = 0 ∨ 2 = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4

State before:
x : ℝ
⊢ (2 * x).cos = 0 ∨ 2 = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
norm_num
State after:
x : ℝ
⊢ (2 * x).cos = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4

State before:
x : ℝ
⊢ (2 * x).cos = 0 ↔ ∃ k, x = (2 * ↑k + 1) * π / 4
Tactic:
rw [cos_eq_zero_iff]
State after:
x : ℝ
⊢ (∃ k, 2 * x = (2 * ↑k + 1) * π / 2) ↔ ∃ k, x = (2 * ↑k + 1) * π / 4

State before:
case mpr
x : ℝ
⊢ (∃ k, x = (2 * ↑k + 1) * π / 4) → ∃ k, 2 * x = (2 * ↑k + 1) * π / 2
Tactic:
rintro ⟨k, h⟩
State after:
case mpr.intro
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ ∃ k, 2 * x = (2 * ↑k + 1) * π / 2

State before:
case mpr.intro
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ ∃ k, 2 * x = (2 * ↑k + 1) * π / 2
Tactic:
use k
State after:
case h
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ 2 * x = (2 * ↑k + 1) * π / 2

State before:
case h
x : ℝ
k : ℤ
h : x = (2 * ↑k + 1) * π / 4
⊢ 2 * x = (2 * ↑k + 1) * π / 2
Tactic:
linarith
State after:
no goals