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