θ : ℂ
h : 2 * sin θ * cos θ = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
have h := (sin_two_mul θ).symm
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
θ : ℂ
h : 2 * sin θ * cos θ = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
rw [mul_assoc] at h
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ sin (θ * 2) / 2 = 0 / 2 ↔ ∃ k, θ = ↑k * ↑π / 2
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * ↑π / 2
rw [tan, div_eq_zero_iff, ← mul_eq_zero, ← MulZeroClass.zero_mul (1 / 2 : ℂ), mul_one_div,
  CancelDenoms.cancel_factors_eq_div h two_ne_zero, mul_comm]
no goals
θ : ℂ
h : 2 * (sin θ * cos θ) = sin (2 * θ)
⊢ sin (θ * 2) / 2 = 0 / 2 ↔ ∃ k, θ = ↑k * ↑π / 2
simpa only [zero_div, MulZeroClass.zero_mul, Ne.def, not_false_iff, field_simps] using
  sin_eq_zero_iff