awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
x : Y.carrier
⊢ Eq (α := Z.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (explicitCokernelπ f ≫ explicitCokernelDesc cond) :
          (a : Y.carrier) → Z.carrier)
        x :
      Z.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) g :
          (a : Y.carrier) → Z.carrier)
        x :
      Z.carrier)
have rw : Eq (α := Z.carrier)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) g :
        (a : Y.carrier) → Z.carrier)
      x :
    Z.carrier)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) g :
        (a : Y.carrier) → Z.carrier)
      x :
    Z.carrier)
Tactic: rw [explicitCokernelπ_desc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ e = explicitCokernelDesc w
have x : ∀ (j : WalkingParallelPair), (cokernelCocone f).ι.app j ≫ e = (Cofork.ofπ g sorry).ι.app j
Tactic: apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.zero
have h : ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g sorry).pt) = (X ⟶ Z) →
  (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = 0
Tactic: convert! w.symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
⊢ f ≫ g ≫ h = 0
have rw : (f ≫ g) ≫ h = 0
Tactic: rw [← CategoryTheory.Category.assoc, cond, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
rw : (f ≫ g) ≫ h = 0
⊢ f ≫ g ≫ h = 0
have rw₁ : Eq (α := X ⟶ W) (0 ≫ h) 0
Tactic: rw [← CategoryTheory.Category.assoc, cond, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
rw : (f ≫ g) ≫ h = 0
rw₁ : Eq (α := X ⟶ W) (0 ≫ h) 0
⊢ f ≫ g ≫ h = 0
have rw₂ : Eq.{u + 1} (α := X ⟶ W) 0 0
Tactic: rw [← CategoryTheory.Category.assoc, cond, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
⊢ explicitCokernelDesc cond ≫ h = explicitCokernelDesc (g := g ≫ h) ⋯
have refine : explicitCokernelπ f ≫ explicitCokernelDesc cond ≫ h = g ≫ h
Tactic: refine explicitCokernelDesc_unique _ _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond ≫ h = g ≫ h
have rw : (explicitCokernelπ f ≫ explicitCokernelDesc cond) ≫ h = g ≫ h
Tactic: rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
rw : (explicitCokernelπ f ≫ explicitCokernelDesc cond) ≫ h = g ≫ h
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond ≫ h = g ≫ h
have rw₁ : g ≫ h = g ≫ h
Tactic: rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (hypothesis)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂
have w : f ≫ g = 0
Tactic: have w : f ≫ g = 0 := by simp [g]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₂ = explicitCokernelDesc w
have he : explicitCokernelπ f ≫ e₂ = g
Tactic: apply explicitCokernelDesc_unique
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (hypothesis)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₁ = e₂
have this : e₂ = explicitCokernelDesc w
Tactic: have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = e₂
have rw : e₁ = explicitCokernelDesc w
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ Epi (explicitCokernelπ f)
have left_cancellation : ∀ {Z : SemiNormedGrp.{u}} (g h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
⊢ g = h
have left_cancellation : ∀ (x : Y.carrier),
  Eq (α := Z.carrier) ((Hom.hom (explicitCokernelπ f ≫ g) : (a : Y.carrier) → Z.carrier) x : Z.carrier)
    ((Hom.hom (explicitCokernelπ f ≫ h) : (a : Y.carrier) → Z.carrier) x : Z.carrier)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
x : Y.carrier
⊢ Eq (α := Z.carrier) ((Hom.hom (explicitCokernelπ f ≫ g) : (a : Y.carrier) → Z.carrier) x : Z.carrier)
    ((Hom.hom (explicitCokernelπ f ≫ h) : (a : Y.carrier) → Z.carrier) x : Z.carrier)
have left_cancellation : Eq (α := Z.carrier) ((Hom.hom (explicitCokernelπ f ≫ h) : (a : Y.carrier) → Z.carrier) x : Z.carrier)
  ((Hom.hom (explicitCokernelπ f ≫ h) : (a : Y.carrier) → Z.carrier) x : Z.carrier)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : (Hom.hom g).NormNoninc
⊢ (Hom.hom (explicitCokernelDesc cond)).NormNoninc
have refine : ‖Hom.hom (explicitCokernelDesc cond)‖ ≤ 1
Tactic: refine NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ explicitCokernelDesc cond ≫ h = 0
have rw : g ≫ h = explicitCokernelπ f ≫ 0
Tactic: rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w
have h : explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
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'
⊢ explicitCokernelDesc condb ≫ g = explicitCokernelDesc ⋯ ≫ explicitCokernelDesc condd
have simp : (explicitCokernelπ fab ≫ explicitCokernelDesc condb) ≫ g =
  (explicitCokernelπ fab ≫ explicitCokernelDesc sorry) ≫ explicitCokernelDesc condd
Tactic: simp only [← Category.assoc, ← cancel_epi (explicitCokernelπ fab)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
⊢ Limits.IsZero V
have refine_1 : ∀ (X : SemiNormedGrp.{u_1}) (f : V ⟶ X), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
refine_1 : ∀ (X : SemiNormedGrp.{u_1}) (f : V ⟶ X), f = default
⊢ Limits.IsZero V
have refine_2 : ∀ (X : SemiNormedGrp.{u_1}) (f : X ⟶ V), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : V ⟶ X
⊢ f = default
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (hypothesis)
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : V ⟶ X
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)
have this : x = 0
Tactic: have : x = 0 := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp
f : X ⟶ V
⊢ f = default
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
⊢ 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)
have 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‖
Tactic: apply AddMonoidHomClass.isometry_of_norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : 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) =
    ‖v‖
have a : ‖v‖ ≤ norm (E := W.carrier) ((Hom.hom i.hom : (a : V.carrier) → W.carrier) v : W.carrier)
Tactic: apply le_antisymm (h1 v)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖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)
have 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)
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
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)
⊢ ‖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)
have 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)
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
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)
⊢ ‖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)
have rw₂ : ‖v‖ = ‖v‖
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖v‖ ≤ norm (E := W.carrier) ((Hom.hom i.hom : (a : V.carrier) → W.carrier) v : W.carrier)
have 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)
Tactic: calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := h2 _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
⊢ ((↑(Hom.hom e.inv) : NormedAddGroupHom N.carrier M.carrier) : (a : N.carrier) → M.carrier)
      (((↑(Hom.hom e.hom) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier) r : N.carrier) =
    r
have rw : ((↑(Hom.hom (e.hom ≫ e.inv)) : NormedAddGroupHom M.carrier M.carrier) : (a : M.carrier) → M.carrier) r = r
Tactic: rw [← comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
⊢ ((↑(Hom.hom e.hom) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier)
      (((↑(Hom.hom e.inv) : NormedAddGroupHom N.carrier M.carrier) : (a : N.carrier) → M.carrier) s : M.carrier) =
    s
have rw : ((↑(Hom.hom (e.inv ≫ e.hom)) : NormedAddGroupHom N.carrier N.carrier) : (a : N.carrier) → N.carrier) s = s
Tactic: rw [← comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
⊢ Limits.IsZero V
have refine_1 : ∀ (X : SemiNormedGrp₁.{u_1}) (f : V ⟶ X), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
refine_1 : ∀ (X : SemiNormedGrp₁.{u_1}) (f : V ⟶ X), f = default
⊢ Limits.IsZero V
have refine_2 : ∀ (X : SemiNormedGrp₁.{u_1}) (f : X ⟶ V), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
⊢ f = default
have refine_1 : ∀ (x : V.carrier),
  Eq (α := X.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
    (((↑(Hom.hom default) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (hypothesis)
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ Eq (α := X.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
    (((↑(Hom.hom default) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
have this : x = 0
Tactic: have : x = 0 := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
⊢ f = default
have refine_2 : ∀ (x : X.carrier),
  Eq (α := V.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom X.carrier V.carrier) : (a : X.carrier) → V.carrier) x : V.carrier)
    (((↑(Hom.hom default) : NormedAddGroupHom X.carrier V.carrier) : (a : X.carrier) → V.carrier) x : V.carrier)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry (α := V.carrier) (β := W.carrier)
    (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier)
have change : Isometry (α := V.carrier) (β := W.carrier)
  (⇑{ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
        map_zero' := sorry, map_add' := sorry } :
    (a : V.carrier) → W.carrier)
Tactic: change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry (α := V.carrier) (β := W.carrier)
    (⇑{ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
          map_zero' := ⋯, map_add' := ⋯ } :
      (a : V.carrier) → W.carrier)
have refine : ∀ (x : V.carrier),
  norm (E := W.carrier)
      (({ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
              map_zero' := sorry, map_add' := sorry : V.carrier →+ W.carrier } :
            (a : V.carrier) → W.carrier)
          x :
        W.carrier) =
    ‖x‖
Tactic: refine AddMonoidHomClass.isometry_of_norm _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ norm (E := W.carrier)
      (({ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
              map_zero' := ⋯, map_add' := ⋯ : V.carrier →+ W.carrier } :
            (a : V.carrier) → W.carrier)
          v :
        W.carrier) =
    ‖v‖
have apply : ‖v‖ ≤ norm (E := W.carrier) ((i.hom.hom' : (a : V.carrier) → W.carrier) v : W.carrier)
Tactic: apply le_antisymm (i.hom.2 v)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
          (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
        V.carrier)
have rw : ‖v‖ =
  norm (E := V.carrier)
    (((↑(Hom.hom (i.hom ≫ i.inv)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v : V.carrier)
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
rw :
  ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom (i.hom ≫ i.inv)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v :
        V.carrier)
⊢ ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
          (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
        V.carrier)
have rw₁ : ‖v‖ =
  norm (E := V.carrier)
    (((↑(Hom.hom (𝟙 V)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v : V.carrier)
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
rw :
  ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom (i.hom ≫ i.inv)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v :
        V.carrier)
rw₁ :
  ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom (𝟙 V)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v : V.carrier)
⊢ ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
          (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
        V.carrier)
have rw₂ : ‖v‖ = ‖v‖
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp (goal)
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ ‖v‖ ≤ norm (E := W.carrier) ((i.hom.hom' : (a : V.carrier) → W.carrier) v : W.carrier)
have by : ‖v‖ =
  norm (E := V.carrier)
    (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
        (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
      V.carrier)
Tactic: calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := i.inv.2 _