θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ abs (cos θ) = abs (sin ψ)
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ abs (cos θ) = abs (sin ψ)
rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h
no goals
θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ abs (cos θ) = abs (sin ψ)
rcases h with (rfl | rfl) <;> simp [cos_pi_div_two_sub]