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 : 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 :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * b * ‖x‖
have rw : ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * (b * ‖x‖)
Tactic: rw [mul_assoc]
-- 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 : 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 :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * (b * ‖x‖)
have refine : dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ dist r 0 * (b * ‖x‖)
Tactic: refine this.trans ?_
-- 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 : 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 :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
⊢ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ dist r 0 * (b * ‖x‖)
have hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ b * ‖x‖
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 : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) n (⇑f : (a : V₁) → V₂) v‖ ≤ n • b * ‖v‖
have rw : ‖HSMul.hSMul (β := V₂) n ((f : (a : V₁) → V₂) v : V₂)‖ ≤ (↑n : ℝ) * (b * ‖v‖)
Tactic: rw [Pi.smul_apply, nsmul_eq_mul, mul_assoc]
-- 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 : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ (↑n : ℝ) * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ (↑n : ℝ) * (b * ‖v‖)
have hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ b * ‖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 : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) z (⇑f : (a : V₁) → V₂) v‖ ≤ ‖z‖ • b * ‖v‖
have rw : ‖HSMul.hSMul (β := V₂) z ((f : (a : V₁) → V₂) v : V₂)‖ ≤ ‖z‖ * (b * ‖v‖)
Tactic: rw [Pi.smul_apply, smul_eq_mul, mul_assoc]
-- 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 : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z‖ * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖z‖ * (b * ‖v‖)
have hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ b * ‖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 : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖g‖ * (‖f‖ * ‖v‖)
have hbc : 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 : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * ‖f‖ * ‖v‖
have rw : ‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * (‖f‖ * ‖v‖)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g‖ * ‖f‖ ≤ C₂ * C₁
have b0 : 0 ≤ C₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₃
have rw : ‖g.comp f‖ ≤ C₂ * C₁
Tactic: rw [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 : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
a b : NormedAddGroupHom V₁ V₂
⊢ (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) (a + b) =
    HAdd.hAdd (α := NormedAddGroupHom V₁ V₃) ((fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) a)
      ((fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) b)
have H : ∀ (x : V₁),
  Eq.{u_4 + 1} (α := V₃) (((fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) (a + b) : (a : V₁) → V₃) x : V₃)
    ((HAdd.hAdd (α := NormedAddGroupHom V₁ V₃) ((fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) a)
            ((fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) b) :
          (a : V₁) → V₃)
        x :
      V₃)
Tactic: ext
-- 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 : NormedAddGroupHom V₁ V₂
a b : NormedAddGroupHom V₂ V₃
⊢ (fun (g : NormedAddGroupHom V₂ V₃) ↦
        (AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) ⋯ :
          NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃))
      (a + b) =
    HAdd.hAdd (α := NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃)
      ((fun (g : NormedAddGroupHom V₂ V₃) ↦
          (AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) ⋯ :
            NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃))
        a)
      ((fun (g : NormedAddGroupHom V₂ V₃) ↦
          (AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) ⋯ :
            NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃))
        b)
have h : ∀ (x : NormedAddGroupHom V₁ V₂) (x_1 : V₁),
  Eq.{u_4 + 1} (α := V₃)
    (((((fun (g : NormedAddGroupHom V₂ V₃) ↦
                    (AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) sorry :
                      NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃))
                  (a + b) :
                (a : NormedAddGroupHom V₁ V₂) → NormedAddGroupHom V₁ V₃)
              x :
            NormedAddGroupHom V₁ V₃) :
          (a : V₁) → V₃)
        x_1 :
      V₃)
    ((((HAdd.hAdd (α := NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃)
                  ((fun (g : NormedAddGroupHom V₂ V₃) ↦
                      (AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) sorry :
                        NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃))
                    a)
                  ((fun (g : NormedAddGroupHom V₂ V₃) ↦
                      (AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) ↦ g.comp f) sorry :
                        NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃))
                    b) :
                (a : NormedAddGroupHom V₁ V₂) → NormedAddGroupHom V₁ V₃)
              x :
            NormedAddGroupHom V₁ V₃) :
          (a : V₁) → V₃)
        x_1 :
      V₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
⊢ Eq (α := NormedAddGroupHom V₁ V₃) (f.comp 0) 0
have H : ∀ (x : V₁), Eq.{u_4 + 1} (α := V₃) ((f.comp 0 : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
⊢ Eq (α := NormedAddGroupHom V₁ V₃) (NormedAddGroupHom.comp 0 f) 0
have H : ∀ (x : V₁), Eq.{u_4 + 1} (α := V₃) ((NormedAddGroupHom.comp 0 f : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst_3 : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
⊢ (h.comp g).comp f = h.comp (g.comp f)
have H : ∀ (x : V₁),
  Eq.{u_5 + 1} (α := V₄) (((h.comp g).comp f : (a : V₁) → V₄) x : V₄) ((h.comp (g.comp f) : (a : V₁) → V₄) x : V₄)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
s : AddSubgroup V
v : ↥s
⊢ ‖(↑v : V)‖ ≤ 1 * ‖v‖
have rw : ‖(↑v : V)‖ ≤ ‖v‖
Tactic: rw [one_mul, AddSubgroup.coe_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
s : AddSubgroup V
v : ↥s
rw : ‖(↑v : V)‖ ≤ ‖v‖
⊢ ‖(↑v : V)‖ ≤ 1 * ‖v‖
have rw₁ : ‖(↑v : V)‖ ≤ ‖(↑v : V)‖
Tactic: rw [one_mul, AddSubgroup.coe_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ v ∈ f.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
have rw : v ∈ f.toAddMonoidHom.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
Tactic: rw [ker, f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
rw : v ∈ f.toAddMonoidHom.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
⊢ v ∈ f.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
have rw₁ : Eq.{u_4 + 1} (α := V₂) ((f.toAddMonoidHom : (a : V₁) → V₂) v : V₂) (0 : V₂) ↔
  Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
Tactic: rw [ker, f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
rw : v ∈ f.toAddMonoidHom.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
rw₁ :
  Eq.{u_4 + 1} (α := V₂) ((f.toAddMonoidHom : (a : V₁) → V₂) v : V₂) (0 : V₂) ↔
    Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
⊢ v ∈ f.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
have rw₂ : Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂) ↔
  Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)
Tactic: rw [ker, f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v : V₁
⊢ Membership.mem (α := V₂) g.ker ((f : (a : V₁) → V₂) v : V₂)
have rw : Eq.{u_5 + 1} (α := V₃) ((g : (a : V₂) → V₃) ((f : (a : V₁) → V₂) v : V₂) : V₃) (0 : V₃)
Tactic: rw [g.mem_ker, ← comp_apply g f, h, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v : V₁
rw : Eq.{u_5 + 1} (α := V₃) ((g : (a : V₂) → V₃) ((f : (a : V₁) → V₂) v : V₂) : V₃) (0 : V₃)
⊢ Membership.mem (α := V₂) g.ker ((f : (a : V₁) → V₂) v : V₂)
have rw₁ : Eq.{u_5 + 1} (α := V₃) ((g.comp f : (a : V₁) → V₃) v : V₃) (0 : V₃)
Tactic: rw [g.mem_ker, ← comp_apply g f, h, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v : V₁
rw : Eq.{u_5 + 1} (α := V₃) ((g : (a : V₂) → V₃) ((f : (a : V₁) → V₂) v : V₂) : V₃) (0 : V₃)
rw₁ : Eq.{u_5 + 1} (α := V₃) ((g.comp f : (a : V₁) → V₃) v : V₃) (0 : V₃)
⊢ Membership.mem (α := V₂) g.ker ((f : (a : V₁) → V₂) v : V₂)
have rw₂ : Eq.{u_5 + 1} (α := V₃) ((0 : (a : V₁) → V₃) v : V₃) (0 : V₃)
Tactic: rw [g.mem_ker, ← comp_apply g f, h, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
v : V₁
rw : Eq.{u_5 + 1} (α := V₃) ((g : (a : V₂) → V₃) ((f : (a : V₁) → V₂) v : V₂) : V₃) (0 : V₃)
rw₁ : Eq.{u_5 + 1} (α := V₃) ((g.comp f : (a : V₁) → V₃) v : V₃) (0 : V₃)
rw₂ : Eq.{u_5 + 1} (α := V₃) ((0 : (a : V₁) → V₃) v : V₃) (0 : V₃)
⊢ Membership.mem (α := V₂) g.ker ((f : (a : V₁) → V₂) v : V₂)
have rw₃ : Eq.{u_5 + 1} (α := V₃) 0 0
Tactic: rw [g.mem_ker, ← comp_apply g f, h, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
⊢ (incl g.ker).comp (lift f g h) = f
have H : ∀ (x : V₁),
  Eq.{u_4 + 1} (α := V₂) (((incl g.ker).comp (lift f g h) : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) x : V₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
⊢ Eq.{u_3 + 1} (α := AddSubgroup V₁) (ker.{u_3, u_4} (V₂ := V₂) 0) ⊤
have h : ∀ (x : V₁),
  Membership.mem (γ := AddSubgroup V₁) (ker.{u_3, u_4} (V₂ := V₂) 0) x ↔ Membership.mem (γ := AddSubgroup V₁) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ (g.comp f).toAddMonoidHom.range = AddSubgroup.map g.toAddMonoidHom f.toAddMonoidHom.range
have rw : (g.comp f).toAddMonoidHom.range = (g.toAddMonoidHom.comp f.toAddMonoidHom).range
Tactic: rw [AddMonoidHom.map_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
⊢ (incl s).range = s
have h : ∀ (x : V₁), x ∈ (incl s).range ↔ x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
h : x ∈ (incl s).range
y : ↥s
hy : ((incl s).toAddMonoidHom : (a : ↥s) → V₁) y = x
⊢ x ∈ s
have rw : Membership.mem (α := V₁) s (((incl s).toAddMonoidHom : (a : ↥s) → V₁) y : V₁)
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ range (V₁ := ↥⊤) (f.comp (incl ⊤)) = f.range
have simp : f.toAddMonoidHom.range = f.range
Tactic: simp [comp_range, incl_range, ← AddMonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
⊢ f.NormNoninc ↔ ‖f‖ ≤ 1
have refine_1 : ∀ (h : f.NormNoninc), ‖f‖ ≤ 1
Tactic: refine ⟨fun h => ?_, fun h => fun v => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
refine_1 : ∀ (h : f.NormNoninc), ‖f‖ ≤ 1
⊢ f.NormNoninc ↔ ‖f‖ ≤ 1
have refine_2 : ∀ (h : ‖f‖ ≤ 1) (v : V), norm.{u_2} (E := W) ((f : (a : V) → W) v : W) ≤ ‖v‖
Tactic: refine ⟨fun h => ?_, fun h => fun v => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
⊢ ‖f‖ ≤ 1
have refine_1 : ∀ (v : V), norm.{u_2} (E := W) ((f : (a : V) → W) v : W) ≤ 1 * ‖v‖
Tactic: refine opNorm_le_bound _ zero_le_one fun v => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
⊢ f.comp (ι f g) = g.comp (ι f g)
have H : ∀ (x : ↥(f.equalizer g)),
  Eq.{u_2 + 1} (α := W) ((f.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
    ((g.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ Eq.{u_2 + 1} (α := W) ((f.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
    ((g.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
have H : Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((ι f g : (a : ↥(f.equalizer g)) → V) x : V) : W) (0 : W)
Tactic: rw [comp_apply, comp_apply, ← sub_eq_zero, ← NormedAddGroupHom.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) (0 : W)
have rw : HSub.hSub (α := W) (β := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
    ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) =
  0
Tactic: rw [NormedAddGroupHom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
rw :
  HSub.hSub (α := W) (β := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
      ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) =
    0
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) (0 : W)
have rw₁ : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
  ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
Tactic: rw [NormedAddGroupHom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]