θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ abs (cos θ) = abs (sin ψ)
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ abs (cos θ) = abs (sin ψ)
simp_rw [two_zsmul, ← two_nsmul] at h
no goals
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ abs (cos θ) = abs (sin ψ)
exact abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h