⊢ ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ ContinuousOn tan {x | cos x ≠ 0}
suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0} by
  have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
  rwa [h_eq] at this
no goals
⊢ ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
exact continuousOn_sin.div continuousOn_cos fun x => id
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
h_eq : (fun x => sin x / cos x) = tan
⊢ ContinuousOn tan {x | cos x ≠ 0}
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ ContinuousOn tan {x | cos x ≠ 0}
have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
no goals
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
h_eq : (fun x => sin x / cos x) = tan
⊢ ContinuousOn tan {x | cos x ≠ 0}
rwa [h_eq] at this
case h
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ (fun x => sin x / cos x) = tan
ext1 x
no goals
case h
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
rw [tan_eq_sin_div_cos]