case mp
θ ψ : ℝ
⊢ sin θ = sin ψ → ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ
θ ψ : ℝ
⊢ sin θ = sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
constructor
case mp
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
case mp
θ ψ : ℝ
⊢ sin θ = sin ψ → ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
intro Hsin
case mp
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
case mp
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
case mp
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
cases' cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h h
case mp.inr.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
right
case mp.inr.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π
case mp.inr.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π
rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add,
  add_halves, sub_sub, sub_eq_zero] at h
no goals
case mp.inr.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π
exact h.symm
case mp.inl.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
left
case mp.inl.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ
case mp.inl.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ
rw [coe_sub, coe_sub] at h
no goals
case mp.inl.h
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2) - ↑ψ
⊢ ↑θ = ↑ψ
exact sub_right_inj.1 h
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - (π - ψ) = 2 * π * ↑k) → sin θ = sin ψ
case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ
rw [angle_eq_iff_two_pi_dvd_sub, ← eq_sub_iff_add_eq, ← coe_sub, angle_eq_iff_two_pi_dvd_sub]
case mpr.inl.intro
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ sin θ = sin ψ

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

case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ sin θ = sin ψ
rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left _ (two_ne_zero' ℝ),
  mul_comm π _, sin_int_mul_pi, MulZeroClass.mul_zero, MulZeroClass.zero_mul]
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ sin θ = sin ψ
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ sin θ = sin ψ
have H' : θ + ψ = 2 * k * π + π := by
  rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
    mul_assoc] at H
no goals
case mpr.inr.intro
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ sin θ = sin ψ
rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
  mul_div_cancel_left _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
  MulZeroClass.mul_zero]
no goals
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ θ + ψ = 2 * ↑k * π + π
rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
  mul_assoc] at H