awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
refine : ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ 1
⊢ (Hom.hom (explicitCokernelDesc cond)).NormNoninc

Tactic:
refine NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 ?_

Premises used: Iff.mpr, NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ (↑1 : ℝ)

Tactic:
explicitCokernelDesc_norm_le_of_norm_le cond 1
      (NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hg)

Premises used: NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one, Iff.mp, SemiNormedGrp.explicitCokernelDesc_norm_le_of_norm_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ (↑1 : ℝ)

Tactic:
exact
    explicitCokernelDesc_norm_le_of_norm_le cond 1
      (NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hg)

Premises used: NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one, Iff.mp, SemiNormedGrp.explicitCokernelDesc_norm_le_of_norm_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
rw : g ≫ h = explicitCokernelπ f ≫ 0
⊢ explicitCokernelDesc cond ≫ h = 0

Tactic:
rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]

Premises used: CategoryTheory.Category.assoc, SemiNormedGrp.explicitCokernelπ, SemiNormedGrp.explicitCokernelπ_desc, CategoryTheory.cancel_epi
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ g ≫ h = explicitCokernelπ f ≫ 0

Tactic:
simp [cond2]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ ‖explicitCokernelDesc w‖ ≤ ‖g‖

Tactic:
explicitCokernelDesc_norm_le_of_norm_le w ‖g‖₊ le_rfl

Premises used: le_rfl, NNNorm.nnnorm, NormedAddGroupHom.opNorm, SemiNormedGrp.explicitCokernelDesc_norm_le_of_norm_le, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom = cokernel.π f

Tactic:
simp [explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]

Premises used: SemiNormedGrp.explicitCokernelπ, SemiNormedGrp.explicitCokernelIso, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f

Tactic:
simp [explicitCokernelπ, explicitCokernelIso]

Premises used: SemiNormedGrp.explicitCokernelπ, SemiNormedGrp.explicitCokernelIso
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h :
  explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w
⊢ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w

Tactic:
ext1
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w

Tactic:
simp [explicitCokernelDesc, explicitCokernelπ, explicitCokernelIso,
    IsColimit.coconePointUniqueUpToIso]

Premises used: SemiNormedGrp.explicitCokernelπ, SemiNormedGrp.explicitCokernelIso, SemiNormedGrp.explicitCokernelDesc, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
A B C D : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
⊢ fab ≫ fbd ≫ explicitCokernelπ fcd = 0

Tactic:
simp [reassoc_of% h]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
simp :
  (explicitCokernelπ fab ≫ explicitCokernelDesc condb) ≫ g =
    (explicitCokernelπ fab ≫ explicitCokernelDesc ⋯) ≫ explicitCokernelDesc condd
⊢ explicitCokernelDesc condb ≫ g = explicitCokernelDesc ⋯ ≫ explicitCokernelDesc condd

Tactic:
simp only [← Category.assoc, ← cancel_epi (explicitCokernelπ fab)]

Premises used: CategoryTheory.Category.assoc, SemiNormedGrp.explicitCokernelπ, CategoryTheory.cancel_epi
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
A B C D B' D' : SemiNormedGrp
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
fbb' : B ⟶ B'
fdd' : D ⟶ D'
condb : fab ≫ fbb' = 0
condd : fcd ≫ fdd' = 0
g : B' ⟶ D'
h' : fbb' ≫ g = fbd ≫ fdd'
⊢ (explicitCokernelπ fab ≫ explicitCokernelDesc condb) ≫ g =
    (explicitCokernelπ fab ≫ explicitCokernelDesc ⋯) ≫ explicitCokernelDesc condd

Tactic:
simp [Category.assoc, explicitCokernelπ_desc, h']

Premises used: CategoryTheory.Category.assoc, SemiNormedGrp.explicitCokernelπ_desc
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp
f₁ f₂ : M ⟶ N
h :
  ∀ (x : M.carrier),
    Eq (α := N.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) f₁ :
            (a : M.carrier) → N.carrier)
          x :
        N.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) f₂ :
            (a : M.carrier) → N.carrier)
          x :
        N.carrier)
⊢ f₁ = f₂

Tactic:
ConcreteCategory.ext_apply h

Premises used: CategoryTheory.ConcreteCategory.ext_apply
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M : SemiNormedGrp
⊢ Hom.hom (𝟙 M) = NormedAddGroupHom.id M.carrier

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.id, rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M : SemiNormedGrp
r : M.carrier
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) (𝟙 M) :
        (a : M.carrier) → M.carrier)
      r =
    r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N O : SemiNormedGrp
f : M ⟶ N
g : N ⟶ O
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.comp, rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N O : SemiNormedGrp
f : M ⟶ N
g : N ⟶ O
r : M.carrier
⊢ Eq (α := O.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (f ≫ g) :
          (a : M.carrier) → O.carrier)
        r :
      O.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) g :
          (a : N.carrier) → O.carrier)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier)
                (CC := carrier) f :
              (a : M.carrier) → N.carrier)
            r :
          N.carrier) :
      O.carrier)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: SemiNormedGrp.Hom.ext
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : Type u
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp
f : M ⟶ N
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M : Type u
inst : SeminormedAddCommGroup M
⊢ ofHom (NormedAddGroupHom.id M) = 𝟙 { carrier := M, str := inst : SemiNormedGrp.{u} }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N O : Type u
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
inst_2 : SeminormedAddCommGroup O
f : NormedAddGroupHom M N
g : NormedAddGroupHom N O
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : Type u
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
r : M
⊢ Eq (α := { carrier := N, str := inst_1 }.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (ofHom f) :
          (a : { carrier := M, str := inst }.carrier) → { carrier := N, str := inst_1 }.carrier)
        r :
      { carrier := N, str := inst_1 }.carrier)
    ((f : (a : M) → N) r : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp
e : M ≅ N
r : M.carrier
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) e.inv :
        (a : N.carrier) → M.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) e.hom :
            (a : M.carrier) → N.carrier)
          r :
        N.carrier) =
    r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp
e : M ≅ N
s : N.carrier
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) e.hom :
        (a : M.carrier) → N.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) e.inv :
            (a : N.carrier) → M.carrier)
          s :
        M.carrier) =
    s

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : Type u
inst : SeminormedAddCommGroup V
⊢ { carrier := V, str := inst : SemiNormedGrp.{u} }.carrier = V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
⊢ Eq (α := (a : V.carrier) → V.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) (𝟙 V)) :
      (a : V.carrier) → V.carrier)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N K : SemiNormedGrp
f : M ⟶ N
g : N ⟶ K
⊢ Eq (α := (a : M.carrier) → K.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) (f ≫ g)) :
      (a : M.carrier) → K.carrier)
    (Function.comp (β := N.carrier)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) g) :
        (a : N.carrier) → K.carrier)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) f) :
        (a : M.carrier) → N.carrier))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
⊢ Eq.{u_1 + 1} (α := NormedAddGroupHom V.carrier W.carrier) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
x : V.carrier
⊢ Eq (α := W.carrier)
    ((@ConcreteCategory.hom _ instLargeCategory
            (fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) carrier _ _ V W 0 :
          (a : V.carrier) → W.carrier)
        x :
      W.carrier)
    (0 : W.carrier)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
⊢ Limits.IsZero V

Tactic:
⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩

Premises used: Unique.mk, Nonempty.intro, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
refine_1 : ∀ (X : SemiNormedGrp.{u_1}) (f : V ⟶ X), f = default
refine_2 : ∀ (X : SemiNormedGrp.{u_1}) (f : X ⟶ V), f = default
⊢ Limits.IsZero V

Tactic:
refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : V ⟶ X
refine_1 :
  ∀ (x : V.carrier),
    Eq (α := X.carrier) ((Hom.hom f : (a : V.carrier) → X.carrier) x : X.carrier)
      ((Hom.hom default : (a : V.carrier) → X.carrier) x : X.carrier)
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ x = 0

Tactic:
have : x = 0 := Subsingleton.elim _ _
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ Eq (α := X.carrier) ((Hom.hom f : (a : V.carrier) → X.carrier) x : X.carrier)
    ((Hom.hom default : (a : V.carrier) → X.carrier) x : X.carrier)

Tactic:
simp only [this, map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : X ⟶ V
refine_2 :
  ∀ (x : X.carrier),
    Eq (α := V.carrier) ((Hom.hom f : (a : X.carrier) → V.carrier) x : V.carrier)
      ((Hom.hom default : (a : X.carrier) → V.carrier) x : V.carrier)
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : X ⟶ V
x : X.carrier
⊢ Eq (α := V.carrier) ((Hom.hom f : (a : X.carrier) → V.carrier) x : V.carrier)
    ((Hom.hom default : (a : X.carrier) → V.carrier) x : V.carrier)

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
⊢ Limits.HasZeroObject SemiNormedGrp

Tactic:
⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩

Premises used: CategoryTheory.Limits.HasZeroObject.mk, SemiNormedGrp.isZero_of_subsingleton, SemiNormedGrp.of, PUnit, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
a :
  ∀ (x : V.carrier),
    norm (E := W.carrier)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier)
                (CC := carrier) i.hom :
              (a : V.carrier) → W.carrier)
            x :
          W.carrier) =
      ‖x‖
⊢ Isometry (α := V.carrier) (β := W.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) i.hom) :
      (a : V.carrier) → W.carrier)

Tactic:
apply AddMonoidHomClass.isometry_of_norm

Premises used: AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
a : ‖v‖ ≤ norm (E := W.carrier) ((Hom.hom i.hom : (a : V.carrier) → W.carrier) v : W.carrier)
⊢ norm (E := W.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) i.hom :
            (a : V.carrier) → W.carrier)
          v :
        W.carrier) =
    ‖v‖

Tactic:
apply le_antisymm (h1 v)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
rw :
  ‖v‖ =
    norm (E := V.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) (i.hom ≫ i.inv) :
            (a : V.carrier) → V.carrier)
          v :
        V.carrier)
rw₁ :
  ‖v‖ =
    norm (E := V.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) (𝟙 V) :
            (a : V.carrier) → V.carrier)
          v :
        V.carrier)
rw₂ rw₃ : ‖v‖ = ‖v‖
⊢ ‖v‖ =
    norm (E := V.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) i.inv :
            (a : W.carrier) → V.carrier)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier)
                  (CC := carrier) i.hom :
                (a : V.carrier) → W.carrier)
              v :
            W.carrier) :
        V.carrier)

Tactic:
rw [← comp_apply, Iso.hom_inv_id, id_apply]

Premises used: SemiNormedGrp.id_apply, CategoryTheory.Iso.hom_inv_id, SemiNormedGrp.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ norm (E := V.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) i.inv :
            (a : W.carrier) → V.carrier)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier)
                  (CC := carrier) i.hom :
                (a : V.carrier) → W.carrier)
              v :
            W.carrier) :
        V.carrier) ≤
    norm (E := W.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) i.hom :
            (a : V.carrier) → W.carrier)
          v :
        W.carrier)

Tactic:
h2 _
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
by :
  ‖v‖ =
    norm (E := V.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
              carrier) i.inv :
            (a : W.carrier) → V.carrier)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u_1}) ↦ NormedAddGroupHom x1.carrier x2.carrier)
                  (CC := carrier) i.hom :
                (a : V.carrier) → W.carrier)
              v :
            W.carrier) :
        V.carrier)
⊢ ‖v‖ ≤ norm (E := W.carrier) ((Hom.hom i.hom : (a : V.carrier) → W.carrier) v : W.carrier)

Tactic:
calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := h2 _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
⊢ Hom.hom (f + g) = Hom.hom f + Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
f : V ⟶ W
⊢ Hom.hom (-f) = -Hom.hom f

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
⊢ Hom.hom (f - g) = Hom.hom f - Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
n : ℕ
f : V ⟶ W
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp
n : ℤ
f : V ⟶ W
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : Type u
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
i : f.NormNoninc
x : { carrier := M, str := inst }.carrier
⊢ Eq (α := { carrier := N, str := inst_1 }.carrier)
    (((↑(Hom.hom (mkHom f i)) :
            NormedAddGroupHom { carrier := M, str := inst }.carrier { carrier := N, str := inst_1 }.carrier) :
          (a : { carrier := M, str := inst }.carrier) → { carrier := N, str := inst_1 }.carrier)
        x :
      { carrier := N, str := inst_1 }.carrier)
    ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
f₁ f₂ : M ⟶ N
h :
  ∀ (x : M.carrier),
    Eq (α := N.carrier)
      (((↑(Hom.hom f₁) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier) x : N.carrier)
      (((↑(Hom.hom f₂) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier) x : N.carrier)
⊢ f₁ = f₂

Tactic:
ConcreteCategory.ext_apply h

Premises used: CategoryTheory.ConcreteCategory.ext_apply
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M : SemiNormedGrp₁
⊢ (↑(Hom.hom (𝟙 M)) : NormedAddGroupHom M.carrier M.carrier) = NormedAddGroupHom.id M.carrier

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.id, rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M : SemiNormedGrp₁
r : M.carrier
⊢ ((↑(Hom.hom (𝟙 M)) : NormedAddGroupHom M.carrier M.carrier) : (a : M.carrier) → M.carrier) r = r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N O : SemiNormedGrp₁
f : M ⟶ N
g : N ⟶ O
⊢ (↑(Hom.hom (f ≫ g)) : NormedAddGroupHom M.carrier O.carrier) =
    (↑(Hom.hom g) : NormedAddGroupHom N.carrier O.carrier).comp (↑(Hom.hom f) : NormedAddGroupHom M.carrier N.carrier)

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.comp, rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N O : SemiNormedGrp₁
f : M ⟶ N
g : N ⟶ O
r : M.carrier
⊢ Eq (α := O.carrier)
    (((↑(Hom.hom (f ≫ g)) : NormedAddGroupHom M.carrier O.carrier) : (a : M.carrier) → O.carrier) r : O.carrier)
    (((↑(Hom.hom g) : NormedAddGroupHom N.carrier O.carrier) : (a : N.carrier) → O.carrier)
        (((↑(Hom.hom f) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier) r : N.carrier) :
      O.carrier)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext (congr_arg Subtype.val hf)

Premises used: SemiNormedGrp₁.Hom.ext, congr_arg, Subtype.val
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : Type u
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : f.NormNoninc
⊢ (↑(Hom.hom (mkHom f hf)) :
      NormedAddGroupHom { carrier := M, str := inst }.carrier { carrier := N, str := inst_1 }.carrier) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
f : M ⟶ N
⊢ mkHom (↑(Hom.hom f) : NormedAddGroupHom M.carrier N.carrier) ⋯ = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M : Type u
inst : SeminormedAddCommGroup M
⊢ mkHom (NormedAddGroupHom.id M) ⋯ = 𝟙 { carrier := M, str := inst : SemiNormedGrp₁.{u} }

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.id, rfl