θ : Angle
⊢ tan (θ + ↑π) = tan θ
⊢ Function.Periodic tan ↑π
intro θ
case h
x✝ : ℝ
⊢ tan (↑x✝ + ↑π) = tan ↑x✝
θ : Angle
⊢ tan (θ + ↑π) = tan θ
induction θ using Real.Angle.induction_on
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝
case h
x✝ : ℝ
⊢ tan (↑x✝ + ↑π) = tan ↑x✝
rw [← coe_add, tan_coe, tan_coe]
no goals
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝
exact Real.tan_periodic _