case mp
θ ψ : ℝ
⊢ cos θ = cos ψ → ↑θ = ↑ψ ∨ ↑θ = -↑ψ

case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ → cos θ = cos ψ
θ ψ : ℝ
⊢ cos θ = cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
constructor
case mp
θ ψ : ℝ
Hcos : cos θ = cos ψ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
case mp
θ ψ : ℝ
⊢ cos θ = cos ψ → ↑θ = ↑ψ ∨ ↑θ = -↑ψ
intro Hcos
case mp
θ ψ : ℝ
Hcos✝ : cos θ = cos ψ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ ∃ n, ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
case mp
θ ψ : ℝ
Hcos : cos θ = cos ψ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
rw [← sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero,
  eq_false (two_ne_zero' ℝ), false_or_iff, sin_eq_zero_iff, sin_eq_zero_iff] at Hcos
case mp.inl.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

case mp.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
case mp
θ ψ : ℝ
Hcos✝ : cos θ = cos ψ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ ∃ n, ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
case mp.inl.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = -↑ψ
case mp.inl.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
right
case mp.inl.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ
case mp.inl.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = -↑ψ
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn
no goals
case mp.inl.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ
rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, coe_int_mul_eq_zsmul,
  mul_comm, coe_two_pi, zsmul_zero]
case mp.inr.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ
case mp.inr.intro
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
left
case mp.inr.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑θ = ↑ψ
case mp.inr.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn
no goals
case mp.inr.intro.h
θ ψ : ℝ
Hcos : cos θ = cos ψ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑θ = ↑ψ
rw [← hn, coe_add, mul_assoc, coe_int_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
  zero_add]
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - -ψ = 2 * π * ↑k) → cos θ = cos ψ
case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ → cos θ = cos ψ
rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]
case mpr.inl.intro
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ cos θ = cos ψ

case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ cos θ = cos ψ
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - -ψ = 2 * π * ↑k) → cos θ = cos ψ
rintro (⟨k, H⟩ | ⟨k, H⟩)
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ cos θ = cos ψ
case mpr.inl.intro
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ cos θ = cos ψ

case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ cos θ = cos ψ
rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left _ (two_ne_zero' ℝ),
  mul_comm π _, sin_int_mul_pi, MulZeroClass.mul_zero]
no goals
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ cos θ = cos ψ
rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
  mul_div_cancel_left _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, MulZeroClass.mul_zero,
  MulZeroClass.zero_mul]