awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁
b : R
hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁ ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - a_1 < ε₁ →
      b_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂ ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - b_1 < ε₂ →
        a_1 * b_1 -
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
            ε ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
              a_1 * b_1 <
            ε
⊢ ‖HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)‖ ≤
    norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) * norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε
have h₃ : ‖a‖ * ‖b‖ -
      norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) * norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
    ε ∧
  norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) * norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
      ‖a‖ * ‖b‖ <
    ε
Tactic: specialize h ‖a‖ ‖b‖ ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I a]⟩
      ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I b]⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ dist _r _y = ‖-_r + _y‖
have rw : |_r - _y| = ‖-_r + _y‖
Tactic: rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
rw : |_r - _y| = ‖-_r + _y‖
⊢ dist _r _y = ‖-_r + _y‖
have rw₁ : |(-(_r - _y))| = ‖-_r + _y‖
Tactic: rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
rw : |_r - _y| = ‖-_r + _y‖
rw₁ : |(-(_r - _y))| = ‖-_r + _y‖
⊢ dist _r _y = ‖-_r + _y‖
have rw₂ : |_y - _r| = ‖-_r + _y‖
Tactic: rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
rw : |_r - _y| = ‖-_r + _y‖
rw₁ : |(-(_r - _y))| = ‖-_r + _y‖
rw₂ : |_y - _r| = ‖-_r + _y‖
⊢ dist _r _y = ‖-_r + _y‖
have rw₃ : |_y - _r| = ‖_y + -_r‖
Tactic: rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
rw : |_r - _y| = ‖-_r + _y‖
rw₁ : |(-(_r - _y))| = ‖-_r + _y‖
rw₂ : |_y - _r| = ‖-_r + _y‖
rw₃ : |_y - _r| = ‖_y + -_r‖
⊢ dist _r _y = ‖-_r + _y‖
have rw₄ : |_y + -_r| = ‖_y + -_r‖
Tactic: rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
rw : |_r - _y| = ‖-_r + _y‖
rw₁ : |(-(_r - _y))| = ‖-_r + _y‖
rw₂ : |_y - _r| = ‖-_r + _y‖
rw₃ : |_y - _r| = ‖_y + -_r‖
rw₄ : |_y + -_r| = ‖_y + -_r‖
⊢ dist _r _y = ‖-_r + _y‖
have rw₅ : |_y + -_r| = |_y + -_r|
Tactic: rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
q : ℚ≥0
⊢ nnnorm (E := ℝ) (↑q : ℝ) = (↑q : ℝ≥0)
have simp : NNReal.mk (↑q : ℝ) sorry = (↑q : ℝ≥0)
Tactic: simp [nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r
have rw : ENNReal.ofReal ‖r‖ = ENNReal.ofReal r
Tactic: rw [← ofReal_norm, norm_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
hr : 0 ≤ r
rw : ENNReal.ofReal ‖r‖ = ENNReal.ofReal r
⊢ ‖r‖ₑ = ENNReal.ofReal r
have rw₁ : ENNReal.ofReal r = ENNReal.ofReal r
Tactic: rw [← ofReal_norm, norm_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
⊢ ‖r‖ₑ = ENNReal.ofReal |r|
have rw : ‖r‖ₑ = ‖|r|‖ₑ
Tactic: rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
rw : ‖r‖ₑ = ‖|r|‖ₑ
⊢ ‖r‖ₑ = ENNReal.ofReal |r|
have rw₁ : ‖r‖ₑ = ‖r‖ₑ
Tactic: rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = ‖r‖₊
have rw : NNReal.mk r hr = ‖r‖₊
Tactic: rw [Real.toNNReal_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
hr : 0 ≤ r
⊢ NNReal.mk r hr = ‖r‖₊
have e_x : r = ‖r‖
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
hr : 0 ≤ r
⊢ r = ‖r‖
have e_x : r = |r|
Tactic: rw [Real.norm_eq_abs r, abs_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
hr : 0 ≤ r
e_x : r = |r|
⊢ r = ‖r‖
have e_x₁ : r = r
Tactic: rw [Real.norm_eq_abs r, abs_of_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
⊢ ENNReal.ofReal r ≤ ‖r‖ₑ
have rw : ENNReal.ofReal r ≤ ENNReal.ofReal |r|
Tactic: rw [enorm_eq_ofReal_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Real (goal)
Goal:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|
have h : r ≤ |r|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
⊢ f ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk ⋯ =
    0 ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk ⋯
have hf : ∀ (x : X.carrier),
  Eq (α :=
    { carrier := Y.carrier ⧸ f.hom'.range, str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
    (((↑(Hom.hom (f ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk sorry)) :
            NormedAddGroupHom X.carrier
              { carrier := Y.carrier ⧸ f.hom'.range,
                  str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier) :
          (a : X.carrier) →
            { carrier := Y.carrier ⧸ f.hom'.range,
                str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
        x :
      { carrier := Y.carrier ⧸ f.hom'.range, str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
    (((↑(Hom.hom (0 ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk sorry)) :
            NormedAddGroupHom X.carrier
              { carrier := Y.carrier ⧸ f.hom'.range,
                  str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier) :
          (a : X.carrier) →
            { carrier := Y.carrier ⧸ f.hom'.range,
                str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
        x :
      { carrier := Y.carrier ⧸ f.hom'.range, str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
⊢ Eq (α :=
    { carrier := Y.carrier ⧸ f.hom'.range, str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
    (((↑(Hom.hom (f ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk ⋯)) :
            NormedAddGroupHom X.carrier
              { carrier := Y.carrier ⧸ f.hom'.range,
                  str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier) :
          (a : X.carrier) →
            { carrier := Y.carrier ⧸ f.hom'.range,
                str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
        x :
      { carrier := Y.carrier ⧸ f.hom'.range, str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
    (((↑(Hom.hom (0 ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk ⋯)) :
            NormedAddGroupHom X.carrier
              { carrier := Y.carrier ⧸ f.hom'.range,
                  str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier) :
          (a : X.carrier) →
            { carrier := Y.carrier ⧸ f.hom'.range,
                str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
        x :
      { carrier := Y.carrier ⧸ f.hom'.range, str := QuotientAddGroup.instSeminormedAddCommGroup f.hom'.range }.carrier)
have hf : ∃ (w : X.carrier),
  Eq (α := Y.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier) : (a : X.carrier) → Y.carrier) w : Y.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier) : (a : X.carrier) → Y.carrier) x : Y.carrier)
Tactic: rw [Limits.zero_comp, comp_apply, SemiNormedGrp₁.mkHom_apply,
        SemiNormedGrp₁.zero_apply, ← NormedAddGroupHom.mem_ker, f.hom.1.range.ker_normedMk,
        f.hom.1.mem_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x w : X.carrier
⊢ ∃ (w : X.carrier),
    Eq (α := Y.carrier)
      (((↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier) : (a : X.carrier) → Y.carrier) w : Y.carrier)
      (((↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier) : (a : X.carrier) → Y.carrier) x : Y.carrier)
have h : Eq (α := Y.carrier)
  (((↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier) : (a : X.carrier) → Y.carrier) x : Y.carrier)
  (((↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier) : (a : X.carrier) → Y.carrier) x : Y.carrier)
Tactic: use x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (cokernelCocone f).pt ⟶ s.pt
have hom' : NormedAddGroupHom (cokernelCocone f).pt.carrier s.pt.carrier
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
hom' : NormedAddGroupHom (cokernelCocone f).pt.carrier s.pt.carrier
⊢ (cokernelCocone f).pt ⟶ s.pt
have normNoninc : (NormedAddGroupHom.lift f.hom'.range (Cofork.π s).hom' sorry).NormNoninc
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ NormedAddGroupHom (cokernelCocone f).pt.carrier s.pt.carrier
have hom' : ∀ s_1 ∈ f.hom'.range,
  Eq (α := s.pt.carrier) (((Cofork.π s).hom' : (a : Y.carrier) → s.pt.carrier) s_1 : s.pt.carrier) (0 : s.pt.carrier)
Tactic: apply NormedAddGroupHom.lift _ s.π.1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
b : X.carrier
⊢ Eq (α := s.pt.carrier)
    (((Cofork.π s).hom' : (a : Y.carrier) → s.pt.carrier)
        ((f.hom'.toAddMonoidHom : (a : X.carrier) → Y.carrier) b : Y.carrier) :
      s.pt.carrier)
    (0 : s.pt.carrier)
have hom' : Eq (α := s.pt.carrier)
  (((↑(Hom.hom (f ≫ Cofork.π s)) : NormedAddGroupHom X.carrier s.pt.carrier) : (a : X.carrier) → s.pt.carrier) b :
    s.pt.carrier)
  (0 : s.pt.carrier)
Tactic: change (f ≫ s.π) b = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (cokernelCocone f).π ≫ cokernelLift f s = Cofork.π s
have hf : ∀ (x : Y.carrier),
  Eq (α := s.pt.carrier)
    (((↑(Hom.hom ((cokernelCocone f).π ≫ cokernelLift f s)) : NormedAddGroupHom Y.carrier s.pt.carrier) :
          (a : Y.carrier) → s.pt.carrier)
        x :
      s.pt.carrier)
    (((↑(Hom.hom (Cofork.π s)) : NormedAddGroupHom Y.carrier s.pt.carrier) : (a : Y.carrier) → s.pt.carrier) x :
      s.pt.carrier)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
x : Y.carrier
⊢ Eq (α := s.pt.carrier)
    (((↑(Hom.hom ((cokernelCocone f).π ≫ cokernelLift f s)) : NormedAddGroupHom Y.carrier s.pt.carrier) :
          (a : Y.carrier) → s.pt.carrier)
        x :
      s.pt.carrier)
    (((↑(Hom.hom (Cofork.π s)) : NormedAddGroupHom Y.carrier s.pt.carrier) : (a : Y.carrier) → s.pt.carrier) x :
      s.pt.carrier)
have hf : ∀ s_1 ∈ f.hom'.range,
  Eq (α := s.pt.carrier) (((Cofork.π s).hom' : (a : Y.carrier) → s.pt.carrier) s_1 : s.pt.carrier) (0 : s.pt.carrier)
Tactic: apply NormedAddGroupHom.lift_mk f.1.range
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
x : Y.carrier
b : X.carrier
⊢ Eq (α := s.pt.carrier)
    (((Cofork.π s).hom' : (a : Y.carrier) → s.pt.carrier)
        ((f.hom'.toAddMonoidHom : (a : X.carrier) → Y.carrier) b : Y.carrier) :
      s.pt.carrier)
    (0 : s.pt.carrier)
have hf : Eq (α := s.pt.carrier)
  (((↑(Hom.hom (f ≫ Cofork.π s)) : NormedAddGroupHom X.carrier s.pt.carrier) : (a : X.carrier) → s.pt.carrier) b :
    s.pt.carrier)
  (0 : s.pt.carrier)
Tactic: change (f ≫ s.π) b = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
⊢ ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f = ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g
have hf : ∀ (v : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier),
  Eq (α := W.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f) :
          (a : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier) → W.carrier)
        v :
      W.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g) :
          (a : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier) → W.carrier)
        v :
      W.carrier)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (hypothesis)
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
v : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier
⊢ Eq (α := W.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f) :
          (a : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier) → W.carrier)
        v :
      W.carrier)
    ((Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g) :
          (a : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier) → W.carrier)
        v :
      W.carrier)
have this : (↑v : V.carrier) ∈ (Hom.hom (f - g)).ker
Tactic: have : v.1 ∈ (f - g).hom.ker := v.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
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 - 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)
    (0 : NormedAddGroupHom c.pt.carrier W.carrier)
have rw : 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: rw [hom_sub, map_sub, AddMonoidHom.sub_apply, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
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.ι
⊢ g = (fun (c : Fork f g_1) ↦ ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g_1)) ⋯)) c
have 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)) sorry)) c) :
          (a : c.pt.carrier) → (fork f g_1).pt.carrier)
        x :
      (fork f g_1).pt.carrier)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
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 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)
have 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) sorry)) :
        (a : c.pt.carrier) → (fork f g_1).pt.carrier)
      x :
    (fork f g_1).pt.carrier)
Tactic: simp_rw [← h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
b : X.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)
have 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)
Tactic: change (f ≫ s.π) b = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
⊢ (cokernelCocone f).π ≫ cokernelLift f s = Cofork.π s
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
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)
have 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)
Tactic: apply NormedAddGroupHom.lift_mk f.hom.range
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
s : CokernelCofork f
x : Y.carrier
b : X.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)
have 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)
Tactic: change (f ≫ s.π) b = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ f ≫ explicitCokernelπ f = 0
have h : (X ⟶ explicitCokernel f) = ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (cokernelCocone f).pt) →
  0 = (cokernelCocone f).ι.app WalkingParallelPair.zero
Tactic: convert! (cokernelCocone f).w WalkingParallelPairHom.left
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels (goal)
Goal:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.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)
have 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)
Tactic: rw [comp_explicitCokernelπ]