Theorem: IsClosed.extendable (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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
⊢ ∀ f ∈ closure s, Extendable f c r
Tactic:
intro F Fe
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
⊢ Extendable F c r

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
⊢ Extendable F c r
Tactic:
have fu : FrechetUrysohnSpace C(Real.Angle, ℂ) := by
  apply @FirstCountableTopology.frechetUrysohnSpace
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r
Tactic:
rw [← seqClosure_eq_closure] at Fe
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ seqClosure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ seqClosure s
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
⊢ Extendable F c r
Tactic:
rcases Fe with ⟨f, fs, fF⟩
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : Tendsto f atTop (𝓝 F)
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : Tendsto f atTop (𝓝 F)
⊢ Extendable F c r
Tactic:
simp only [ContinuousMap.tendsto_iff_tendstoLocallyUniformly,
  tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace] at fF
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
⊢ Extendable F c r
Tactic:
generalize hg : (fun n ↦ Classical.choose (e _ (fs n))) = g
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ Extendable F c r
Tactic:
have gs : ∀ n, HasExtension (f n) (g n) c r := by
  rw [← hg]; exact fun n ↦ Classical.choose_spec (e _ (fs n))
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ Extendable F c r
Tactic:
have cauchy : UniformCauchySeqOn g atTop (closedBall c r) := by
  rw [Metric.uniformCauchySeqOn_iff]
  simp_rw [Metric.tendstoUniformly_iff, Filter.eventually_atTop] at fF
  intro t tp; rcases fF (t / 4) (by linarith) with ⟨N, H⟩; exists N
  intro a aN b bN z zs
  have eab := (gs a).sub (gs b)
  have fab : ∀ u : Real.Angle, ‖f a u - f b u‖ ≤ t / 2 := by
    intro u
    have ta := H a aN u
    have tb := H b bN u
    rw [← dist_eq_norm]; rw [dist_comm] at ta
    calc dist (f a u) (f b u)
      _ ≤ dist (f a u) (F u) + dist (F u) (f b u) := dist_triangle _ _ _
      _ ≤ t / 4 + t / 4 := by linarith
      _ = t / 2 := by ring_nf
  have m := Extension.maximum_principle eab fab rp z zs
  simp only [Complex.dist_eq, Pi.sub_apply, Complex.norm_eq_abs] at m ⊢
  exact lt_of_le_of_lt m (by linarith)
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
⊢ Extendable F c r
Tactic:
set G := fun z ↦ limUnder atTop fun n ↦ g n z
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ Extendable F c r
Tactic:
have gG : TendstoUniformlyOn g G atTop (closedBall c r) := by
  apply UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto cauchy
  intro z zs; exact (cauchy.cauchySeq zs).tendsto_limUnder
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ Extendable F c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ Extendable F c r
Tactic:
exists G
State after:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ HasExtension F G c r

State before:
case intro.intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ HasExtension F G c r
Tactic:
exact
  { gh := uniform_harmonic_lim (fun n ↦ (gs n).gh) gG
    b := by
      intro z
      refine (Filter.Tendsto.limUnder_eq ?_).symm
      simp_rw [← (gs _).b]
      exact fF.tendsto_at z }
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
Fe : F ∈ closure s
⊢ FrechetUrysohnSpace C(Real.Angle, ℂ)
Tactic:
apply @FirstCountableTopology.frechetUrysohnSpace
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ ∀ (n : ℕ), HasExtension (f n) (g n) c r
Tactic:
rw [← hg]
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ ∀ (n : ℕ), HasExtension (f n) ((fun n => Classical.choose ⋯) n) c r

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
⊢ ∀ (n : ℕ), HasExtension (f n) ((fun n => Classical.choose ⋯) n) c r
Tactic:
exact fun n ↦ Classical.choose_spec (e _ (fs n))
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ UniformCauchySeqOn g atTop (closedBall c r)
Tactic:
rw [Metric.uniformCauchySeqOn_iff]
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε
Tactic:
simp_rw [Metric.tendstoUniformly_iff, Filter.eventually_atTop] at fF
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < ε
Tactic:
intro t tp
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Tactic:
rcases fF (t / 4) (by linarith) with ⟨N, H⟩
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Tactic:
exists N
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
⊢ ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ closedBall c r, dist (g m x) (g n x) < t
Tactic:
intro a aN b bN z zs
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
⊢ dist (g a z) (g b z) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
⊢ dist (g a z) (g b z) < t
Tactic:
have eab := (gs a).sub (gs b)
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
⊢ dist (g a z) (g b z) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
⊢ dist (g a z) (g b z) < t
Tactic:
have fab : ∀ u : Real.Angle, ‖f a u - f b u‖ ≤ t / 2 := by
  intro u
  have ta := H a aN u
  have tb := H b bN u
  rw [← dist_eq_norm]; rw [dist_comm] at ta
  calc dist (f a u) (f b u)
    _ ≤ dist (f a u) (F u) + dist (F u) (f b u) := dist_triangle _ _ _
    _ ≤ t / 4 + t / 4 := by linarith
    _ = t / 2 := by ring_nf
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t
Tactic:
have m := Extension.maximum_principle eab fab rp z zs
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : ‖(g a - g b) z‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : ‖(g a - g b) z‖ ≤ t / 2
⊢ dist (g a z) (g b z) < t
Tactic:
simp only [Complex.dist_eq, Pi.sub_apply, Complex.norm_eq_abs] at m ⊢
State after:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : Complex.abs (g a z - g b z) ≤ t / 2
⊢ Complex.abs (g a z - g b z) < t

State before:
case intro
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : Complex.abs (g a z - g b z) ≤ t / 2
⊢ Complex.abs (g a z - g b z) < t
Tactic:
exact lt_of_le_of_lt m (by linarith)
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
⊢ t / 4 > 0
Tactic:
linarith
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
⊢ ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
intro u
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
have ta := H a aN u
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
have tb := H b bN u
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ ‖(f a) u - (f b) u‖ ≤ t / 2
Tactic:
rw [← dist_eq_norm]
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist (F u) ((f a) u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2
Tactic:
rw [dist_comm] at ta
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) ((f b) u) ≤ t / 2
Tactic:
calc dist (f a u) (f b u)
  _ ≤ dist (f a u) (F u) + dist (F u) (f b u) := dist_triangle _ _ _
  _ ≤ t / 4 + t / 4 := by linarith
  _ = t / 2 := by ring_nf
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ dist ((f a) u) (F u) + dist (F u) ((f b) u) ≤ t / 4 + t / 4
Tactic:
linarith
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
u : Real.Angle
ta : dist ((f a) u) (F u) < t / 4
tb : dist (F u) ((f b) u) < t / 4
⊢ t / 4 + t / 4 = t / 2
Tactic:
ring_nf
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
fF : ∀ ε > 0, ∃ a, ∀ b ≥ a, ∀ (x : Real.Angle), dist (F x) ((f b) x) < ε
t : ℝ
tp : t > 0
N : ℕ
H : ∀ b ≥ N, ∀ (x : Real.Angle), dist (F x) ((f b) x) < t / 4
a : ℕ
aN : a ≥ N
b : ℕ
bN : b ≥ N
z : ℂ
zs : z ∈ closedBall c r
eab : HasExtension (f a - f b) (g a - g b) c r
fab : ∀ (u : Real.Angle), ‖(f a) u - (f b) u‖ ≤ t / 2
m : Complex.abs (g a z - g b z) ≤ t / 2
⊢ t / 2 < t
Tactic:
linarith
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ TendstoUniformlyOn g G atTop (closedBall c r)
Tactic:
apply UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto cauchy
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ ∀ x ∈ closedBall c r, Tendsto (fun n => g n x) atTop (𝓝 (G x))

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
⊢ ∀ x ∈ closedBall c r, Tendsto (fun n => g n x) atTop (𝓝 (G x))
Tactic:
intro z zs
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
z : ℂ
zs : z ∈ closedBall c r
⊢ Tendsto (fun n => g n z) atTop (𝓝 (G z))

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
z : ℂ
zs : z ∈ closedBall c r
⊢ Tendsto (fun n => g n z) atTop (𝓝 (G z))
Tactic:
exact (cauchy.cauchySeq zs).tendsto_limUnder
State after:
no goals

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
⊢ ∀ (t : Real.Angle), F t = G (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
intro z
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ F z = G (c + ↑r * ↑(AddCircle.toCircle z))

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ F z = G (c + ↑r * ↑(AddCircle.toCircle z))
Tactic:
refine (Filter.Tendsto.limUnder_eq ?_).symm
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => g n (c + ↑r * ↑(AddCircle.toCircle z))) atTop (𝓝 (F z))

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => g n (c + ↑r * ↑(AddCircle.toCircle z))) atTop (𝓝 (F z))
Tactic:
simp_rw [← (gs _).b]
State after:
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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => (f n) z) atTop (𝓝 (F z))

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 : ℝ
s : Set C(Real.Angle, ℂ)
e : ∀ f ∈ s, Extendable f c r
rp : r > 0
F : C(Real.Angle, ℂ)
fu : FrechetUrysohnSpace C(Real.Angle, ℂ)
f : ℕ → C(Real.Angle, ℂ)
fs : ∀ (n : ℕ), f n ∈ s
fF : TendstoUniformly (fun i a => (f i) a) (⇑F) atTop
g : ℕ → ℂ → ℂ
hg : (fun n => Classical.choose ⋯) = g
gs : ∀ (n : ℕ), HasExtension (f n) (g n) c r
cauchy : UniformCauchySeqOn g atTop (closedBall c r)
G : ℂ → ℂ := fun z => limUnder atTop fun n => g n z
gG : TendstoUniformlyOn g G atTop (closedBall c r)
z : Real.Angle
⊢ Tendsto (fun n => (f n) z) atTop (𝓝 (F z))
Tactic:
exact fF.tendsto_at z
State after:
no goals