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

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

State before:
x : ℝ
⊢ (∃ k, 3 * x = (2 * ↑k + 1) * π / 2) ↔ ∃ k, x = (2 * ↑k + 1) * π / 6
Tactic:
refine exists_congr fun k => ?_
State after:
x : ℝ
k : ℤ
⊢ 3 * x = (2 * ↑k + 1) * π / 2 ↔ x = (2 * ↑k + 1) * π / 6

State before:
x : ℝ
k : ℤ
⊢ 3 * x = (2 * ↑k + 1) * π / 2 ↔ x = (2 * ↑k + 1) * π / 6
Tactic:
constructor <;> intro <;> linarith
State after:
no goals