[GOAL]
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
⊢ f ≫
      mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
        (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖) =
    0 ≫
      mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
        (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖)
[PROOFSTEP]
ext x
[GOAL]
case w.h
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
x : ↑X
⊢ ↑(f ≫
          mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
            (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖))
      x =
    ↑(0 ≫
          mkHom (AddSubgroup.normedMk (NormedAddGroupHom.range ↑f))
            (_ : ∀ (m : ↑Y), ‖↑(AddSubgroup.normedMk (NormedAddGroupHom.range ↑f)) m‖ ≤ ‖m‖))
      x
[PROOFSTEP]
rw [Limits.zero_comp, comp_apply, SemiNormedGroupCat₁.mkHom_apply, SemiNormedGroupCat₁.zero_apply, ←
  NormedAddGroupHom.mem_ker, f.1.range.ker_normedMk, f.1.mem_range]
[GOAL]
case w.h
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
x : ↑X
⊢ ∃ w, ↑↑f w = ↑f x
[PROOFSTEP]
use x
[GOAL]
case h
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
x : ↑X
⊢ ↑↑f x = ↑f x
[PROOFSTEP]
rfl
[GOAL]
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (cokernelCocone f).pt ⟶ s.pt
[PROOFSTEP]
fconstructor
  -- The lift itself:
[GOAL]
case val
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom ↑(cokernelCocone f).pt ↑s.pt
[PROOFSTEP]
apply NormedAddGroupHom.lift _ s.π.1
[GOAL]
case val
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ ∀ (s_1 : ↑((parallelPair f 0).obj WalkingParallelPair.one)), s_1 ∈ NormedAddGroupHom.range ↑f → ↑↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case val.intro
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom ↑f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case val.intro
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
  -- The lift has norm at most one:
[GOAL]
case property
X Y : SemiNormedGroupCat₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom.NormNoninc
    (NormedAddGroupHom.lift (NormedAddGroupHom.range ↑f) ↑(Cofork.π s)
      (_ :
        ∀ (s_1 : ↑((parallelPair f 0).obj WalkingParallelPair.one)),
          s_1 ∈ NormedAddGroupHom.range ↑f → ↑↑(Cofork.π s) s_1 = 0))
[PROOFSTEP]
exact NormedAddGroupHom.lift_normNoninc _ _ _ s.π.2
[GOAL]
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
⊢ Cofork.π (cokernelCocone f) ≫ cokernelLift f s = Cofork.π s
[PROOFSTEP]
ext
[GOAL]
case w.h
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ↑(Cofork.π (cokernelCocone f) ≫ cokernelLift f s) x✝ = ↑(Cofork.π s) x✝
[PROOFSTEP]
apply NormedAddGroupHom.lift_mk f.1.range
[GOAL]
case w.h.hf
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ∀ (s_1 : ↑Y✝), s_1 ∈ NormedAddGroupHom.range ↑f → ↑↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case w.h.hf.intro
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X✝
⊢ ↑↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom ↑f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case w.h.hf.intro
X✝ Y✝ : SemiNormedGroupCat₁
f : X✝ ⟶ Y✝
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X✝
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
[GOAL]
⊢ HasCokernels SemiNormedGroupCat₁
[PROOFSTEP]
infer_instance
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
⊢ NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f =
    NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g
[PROOFSTEP]
change NormedAddGroupHom V W at f g 
[GOAL]
V W : SemiNormedGroupCat
f g : NormedAddGroupHom ↑V ↑W
⊢ NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f =
    NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g
[PROOFSTEP]
ext v
[GOAL]
case h
V W : SemiNormedGroupCat
f g : NormedAddGroupHom ↑V ↑W
v : ↑(of { x // x ∈ NormedAddGroupHom.ker (f - g) })
⊢ ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f) v =
    ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g) v
[PROOFSTEP]
have : v.1 ∈ (f - g).ker := v.2
[GOAL]
case h
V W : SemiNormedGroupCat
f g : NormedAddGroupHom ↑V ↑W
v : ↑(of { x // x ∈ NormedAddGroupHom.ker (f - g) })
this : ↑v ∈ NormedAddGroupHom.ker (f - g)
⊢ ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ f) v =
    ↑(NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g)) ≫ g) v
[PROOFSTEP]
simpa only [NormedAddGroupHom.incl_apply, Pi.zero_apply, coe_comp, NormedAddGroupHom.coe_zero,
  NormedAddGroupHom.mem_ker, NormedAddGroupHom.coe_sub, Pi.sub_apply, sub_eq_zero] using this
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
c : Fork f g
⊢ ↑(↑NormedAddGroupHom.compHom (f - g)) (Fork.ι c) = 0
[PROOFSTEP]
rw [AddMonoidHom.map_sub, AddMonoidHom.sub_apply, sub_eq_zero]
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
c : Fork f g
⊢ ↑(↑NormedAddGroupHom.compHom f) (Fork.ι c) = ↑(↑NormedAddGroupHom.compHom g) (Fork.ι c)
[PROOFSTEP]
exact c.condition
[GOAL]
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
⊢ g =
    (fun c =>
        NormedAddGroupHom.ker.lift (Fork.ι c) (f - g✝) (_ : ↑(↑NormedAddGroupHom.compHom (f - g✝)) (Fork.ι c) = 0))
      c
[PROOFSTEP]
ext x
[GOAL]
case h
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
x : ↑c.pt
⊢ ↑g x =
    ↑((fun c =>
            NormedAddGroupHom.ker.lift (Fork.ι c) (f - g✝) (_ : ↑(↑NormedAddGroupHom.compHom (f - g✝)) (Fork.ι c) = 0))
          c)
      x
[PROOFSTEP]
dsimp
[GOAL]
case h
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
x : ↑c.pt
⊢ ↑g x =
    ↑(NormedAddGroupHom.ker.lift (Fork.ι c) (f - g✝)
          (_ : ↑(↑NormedAddGroupHom.compHom f) (Fork.ι c) - ↑(↑NormedAddGroupHom.compHom g✝) (Fork.ι c) = 0))
      x
[PROOFSTEP]
simp_rw [← h]
[GOAL]
case h
V W : SemiNormedGroupCat
f g✝ : V ⟶ W
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ Fork.ι (fork f g✝) = Fork.ι c
x : ↑c.pt
⊢ ↑g x =
    ↑(NormedAddGroupHom.ker.lift (g ≫ Fork.ι (fork f g✝)) (f - g✝)
          (_ : NormedAddGroupHom.comp (f - g✝) (g ≫ Fork.ι (fork f g✝)) = 0))
      x
[PROOFSTEP]
rfl
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ f ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f) = 0 ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)
[PROOFSTEP]
ext
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
⊢ ↑(f ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)) x✝ =
    ↑(0 ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)) x✝
[PROOFSTEP]
simp only [comp_apply, Limits.zero_comp]
  -- porting note: `simp` not firing on the below
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
⊢ ↑(f ≫ AddSubgroup.normedMk (NormedAddGroupHom.range f)) x✝ = ↑0 x✝
[PROOFSTEP]
rw [comp_apply, NormedAddGroupHom.zero_apply]
  -- porting note: Lean 3 didn't need this instance
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
⊢ ↑(AddSubgroup.normedMk (NormedAddGroupHom.range f)) (↑f x✝) = 0
[PROOFSTEP]
letI : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) :=
  (inferInstance : SeminormedAddCommGroup Y)
    -- porting note: again simp doesn't seem to be firing in the below line
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
this : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) := inferInstance
⊢ ↑(AddSubgroup.normedMk (NormedAddGroupHom.range f)) (↑f x✝) = 0
[PROOFSTEP]
rw [← NormedAddGroupHom.mem_ker, f.range.ker_normedMk, f.mem_range]
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
x✝ : ↑X
this : SeminormedAddCommGroup ((forget SemiNormedGroupCat).obj Y) := inferInstance
⊢ ∃ w, ↑f w = ↑f x✝
[PROOFSTEP]
simp only [exists_apply_eq_apply]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
⊢ ∀ (s_1 : ↑Y), s_1 ∈ NormedAddGroupHom.range f → ↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
b : ↑X
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
⊢ Cofork.π (cokernelCocone f) ≫ cokernelLift f s = Cofork.π s
[PROOFSTEP]
ext
[GOAL]
case h
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ↑(Cofork.π (cokernelCocone f) ≫ cokernelLift f s) x✝ = ↑(Cofork.π s) x✝
[PROOFSTEP]
apply NormedAddGroupHom.lift_mk f.range
[GOAL]
case h.hf
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ ∀ (s_1 : ↑Y), s_1 ∈ NormedAddGroupHom.range f → ↑(Cofork.π s) s_1 = 0
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case h.hf.intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X
⊢ ↑(Cofork.π s) (↑(NormedAddGroupHom.toAddMonoidHom f) b) = 0
[PROOFSTEP]
change (f ≫ s.π) b = 0
[GOAL]
case h.hf.intro
X Y : SemiNormedGroupCat
f : X ⟶ Y
s : CokernelCofork f
x✝ : ↑((parallelPair f 0).obj WalkingParallelPair.one)
b : ↑X
⊢ ↑(f ≫ Cofork.π s) b = 0
[PROOFSTEP]
simp
[GOAL]
⊢ HasCokernels SemiNormedGroupCat
[PROOFSTEP]
infer_instance
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ g = 0 ≫ g
[PROOFSTEP]
simp [w]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ f ≫ explicitCokernelπ f = 0
[PROOFSTEP]
convert (cokernelCocone f).w WalkingParallelPairHom.left
[GOAL]
case h.e'_3.h
X Y : SemiNormedGroupCat
f : X ⟶ Y
e_1✝ :
  (X ⟶ explicitCokernel f) =
    ((parallelPair f 0).obj WalkingParallelPair.zero ⟶
      ((Functor.const WalkingParallelPair).obj (cokernelCocone f).pt).obj WalkingParallelPair.one)
⊢ 0 = NatTrans.app (cokernelCocone f).ι WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
x : ↑X
⊢ ↑(f ≫ explicitCokernelπ f) x = 0
[PROOFSTEP]
rw [comp_explicitCokernelπ]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
x : ↑X
⊢ ↑0 x = 0
[PROOFSTEP]
rfl
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
x : ↑Y
⊢ ↑(explicitCokernelπ f ≫ explicitCokernelDesc cond) x = ↑g x
[PROOFSTEP]
rw [explicitCokernelπ_desc]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ e = explicitCokernelDesc w
[PROOFSTEP]
apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ f ≫ g = 0 ≫ g
[PROOFSTEP]
simp [w]
[GOAL]
case x
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (cokernelCocone f).ι j ≫ e = NatTrans.app (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case x.zero
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ NatTrans.app (cokernelCocone f).ι WalkingParallelPair.zero ≫ e =
    NatTrans.app (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).ι WalkingParallelPair.zero
[PROOFSTEP]
convert w.symm
[GOAL]
case h.e'_2.h
X Y Z : SemiNormedGroupCat
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 (_ : f ≫ g = 0 ≫ g)).pt) = (X ⟶ Z)
⊢ NatTrans.app (cokernelCocone f).ι WalkingParallelPair.zero ≫ e = 0
[PROOFSTEP]
simp
[GOAL]
case x.one
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ NatTrans.app (cokernelCocone f).ι WalkingParallelPair.one ≫ e =
    NatTrans.app (Cofork.ofπ g (_ : f ≫ g = 0 ≫ g)).ι WalkingParallelPair.one
[PROOFSTEP]
exact he
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ f ≫ g ≫ h = 0
[PROOFSTEP]
rw [← CategoryTheory.Category.assoc, cond', Limits.zero_comp]
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelDesc cond' ≫ h = explicitCokernelDesc (_ : f ≫ g ≫ h = 0)
[PROOFSTEP]
refine' explicitCokernelDesc_unique _ _ _
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond' ≫ h = g ≫ h
[PROOFSTEP]
rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂
[PROOFSTEP]
let g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂
[PROOFSTEP]
have w : f ≫ g = 0 := by simp
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ f ≫ g = 0
[PROOFSTEP]
simp
[GOAL]
X Y Z : SemiNormedGroupCat
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₂
[PROOFSTEP]
have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl
[GOAL]
X Y Z : SemiNormedGroupCat
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
[PROOFSTEP]
apply explicitCokernelDesc_unique
[GOAL]
case he
X Y Z : SemiNormedGroupCat
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
[PROOFSTEP]
rfl
[GOAL]
X Y Z : SemiNormedGroupCat
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₂
[PROOFSTEP]
rw [this]
[GOAL]
X Y Z : SemiNormedGroupCat
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₁ = explicitCokernelDesc w
[PROOFSTEP]
apply explicitCokernelDesc_unique
[GOAL]
case he
X Y Z : SemiNormedGroupCat
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
[PROOFSTEP]
exact h
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ Epi (explicitCokernelπ f)
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ ∀ {Z : SemiNormedGroupCat} (g h : explicitCokernel f ⟶ Z), explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h → g = h
[PROOFSTEP]
intro Z g h H
[GOAL]
case left_cancellation
X Y : SemiNormedGroupCat
f : X ⟶ Y
Z : SemiNormedGroupCat
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
⊢ g = h
[PROOFSTEP]
ext x
[GOAL]
case left_cancellation.h.h
X Y : SemiNormedGroupCat
f : X ⟶ Y
Z : SemiNormedGroupCat
g h : explicitCokernel f ⟶ Z
H : explicitCokernelπ f ≫ g = explicitCokernelπ f ≫ h
x : ↑Y
⊢ ↑(explicitCokernelπ f ≫ g) x = ↑(explicitCokernelπ f ≫ h) x
[PROOFSTEP]
rw [H]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : NormedAddGroupHom.NormNoninc g
⊢ NormedAddGroupHom.NormNoninc (explicitCokernelDesc cond)
[PROOFSTEP]
refine' NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 _
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : NormedAddGroupHom.NormNoninc g
⊢ ‖explicitCokernelDesc cond‖ ≤ 1
[PROOFSTEP]
rw [← NNReal.coe_one]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
cond : f ≫ g = 0
hg : NormedAddGroupHom.NormNoninc g
⊢ ‖explicitCokernelDesc cond‖ ≤ ↑1
[PROOFSTEP]
exact explicitCokernelDesc_norm_le_of_norm_le cond 1 (NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hg)
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ explicitCokernelDesc cond ≫ h = 0
[PROOFSTEP]
rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]
[GOAL]
X Y Z W : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond : f ≫ g = 0
cond2 : g ≫ h = 0
⊢ g ≫ h = explicitCokernelπ f ≫ 0
[PROOFSTEP]
simp [cond2]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom = cokernel.π f
[PROOFSTEP]
simp [explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]
[GOAL]
X Y : SemiNormedGroupCat
f : X ⟶ Y
⊢ cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f
[PROOFSTEP]
simp [explicitCokernelπ, explicitCokernelIso]
[GOAL]
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w
[PROOFSTEP]
ext1
[GOAL]
case h
X Y Z : SemiNormedGroupCat
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w
[PROOFSTEP]
simp [explicitCokernelDesc, explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]
[GOAL]
A B C D : SemiNormedGroupCat
fab : A ⟶ B
fbd : B ⟶ D
fac : A ⟶ C
fcd : C ⟶ D
h : fab ≫ fbd = fac ≫ fcd
⊢ fab ≫ fbd ≫ explicitCokernelπ fcd = 0
[PROOFSTEP]
simp [reassoc_of% h]
[GOAL]
A B C D B' D' : SemiNormedGroupCat
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 = explicitCokernel.map h ≫ explicitCokernelDesc condd
[PROOFSTEP]
delta explicitCokernel.map
[GOAL]
A B C D B' D' : SemiNormedGroupCat
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 (_ : fab ≫ fbd ≫ explicitCokernelπ fcd = 0) ≫ explicitCokernelDesc condd
[PROOFSTEP]
simp [← cancel_epi (explicitCokernelπ fab), ← Category.assoc, explicitCokernelπ_desc, h']
