x : ℝ
⊢ sin x = 0 ↔ 0 = sin x * sin x
x : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq x, sq, sq, ← sub_eq_iff_eq_add, sub_self]
no goals
x : ℝ
⊢ sin x = 0 ↔ 0 = sin x * sin x
exact ⟨fun h => by rw [h, MulZeroClass.mul_zero], eq_zero_of_mul_self_eq_zero ∘ Eq.symm⟩
no goals
x : ℝ
h : sin x = 0
⊢ 0 = sin x * sin x
rw [h, MulZeroClass.mul_zero]