-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem UniformCauchySeqOnFilter.one_smulRight {l' : Filter 𝕜}
    (hf' : UniformCauchySeqOnFilter f' l l') :
    UniformCauchySeqOnFilter (fun n => fun z => (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)) l l'

Proof state:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l',
      dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε

Tactic:
intro ε hε

Result:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l',
    dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : (ι × ι) × 𝕜
hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q
z : 𝕜
⊢ ‖(ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) z‖ ≤ q * ‖z‖

Tactic:
simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.one_apply]

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : (ι × ι) × 𝕜
hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q
z : 𝕜
⊢ ‖z • f' n.1.1 n.2 - z • f' n.1.2 n.2‖ ≤ q * ‖z‖

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
⊢ ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l',
    dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε

Tactic:
apply (hf' q hq).mono

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
⊢ ∀ (x : (ι × ι) × 𝕜),
    dist (0 x.2) (f' x.1.1 x.2 - f' x.1.2 x.2) < q →
      dist (0 x.2) (ContinuousLinearMap.smulRight 1 (f' x.1.1 x.2) - ContinuousLinearMap.smulRight 1 (f' x.1.2 x.2)) < ε

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : (ι × ι) × 𝕜
hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q
z : 𝕜
⊢ ‖z • f' n.1.1 n.2 - z • f' n.1.2 n.2‖ ≤ q * ‖z‖

Tactic:
rw [← smul_sub, norm_smul, mul_comm]

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : (ι × ι) × 𝕜
hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q
z : 𝕜
⊢ ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ * ‖z‖ ≤ q * ‖z‖

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : (ι × ι) × 𝕜
hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q
z : 𝕜
⊢ ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ * ‖z‖ ≤ q * ‖z‖

Tactic:
gcongr

Result:
no goals