θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ tan θ = tan ψ
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ tan θ = tan ψ
rw [two_nsmul_eq_iff] at h
case inl
θ : Angle
⊢ tan θ = tan θ

case inr
ψ : Angle
⊢ tan (ψ + ↑π) = tan ψ
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ tan θ = tan ψ
rcases h with (rfl | rfl)
no goals
case inl
θ : Angle
⊢ tan θ = tan θ
rfl
no goals
case inr
ψ : Angle
⊢ tan (ψ + ↑π) = tan ψ
exact tan_add_pi _