ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.fst) (f' n.fst n.snd) n.snd
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
⊢ HasDerivAt g (g' x) x
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.fst) (f' n.fst n.snd) n.snd
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
⊢ HasDerivAt g (g' x) x
let F' n z := (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.fst) (f' n.fst n.snd) n.snd
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
⊢ HasDerivAt g (g' x) x
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.fst) (f' n.fst n.snd) n.snd
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
⊢ HasDerivAt g (g' x) x
let G' z := (1 : 𝕜 →L[𝕜] 𝕜).smulRight (g' z)
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ HasFDerivAt g (ContinuousLinearMap.smulRight 1 (g' x)) x
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.fst) (f' n.fst n.snd) n.snd
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
⊢ HasDerivAt g (g' x) x
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf ⊢
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf'✝ : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x)
⊢ HasFDerivAt g (ContinuousLinearMap.smulRight 1 (g' x)) x
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ HasFDerivAt g (ContinuousLinearMap.smulRight 1 (g' x)) x
have hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x) := by
  rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
  intro ε hε
  obtain ⟨q, hq, hq'⟩ := exists_between hε.lt
  apply (hf' q hq).mono
  intro n hn
  refine' lt_of_le_of_lt _ hq'
  simp only [dist_eq_norm] at hn ⊢
  refine' ContinuousLinearMap.op_norm_le_bound _ hq.le _
  intro z
  simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
    ContinuousLinearMap.one_apply]
  rw [← smul_sub, norm_smul, mul_comm]
  gcongr
no goals
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf'✝ : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x)
⊢ HasFDerivAt g (ContinuousLinearMap.smulRight 1 (g' x)) x
exact hasFDerivAt_of_tendstoUniformlyOnFilter hf' hf hfg
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (G' n.snd) (F' n.fst n.snd) < ε
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ TendstoUniformlyOnFilter F' G' l (𝓝 x)
rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (G' n.snd) (F' n.fst n.snd) < ε
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (G' n.snd) (F' n.fst n.snd) < ε
intro ε hε
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
⊢ ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (G' n.snd) (F' n.fst n.snd) < ε
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (G' n.snd) (F' n.fst n.snd) < ε
obtain ⟨q, hq, hq'⟩ := exists_between hε.lt
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
⊢ ∀ (x : ι × 𝕜), dist (g' x.snd) (f' x.fst x.snd) < q → dist (G' x.snd) (F' x.fst x.snd) < ε
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
⊢ ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (G' n.snd) (F' n.fst n.snd) < ε
apply (hf' q hq).mono
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.snd) (f' n.fst n.snd) < q
⊢ dist (G' n.snd) (F' n.fst n.snd) < ε
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
⊢ ∀ (x : ι × 𝕜), dist (g' x.snd) (f' x.fst x.snd) < q → dist (G' x.snd) (F' x.fst x.snd) < ε
intro n hn
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.snd) (f' n.fst n.snd) < q
⊢ dist (G' n.snd) (F' n.fst n.snd) ≤ q
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.snd) (f' n.fst n.snd) < q
⊢ dist (G' n.snd) (F' n.fst n.snd) < ε
refine' lt_of_le_of_lt _ hq'
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
⊢ ‖ContinuousLinearMap.smulRight 1 (g' n.snd) - ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)‖ ≤ q
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.snd) (f' n.fst n.snd) < q
⊢ dist (G' n.snd) (F' n.fst n.snd) ≤ q
simp only [dist_eq_norm] at hn ⊢
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
⊢ ∀ (x : 𝕜),
    ‖↑(ContinuousLinearMap.smulRight 1 (g' n.snd) - ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) x‖ ≤ q * ‖x‖
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
⊢ ‖ContinuousLinearMap.smulRight 1 (g' n.snd) - ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)‖ ≤ q
refine' ContinuousLinearMap.op_norm_le_bound _ hq.le _
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
z : 𝕜
⊢ ‖↑(ContinuousLinearMap.smulRight 1 (g' n.snd) - ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) z‖ ≤ q * ‖z‖
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
⊢ ∀ (x : 𝕜),
    ‖↑(ContinuousLinearMap.smulRight 1 (g' n.snd) - ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) x‖ ≤ q * ‖x‖
intro z
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
z : 𝕜
⊢ ‖z • g' n.snd - z • f' n.fst n.snd‖ ≤ q * ‖z‖
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
z : 𝕜
⊢ ‖↑(ContinuousLinearMap.smulRight 1 (g' n.snd) - ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) z‖ ≤ q * ‖z‖
simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.one_apply]
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
z : 𝕜
⊢ ‖g' n.snd - f' n.fst n.snd‖ * ‖z‖ ≤ q * ‖z‖
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
z : 𝕜
⊢ ‖z • g' n.snd - z • f' n.fst n.snd‖ ≤ q * ‖z‖
rw [← smul_sub, norm_smul, mul_comm]
no goals
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : IsROrC 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝ : NeBot l
hf' : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.snd) (f' n.fst n.snd) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.fst) (ContinuousLinearMap.smulRight 1 (f' n.fst n.snd)) n.snd
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.snd - f' n.fst n.snd‖ < q
z : 𝕜
⊢ ‖g' n.snd - f' n.fst n.snd‖ * ‖z‖ ≤ q * ‖z‖
gcongr