awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : V₁ → V₂) (map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂)
  (bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖)
  (h : { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun = g.toFun),
  { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f g_1 g : NormedAddGroupHom V₁ V₂
toFun : V₁ → V₂
map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂
bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖
h : { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun = g.toFun
⊢ { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g
have mk : ∀ (toFun_1 : V₁ → V₂) (map_add'_1 : ∀ (v₁ v₂ : V₁), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂)
  (bound'_1 : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun_1 v‖ ≤ C * ‖v‖)
  (h :
    { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun =
      { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 : NormedAddGroupHom V₁ V₂ }.toFun),
  { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } =
    { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
H : Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
⊢ f = g
have mk : ∀ (toFun : V₁ → V₂) (map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂)
  (bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖)
  (H :
    Eq (α := (a : V₁) → V₂)
      (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
      (⇑g : (a : V₁) → V₂)),
  { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g
Tactic: cases f
Cleared hypotheses: f, H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun : V₁ → V₂
map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂
bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖
H :
  Eq (α := (a : V₁) → V₂)
    (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
    (⇑g : (a : V₁) → V₂)
⊢ { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g
have mk : ∀ (toFun_1 : V₁ → V₂) (map_add'_1 : ∀ (v₁ v₂ : V₁), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂)
  (bound'_1 : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun_1 v‖ ≤ C * ‖v‖)
  (H :
    Eq (α := (a : V₁) → V₂)
      (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
      (⇑{ toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)),
  { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } =
    { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }
Tactic: cases g
Cleared hypotheses: g, H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
⊢ Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
have rw : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
Tactic: rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
rw : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
⊢ Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
have rw₁ : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂)
Tactic: rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
rw : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
rw₁ : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂)
⊢ Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
have rw₂ : Eq (α := (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂)
Tactic: rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
k : V₂
k_in : k ∈ K
⊢ ∃ (g : V₁), (f : (a : V₁) → V₂) g = k ∧ ‖g‖ ≤ C' * ‖k‖
have rcases : ∀ (g : V₁) (k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂))
  (hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)),
  ∃ (g_1 : V₁),
    Eq.{u_3 + 1} (α := V₂) ((f : (a : V₁) → V₂) g_1 : V₂) ((f : (a : V₁) → V₂) g : V₂) ∧
      ‖g_1‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Tactic: rcases h k k_in with ⟨g, rfl, hg⟩
Cleared hypotheses: k, k_in
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ ∃ (g_1 : V₁),
    Eq.{u_3 + 1} (α := V₂) ((f : (a : V₁) → V₂) g_1 : V₂) ((f : (a : V₁) → V₂) g : V₂) ∧
      ‖g_1‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
have right : ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Tactic: use g, rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
have pos : ∀ (Hg : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0),
  ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Tactic: by_cases Hg : ‖f g‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
pos :
  ∀ (Hg : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0),
    ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
have neg : ∀ (Hg : ¬norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0),
  ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Tactic: by_cases Hg : ‖f g‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Hg : ¬norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0
⊢ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
have ha : 0 ≤ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'
have refine_1 : |C| + 1 > 0
Tactic: refine ⟨|C| + 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
refine_1 : |C| + 1 > 0
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'
have refine_2 : f.SurjectiveOnWith K (|C| + 1)
Tactic: refine ⟨|C| + 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ |C| + 1 > 0
have linarith : |C| + 1 ≤ 0 → -1 + (|C| + 1 - 0) + (0 - |C|) = 0
Tactic: linarith [abs_nonneg C]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ f.SurjectiveOnWith K (|C| + 1)
have refine_2 : C ≤ |C| + 1
Tactic: apply h.mono
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ C ≤ |C| + 1
have linarith : |C| + 1 < C → -1 + (|C| + 1 - C) + (C - |C|) = 0
Tactic: linarith [le_abs_self C]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have obtain : ∀ (C : ℝ) (_Cpos : 0 < C) (hC : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖),
  norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
Tactic: obtain ⟨C, _Cpos, hC⟩ := f.bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (hypothesis)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have hC₁ : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
Tactic: replace hC := hC x
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have pos : ∀ (h : ‖x‖ = 0), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
Tactic: by_cases h : ‖x‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
pos : ∀ (h : ‖x‖ = 0), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have neg : ∀ (h : ¬‖x‖ = 0), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
Tactic: by_cases h : ‖x‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ‖x‖ = 0
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have pos : ∀ (hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * 0) (h : ‖x‖ = 0),
  norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * 0
Tactic: rwa [h, mul_zero] at hC ⊢
Cleared hypotheses: hC, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ‖x‖ = 0
pos :
  ∀ (hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * 0) (h : ‖x‖ = 0),
    norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * 0
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have pos₁ : ∀ (hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ 0) (h : ‖x‖ = 0),
  norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ 0
Tactic: rwa [h, mul_zero] at hC ⊢
Cleared hypotheses: hC, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (hypothesis)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
have hlt : 0 < ‖x‖
Tactic: have hlt : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg x) (Ne.symm h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * c
have ha : 0 ≤ ‖f‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
h : ‖f‖ ≤ c
x : V₁
⊢ ‖f‖ * ‖x‖ ≤ c * ‖x‖
have ha : 0 ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) y : V₂) ≤
    (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯) : ℝ) * dist x y
have rw : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) (x - y) : V₂) ≤ (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ sorry) : ℝ) * ‖x - y‖
Tactic: rw [dist_eq_norm, dist_eq_norm, ← map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
x : V₁
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖
have hbc : C ≤ max C 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) + norm.{u_3} (E := V₂) ((g : (a : V₁) → V₂) v : V₂) ≤
    ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖
have h₁ : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
v : V₁
h₁ : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) + norm.{u_3} (E := V₂) ((g : (a : V₁) → V₂) v : V₂) ≤
    ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖
have h₂ : norm.{u_3} (E := V₂) ((g : (a : V₁) → V₂) v : V₂) ≤ ‖g‖ * ‖v‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = (‖f‖ + ‖g‖) * ‖v‖
have rw : ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
x : V₁
⊢ norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) x : V₂) = 0 * ‖x‖
have rw : norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) x : V₂) = 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_5
V₂ : Type u_6
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ ‖f‖ * ‖x‖ = 0
have rw : 0 * ‖x‖ = 0
Tactic: rw [hn, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_5
V₂ : Type u_6
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
rw : 0 * ‖x‖ = 0
⊢ ‖f‖ * ‖x‖ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [hn, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_5
V₂ : Type u_6
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hf : f = 0
⊢ ‖f‖ = 0
have rw : norm (E := NormedAddGroupHom V₁ V₂) 0 = 0
Tactic: rw [hf, opNorm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_5
V₂ : Type u_6
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hf : f = 0
rw : norm (E := NormedAddGroupHom V₁ V₂) 0 = 0
⊢ ‖f‖ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [hf, opNorm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
⊢ 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
have let : ∀ (x : V) (hx : ‖x‖ ≠ 0), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
Tactic: let ⟨x, hx⟩ := exists_norm_ne_zero V
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (hypothesis)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
have this : norm (E := V) ((id V : (a : V) → V) x : V) / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)
Tactic: have := (id V).ratio_le_opNorm x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : norm (E := V) ((id V : (a : V) → V) x : V) / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)
⊢ 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
have rwa : ∀ (this : ‖x‖ / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
Tactic: rwa [id_apply, div_self hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : norm (E := V) ((id V : (a : V) → V) x : V) / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)
rwa : ∀ (this : ‖x‖ / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
⊢ 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
have rwa₁ : ∀ (this : 1 ≤ norm (E := NormedAddGroupHom V V) (id V)), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
Tactic: rwa [id_apply, div_self hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
⊢ ∃ (C : ℝ), ∀ (v : V₁), ‖(↑(f.toAddMonoidHom - g.toAddMonoidHom) : ZeroHom V₁ V₂).toFun v‖ ≤ C * ‖v‖
have simp : ∃ (C : ℝ), ∀ (v : V₁), norm.{u_3} (E := V₂) ((f.toAddMonoidHom + -g.toAddMonoidHom : (a : V₁) → V₂) v : V₂) ≤ C * ‖v‖
Tactic: simp only [AddMonoidHom.toFun_eq_coe, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (hypothesis)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * b * ‖x‖
have this : dist (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)) (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) 0 : V₂)) ≤
  dist r 0 * dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) 0 : V₂)
Tactic: have := dist_smul_pair r (f x) (f 0)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (hypothesis)
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  dist (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)) (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) 0 : V₂)) ≤
    dist r 0 * dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) 0 : V₂)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * b * ‖x‖
have this₁ : ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
Tactic: rw [map_zero, smul_zero, dist_zero_right, dist_zero_right] at this
Cleared hypotheses: this