awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
c : Fork f g
⊢ Eq (α := NormedAddGroupHom c.pt.carrier W.carrier)
    ((((NormedAddGroupHom.compHom :
                (a : NormedAddGroupHom V.carrier W.carrier) →
                  NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier)
              (Hom.hom f) :
            NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier) :
          (a : NormedAddGroupHom c.pt.carrier V.carrier) → NormedAddGroupHom c.pt.carrier W.carrier)
        (Hom.hom c.ι) :
      NormedAddGroupHom c.pt.carrier W.carrier)
    ((((NormedAddGroupHom.compHom :
                (a : NormedAddGroupHom V.carrier W.carrier) →
                  NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier)
              (Hom.hom g) :
            NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier) :
          (a : NormedAddGroupHom c.pt.carrier V.carrier) → NormedAddGroupHom c.pt.carrier W.carrier)
        (Hom.hom c.ι) :
      NormedAddGroupHom c.pt.carrier W.carrier)

Tactic:
exact congr_arg Hom.hom c.condition

Premises used: SemiNormedGrp.Hom.hom, congr_arg, CategoryTheory.Limits.Fork.condition
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g_1 : V ⟶ W
this :
  ∀ (c : Fork f g_1),
    Eq (α := NormedAddGroupHom c.pt.carrier W.carrier)
      ((((NormedAddGroupHom.compHom :
                  (a : NormedAddGroupHom V.carrier W.carrier) →
                    NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier)
                (Hom.hom (f - g_1)) :
              NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier) :
            (a : NormedAddGroupHom c.pt.carrier V.carrier) → NormedAddGroupHom c.pt.carrier W.carrier)
          (Hom.hom c.ι) :
        NormedAddGroupHom c.pt.carrier W.carrier)
      (0 : NormedAddGroupHom c.pt.carrier W.carrier)
c : Fork f g_1
g : c.pt ⟶ (fork f g_1).pt
h : g ≫ (fork f g_1).ι = c.ι
hf :
  ∀ (x : c.pt.carrier),
    Eq (α := (fork f g_1).pt.carrier)
      ((Hom.hom g : (a : c.pt.carrier) → (fork f g_1).pt.carrier) x : (fork f g_1).pt.carrier)
      ((Hom.hom ((fun (c : Fork f g_1) ↦ ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g_1)) ⋯)) c) :
            (a : c.pt.carrier) → (fork f g_1).pt.carrier)
          x :
        (fork f g_1).pt.carrier)
⊢ g = (fun (c : Fork f g_1) ↦ ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g_1)) ⋯)) c

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g_1 : V ⟶ W
this :
  ∀ (c : Fork f g_1),
    Eq (α := NormedAddGroupHom c.pt.carrier W.carrier)
      ((((NormedAddGroupHom.compHom :
                  (a : NormedAddGroupHom V.carrier W.carrier) →
                    NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier)
                (Hom.hom (f - g_1)) :
              NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier) :
            (a : NormedAddGroupHom c.pt.carrier V.carrier) → NormedAddGroupHom c.pt.carrier W.carrier)
          (Hom.hom c.ι) :
        NormedAddGroupHom c.pt.carrier W.carrier)
      (0 : NormedAddGroupHom c.pt.carrier W.carrier)
c : Fork f g_1
g : c.pt ⟶ (fork f g_1).pt
h : g ≫ (fork f g_1).ι = c.ι
x : c.pt.carrier
hf :
  Eq (α := (fork f g_1).pt.carrier)
    ((Hom.hom g : (a : c.pt.carrier) → (fork f g_1).pt.carrier) x : (fork f g_1).pt.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom (g ≫ (fork f g_1).ι)) (Hom.hom f - Hom.hom g_1) ⋯)) :
          (a : c.pt.carrier) → (fork f g_1).pt.carrier)
        x :
      (fork f g_1).pt.carrier)
⊢ Eq (α := (fork f g_1).pt.carrier)
    ((Hom.hom g : (a : c.pt.carrier) → (fork f g_1).pt.carrier) x : (fork f g_1).pt.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom f - Hom.hom g_1) ⋯)) :
          (a : c.pt.carrier) → (fork f g_1).pt.carrier)
        x :
      (fork f g_1).pt.carrier)

Tactic:
simp_rw [← h]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g_1 : V ⟶ W
this :
  ∀ (c : Fork f g_1),
    Eq (α := NormedAddGroupHom c.pt.carrier W.carrier)
      ((((NormedAddGroupHom.compHom :
                  (a : NormedAddGroupHom V.carrier W.carrier) →
                    NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier)
                (Hom.hom (f - g_1)) :
              NormedAddGroupHom c.pt.carrier V.carrier →+ NormedAddGroupHom c.pt.carrier W.carrier) :
            (a : NormedAddGroupHom c.pt.carrier V.carrier) → NormedAddGroupHom c.pt.carrier W.carrier)
          (Hom.hom c.ι) :
        NormedAddGroupHom c.pt.carrier W.carrier)
      (0 : NormedAddGroupHom c.pt.carrier W.carrier)
c : Fork f g_1
g : c.pt ⟶ (fork f g_1).pt
h : g ≫ (fork f g_1).ι = c.ι
x : c.pt.carrier
⊢ Eq (α := (fork f g_1).pt.carrier)
    ((Hom.hom g : (a : c.pt.carrier) → (fork f g_1).pt.carrier) x : (fork f g_1).pt.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom (g ≫ (fork f g_1).ι)) (Hom.hom f - Hom.hom g_1) ⋯)) :
          (a : c.pt.carrier) → (fork f g_1).pt.carrier)
        x :
      (fork f g_1).pt.carrier)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
⊢ HasEqualizers SemiNormedGrp

Tactic:
@hasEqualizers_of_hasLimit_parallelPair SemiNormedGrp _ fun {_ _ f g} =>
    SemiNormedGrp.hasLimit_parallelPair f g

Premises used: CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair, SemiNormedGrp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ f ≫ ofHom (Hom.hom f).range.normedMk = 0 ≫ ofHom (Hom.hom f).range.normedMk

Tactic:
aesop
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
b : X.carrier
change :
  Eq (α := s.pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (f ≫ Cofork.π s) :
          (a : X.carrier) → s.pt.carrier)
        b :
      s.pt.carrier)
    (0 : s.pt.carrier)
⊢ Eq (α := carrier s.1)
    ((Hom.hom (Cofork.π s) : (a : Y.carrier) → s.1.carrier)
        (((Hom.hom f).toAddMonoidHom : (a : X.carrier) → Y.carrier) b : Y.carrier) :
      carrier s.1)
    (0 : carrier s.1)

Tactic:
change (f ≫ s.π) b = 0

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
b : X.carrier
⊢ Eq (α := s.pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (f ≫ Cofork.π s) :
          (a : X.carrier) → s.pt.carrier)
        b :
      s.pt.carrier)
    (0 : s.pt.carrier)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
hf :
  ∀ (x : Y.carrier),
    Eq (α := s.pt.carrier)
      ((Hom.hom ((cokernelCocone f).π ≫ cokernelLift f s) : (a : Y.carrier) → s.pt.carrier) x : s.pt.carrier)
      ((Hom.hom (Cofork.π s) : (a : Y.carrier) → s.pt.carrier) x : s.pt.carrier)
⊢ (cokernelCocone f).π ≫ cokernelLift f s = Cofork.π s

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
x : Y.carrier
hf :
  ∀ s_1 ∈ (Hom.hom f).range,
    Eq (α := s.pt.carrier) ((Hom.hom (Cofork.π s) : (a : Y.carrier) → s.pt.carrier) s_1 : s.pt.carrier)
      (0 : s.pt.carrier)
⊢ Eq (α := s.pt.carrier)
    ((Hom.hom ((cokernelCocone f).π ≫ cokernelLift f s) : (a : Y.carrier) → s.pt.carrier) x : s.pt.carrier)
    ((Hom.hom (Cofork.π s) : (a : Y.carrier) → s.pt.carrier) x : s.pt.carrier)

Tactic:
apply NormedAddGroupHom.lift_mk f.hom.range

Premises used: NormedAddGroupHom.lift_mk, NormedAddGroupHom.range, SemiNormedGrp.Hom.hom
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
x : Y.carrier
b : X.carrier
hf :
  Eq (α := s.pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (f ≫ Cofork.π s) :
          (a : X.carrier) → s.pt.carrier)
        b :
      s.pt.carrier)
    (0 : s.pt.carrier)
⊢ Eq (α := s.pt.carrier)
    ((Hom.hom (Cofork.π s) : (a : Y.carrier) → s.pt.carrier)
        (((Hom.hom f).toAddMonoidHom : (a : X.carrier) → Y.carrier) b : Y.carrier) :
      s.pt.carrier)
    (0 : s.pt.carrier)

Tactic:
change (f ≫ s.π) b = 0

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
x : Y.carrier
b : X.carrier
⊢ Eq (α := s.pt.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (f ≫ Cofork.π s) :
          (a : X.carrier) → s.pt.carrier)
        b :
      s.pt.carrier)
    (0 : s.pt.carrier)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
⊢ HasCokernels SemiNormedGrp

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ g = 0 ≫ g

Tactic:
simp [w]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ Function.Surjective (α := Y.carrier) (β := (explicitCokernel f).carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
          carrier) (explicitCokernelπ f)) :
      (a : Y.carrier) → (explicitCokernel f).carrier)

Tactic:
Quot.mk_surjective

Premises used: Quotient, Quot.mk_surjective
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ (parallelPair f 0).map WalkingParallelPairHom.left ≫ (cokernelCocone f).ι.app WalkingParallelPair.one =
    (cokernelCocone f).ι.app WalkingParallelPair.zero

Tactic:
(cokernelCocone f).w WalkingParallelPairHom.left

Premises used: SemiNormedGrp.cokernelCocone, CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingParallelPairHom.left
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
h :
  (X ⟶ explicitCokernel f) = ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (cokernelCocone f).pt) →
    0 = (cokernelCocone f).ι.app WalkingParallelPair.zero
⊢ f ≫ explicitCokernelπ f = 0

Tactic:
convert! (cokernelCocone f).w WalkingParallelPairHom.left

Premises used: SemiNormedGrp.cokernelCocone, CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingParallelPairHom.left
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
e_1 : (X ⟶ explicitCokernel f) = ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (cokernelCocone f).pt)
⊢ 0 = (cokernelCocone f).ι.app WalkingParallelPair.zero

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
rw :
  Eq (α := (explicitCokernel f).carrier)
    ((@ConcreteCategory.hom _ instLargeCategory
            (fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) carrier _ _ X
            (explicitCokernel f) 0 :
          (a : X.carrier) → (explicitCokernel f).carrier)
        x :
      (explicitCokernel f).carrier)
    (0 : (explicitCokernel f).carrier)
⊢ Eq (α := (explicitCokernel f).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) (CC :=
            carrier) (f ≫ explicitCokernelπ f) :
          (a : X.carrier) → (explicitCokernel f).carrier)
        x :
      (explicitCokernel f).carrier)
    (0 : (explicitCokernel f).carrier)

Tactic:
rw [comp_explicitCokernelπ]

Premises used: SemiNormedGrp.comp_explicitCokernelπ
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ Eq (α := (explicitCokernel f).carrier)
    ((@ConcreteCategory.hom _ instLargeCategory
            (fun (x1 x2 : SemiNormedGrp.{u}) ↦ NormedAddGroupHom x1.carrier x2.carrier) carrier _ _ X
            (explicitCokernel f) 0 :
          (a : X.carrier) → (explicitCokernel f).carrier)
        x :
      (explicitCokernel f).carrier)
    (0 : (explicitCokernel f).carrier)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc w = g

Tactic:
(isColimitCokernelCocone f).fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, SemiNormedGrp.isColimitCokernelCocone
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
x : Y.carrier
rw 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)
⊢ 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)

Tactic:
rw [explicitCokernelπ_desc]

Premises used: SemiNormedGrp.explicitCokernelπ_desc
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ f ≫ g = 0 ≫ g

Tactic:
simp [w]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
x : ∀ (j : WalkingParallelPair), (cokernelCocone f).ι.app j ≫ e = (Cofork.ofπ g ⋯).ι.app j
⊢ e = explicitCokernelDesc w

Tactic:
apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))

Premises used: SemiNormedGrp.isColimitCokernelCocone, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ 0 = f ≫ g

Tactic:
w.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
h :
  ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g ⋯).pt) = (X ⟶ Z) →
    (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = 0
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

Tactic:
convert! w.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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_1 : ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g ⋯).pt) = (X ⟶ Z)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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.one ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
he
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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.one ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
exact he
-- 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
rw : (f ≫ g) ≫ h = 0
rw₁ : Eq (α := X ⟶ W) (0 ≫ h) 0
rw₂ rw₃ : Eq.{u + 1} (α := X ⟶ W) 0 0
⊢ f ≫ g ≫ h = 0

Tactic:
rw [← CategoryTheory.Category.assoc, cond, Limits.zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp
-- 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
⊢ explicitCokernelDesc cond ≫ h = explicitCokernelDesc (g := g ≫ h) ⋯

Tactic:
explicitCokernelDesc_unique _ _ ?_

Premises used: SemiNormedGrp.explicitCokernelDesc_unique
-- 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
refine : explicitCokernelπ f ≫ explicitCokernelDesc cond ≫ h = g ≫ h
⊢ explicitCokernelDesc cond ≫ h = explicitCokernelDesc (g := g ≫ h) ⋯

Tactic:
refine explicitCokernelDesc_unique _ _ ?_

Premises used: SemiNormedGrp.explicitCokernelDesc_unique
-- 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
rw : (explicitCokernelπ f ≫ explicitCokernelDesc cond) ≫ h = g ≫ h
rw₁ rw₂ : g ≫ h = g ≫ h
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond ≫ h = g ≫ h

Tactic:
rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]

Premises used: CategoryTheory.Category.assoc, SemiNormedGrp.explicitCokernelπ_desc
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
⊢ Eq.{u + 1} (α := explicitCokernel f ⟶ Z) (explicitCokernelDesc (g := 0) ⋯) 0

Tactic:
Eq.symm <| explicitCokernelDesc_unique _ _ CategoryTheory.Limits.comp_zero

Premises used: SemiNormedGrp.explicitCokernelDesc_unique, CategoryTheory.Limits.comp_zero, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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₂
⊢ f ≫ g = 0

Tactic:
simp [g]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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₂
⊢ f ≫ g = 0

Tactic:
have w : f ≫ g = 0 := by simp [g]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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
he : explicitCokernelπ f ≫ e₂ = g
⊢ e₂ = explicitCokernelDesc w

Tactic:
apply explicitCokernelDesc_unique

Premises used: SemiNormedGrp.explicitCokernelDesc_unique
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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
⊢ explicitCokernelπ f ≫ e₂ = g

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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

Tactic:
have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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
rw : e₁ = explicitCokernelDesc w
⊢ e₁ = e₂

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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
he : explicitCokernelπ f ≫ e₁ = g
⊢ e₁ = explicitCokernelDesc w

Tactic:
apply explicitCokernelDesc_unique

Premises used: SemiNormedGrp.explicitCokernelDesc_unique
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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
⊢ explicitCokernelπ f ≫ e₁ = g

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
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
⊢ explicitCokernelπ f ≫ e₁ = g

Tactic:
exact h
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
left_cancellation :
  ∀ {Z : SemiNormedGrp.{u}} (g h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h
⊢ Epi (explicitCokernelπ f)

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
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)
⊢ g = h

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
Z : SemiNormedGrp
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
x : Y.carrier
left_cancellation 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)
⊢ 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:
rw [H]
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ (Hom.hom (explicitCokernelπ f)).IsQuotient

Tactic:
NormedAddGroupHom.isQuotientQuotient _

Premises used: AddSubgroup.normedMk, NormedAddGroupHom.isQuotientQuotient
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ (Hom.hom (explicitCokernelπ f)).NormNoninc

Tactic:
(isQuotient_explicitCokernelπ f).norm_le

Premises used: NormedAddGroupHom.IsQuotient.norm_le, SemiNormedGrp.isQuotient_explicitCokernelπ, NormedAddGroupHom.NormNoninc
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
c : ℝ≥0
h : ‖g‖ ≤ (↑c : ℝ)
⊢ ‖explicitCokernelDesc w‖ ≤ (↑c : ℝ)

Tactic:
NormedAddGroupHom.lift_norm_le _ _ _ h

Premises used: NormedAddGroupHom.lift, NormedAddGroupHom.lift_norm_le
-- 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)).NormNoninc

Tactic:
NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 ?_

Premises used: Iff.mpr, NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one