awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖
⊢ ‖g‖ * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖g‖ * (‖f‖ * ‖v‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖

Tactic:
apply le_opNorm

Premises used: NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
rw rw₁ : ‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * (‖f‖ * ‖v‖)
⊢ ‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * ‖f‖ * ‖v‖

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
⊢ 0 ≤ ‖g‖ * ‖f‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
b0 : 0 ≤ C₂
⊢ ‖g‖ * ‖f‖ ≤ C₂ * C₁

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
⊢ 0 ≤ C₂

Tactic:
le_trans (norm_nonneg _) hg

Premises used: norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
⊢ 0 ≤ C₂

Tactic:
exact le_trans (norm_nonneg _) hg

Premises used: norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₁
rw : ‖g.comp f‖ ≤ C₂ * C₁
⊢ ‖g.comp f‖ ≤ C₃

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂ * C₁

Tactic:
norm_comp_le_of_le hg hf

Premises used: NormedAddGroupHom.norm_comp_le_of_le
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂ * C₁

Tactic:
exact norm_comp_le_of_le hg hf

Premises used: NormedAddGroupHom.norm_comp_le_of_le
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂
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₃)
⊢ (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)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂
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:
map_add g _ _

Premises used: map_add
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂
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:
exact map_add g _ _

Premises used: map_add
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
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) ⋯ :
                        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) ⋯ :
                          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) :
                  (a : NormedAddGroupHom V₁ V₂) → NormedAddGroupHom V₁ V₃)
                x :
              NormedAddGroupHom V₁ V₃) :
            (a : V₁) → V₃)
          x_1 :
        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)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
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) ⋯ :
                      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) ⋯ :
                        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) :
                (a : NormedAddGroupHom V₁ V₂) → NormedAddGroupHom V₁ V₃)
              x :
            NormedAddGroupHom V₁ V₃) :
          (a : V₁) → V₃)
        x_1 :
      V₃)

Tactic:
simp only [comp_apply, Pi.add_apply, AddMonoidHom.add_apply,
        AddMonoidHom.mk'_apply, coe_add]

Premises used: Pi.add_apply, NormedAddGroupHom.comp_apply, AddMonoidHom.mk'_apply, AddMonoidHom.add_apply, NormedAddGroupHom.coe_add
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
H : ∀ (x : V₁), Eq.{u_4 + 1} (α := V₃) ((f.comp 0 : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)
⊢ Eq (α := NormedAddGroupHom V₁ V₃) (f.comp 0) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
x : V₁
⊢ Eq.{u_4 + 1} (α := V₃) ((f.comp 0 : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
x : V₁
⊢ Eq.{u_4 + 1} (α := V₃) ((f.comp 0 : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)

Tactic:
exact map_zero f

Premises used: map_zero
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂
H :
  ∀ (x : V₁), Eq.{u_4 + 1} (α := V₃) ((NormedAddGroupHom.comp 0 f : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)
⊢ Eq (α := NormedAddGroupHom V₁ V₃) (NormedAddGroupHom.comp 0 f) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂
x : V₁
⊢ Eq.{u_4 + 1} (α := V₃) ((NormedAddGroupHom.comp 0 f : (a : V₁) → V₃) x : V₃) ((0 : (a : V₁) → V₃) x : V₃)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
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 :
  ∀ (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₄)
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂
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:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
⊢ Eq (α := (a : V₁) → V₃) (⇑(g.comp f) : (a : V₁) → V₃)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := V₂) (⇑g : (a : V₂) → V₃) (⇑f : (a : V₁) → V₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
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‖
rw₁ rw₂ : ‖(↑v : V)‖ ≤ ‖(↑v : V)‖
⊢ ‖(↑v : V)‖ ≤ 1 * ‖v‖

Tactic:
rw [one_mul, AddSubgroup.coe_norm]

Premises used: AddSubgroup.coe_norm, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
V' : AddSubgroup V
x : ↥V'
⊢ norm (E := V) ((incl V' : (a : ↥V') → V) x : V) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₂)
rw₂ 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₂)
⊢ v ∈ f.ker ↔ Eq.{u_4 + 1} (α := V₂) ((f : (a : V₁) → V₂) v : V₂) (0 : V₂)

Tactic:
rw [ker, f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]

Premises used: NormedAddGroupHom.coe_toAddMonoidHom, NormedAddGroupHom.ker, AddMonoidHom.mem_ker
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃)
rw₃ rw₄ : Eq.{u_5 + 1} (α := V₃) 0 0
⊢ Membership.mem (α := V₂) g.ker ((f : (a : V₁) → V₂) v : V₂)

Tactic:
rw [g.mem_ker, ← comp_apply g f, h, zero_apply]

Premises used: NormedAddGroupHom.mem_ker, NormedAddGroupHom.zero_apply, NormedAddGroupHom.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.Hom
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 w : V₁
⊢ Subtype.mk (p := fun (x : V₂) ↦ x ∈ g.ker) ((f : (a : V₁) → V₂) (v + w)) ⋯ =
    HAdd.hAdd (α := ↥g.ker) (β := ↥g.ker)
      (Subtype.mk (p := fun (x : V₂) ↦ x ∈ g.ker) ((f : (a : V₁) → V₂) v) ⋯ : ↥g.ker)
      (Subtype.mk (p := fun (x : V₂) ↦ x ∈ g.ker) ((f : (a : V₁) → V₂) w) ⋯ : ↥g.ker)

Tactic:
simp only [map_add, AddMemClass.mk_add_mk]

Premises used: map_add, AddMemClass.mk_add_mk
-- Module: Mathlib.Analysis.Normed.Group.Hom
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
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₂)
⊢ (incl g.ker).comp (lift f g h) = f

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
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
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:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
h :
  ∀ (x : V₁),
    Membership.mem (γ := AddSubgroup V₁) (ker.{u_3, u_4} (V₂ := V₂) 0) x ↔ Membership.mem (γ := AddSubgroup V₁) ⊤ x
⊢ Eq.{u_3 + 1} (α := AddSubgroup V₁) (ker.{u_3, u_4} (V₂ := V₂) 0) ⊤

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
x : V₁
⊢ Membership.mem (γ := AddSubgroup V₁) (ker.{u_3, u_4} (V₂ := V₂) 0) x ↔ Membership.mem (γ := AddSubgroup V₁) ⊤ x

Tactic:
simp [mem_ker]

Premises used: NormedAddGroupHom.mem_ker
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ (↑f.ker : Set V₁) = Set.preimage (β := V₂) (⇑f : (a : V₁) → V₂) {0}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
V₂ : Type u_6
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ IsClosed (↑f.ker : Set V₁)

Tactic:
f.coe_ker ▸ IsClosed.preimage f.continuous (T1Space.t1 0)

Premises used: T1Space.t1, Eq.rec, NormedAddGroupHom.coe_ker, IsClosed.preimage, OfNat.ofNat, Eq.symm, NormedAddGroupHom.continuous
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₂
⊢ v ∈ f.range ↔ ∃ (w : V₁), (f : (a : V₁) → V₂) w = v

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ Membership.mem (α := V₂) f.range ((f : (a : V₁) → V₂) v : V₂)

Tactic:
⟨v, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
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₃
rw : (g.comp f).toAddMonoidHom.range = (g.toAddMonoidHom.comp f.toAddMonoidHom).range
⊢ (g.comp f).toAddMonoidHom.range = AddSubgroup.map g.toAddMonoidHom f.toAddMonoidHom.range

Tactic:
rw [AddMonoidHom.map_range]

Premises used: AddMonoidHom.map_range
-- Module: Mathlib.Analysis.Normed.Group.Hom
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 = (g.toAddMonoidHom.comp f.toAddMonoidHom).range

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
h : ∀ (x : V₁), x ∈ (incl s).range ↔ x ∈ s
⊢ (incl s).range = s

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.Hom
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
rw : Membership.mem (α := V₁) s (((incl s).toAddMonoidHom : (a : ↥s) → V₁) y : V₁)
⊢ x ∈ s

Tactic:
rw [← hy]
-- Module: Mathlib.Analysis.Normed.Group.Hom
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
⊢ Membership.mem (α := V₁) s (((incl s).toAddMonoidHom : (a : ↥s) → V₁) y : V₁)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
hx : x ∈ s
⊢ ((incl s).toAddMonoidHom : (a : ↥s) → V₁) (Subtype.mk (p := fun (x : V₁) ↦ x ∈ s) x hx) = x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
⊢ x ∈ (incl s).range ↔ x ∈ s

Tactic:
exact ⟨fun ⟨y, hy⟩ => by rw [← hy]; simp, fun hx => ⟨⟨x, hx⟩, by simp⟩⟩
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
simp : f.toAddMonoidHom.range = f.range
⊢ range (V₁ := ↥⊤) (f.comp (incl ⊤)) = f.range

Tactic:
simp [comp_range, incl_range, ← AddMonoidHom.range_eq_map]

Premises used: NormedAddGroupHom.incl_range, AddMonoidHom.range_eq_map, NormedAddGroupHom.comp_range
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ f.toAddMonoidHom.range = f.range

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
⊢ f.NormNoninc ↔ ‖f‖ ≤ 1

Tactic:
⟨fun h => ?_, fun h => fun v => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Normed.Group.Hom
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
refine_2 : ∀ (h : ‖f‖ ≤ 1) (v : V), norm.{u_2} (E := W) ((f : (a : V) → W) v : W) ≤ ‖v‖
⊢ f.NormNoninc ↔ ‖f‖ ≤ 1

Tactic:
refine ⟨fun h => ?_, fun h => fun v => ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Hom
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

Tactic:
opNorm_le_bound _ zero_le_one fun v => ?_

Premises used: NormedAddGroupHom.opNorm_le_bound, zero_le_one
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
refine_1 : ∀ (v : V), norm.{u_2} (E := W) ((f : (a : V) → W) v : W) ≤ 1 * ‖v‖
⊢ ‖f‖ ≤ 1

Tactic:
refine opNorm_le_bound _ zero_le_one fun v => ?_

Premises used: NormedAddGroupHom.opNorm_le_bound, zero_le_one
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
v : V
⊢ norm.{u_2} (E := W) ((f : (a : V) → W) v : W) ≤ 1 * ‖v‖

Tactic:
simpa [one_mul] using h v

Premises used: one_mul