Theorem: HasExtension.sub (Ray/Hartogs/Subharmonic.lean)

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f0 f1 : C(Real.Angle, ℂ)
g0 g1 : ℂ → ℂ
e0 : HasExtension f0 g0 c r
e1 : HasExtension f1 g1 c r
⊢ ∀ (t : Real.Angle), (f0 - f1) t = (g0 - g1) (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
simp only [e0.b, e1.b, ContinuousMap.coe_sub, Pi.sub_apply, eq_self_iff_true,
forall_const]
State after:
no goals