awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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‖ * ‖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‖ <
      ε
⊢ ‖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) + ε

Tactic:
(sub_lt_iff_lt_add'.mp h.1).le

Premises used: LT.lt.le, sub_lt_iff_lt_add', And.left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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‖ * ‖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‖ <
      ε
⊢ ‖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) + ε

Tactic:
calc
      _ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
      _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

Premises used: HMul.hMul, LT.lt.le, sub_lt_iff_lt_add', And.left, Iff.mp, LE.le.trans, norm_mul_le, Ideal.Quotient.norm_mk_le
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
x : ℝ≥0
⊢ ‖x‖₊ = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
x : ℝ≥0∞
⊢ ‖x‖ₑ = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Real
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
⊢ enorm (E := ℝ≥0∞) 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Real
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
⊢ ∀ (x y : ℝ≥0∞), ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Real
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
⊢ ∀ (x : ℝ≥0∞), ‖x‖ₑ = 0 ↔ x = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
⊢ ‖r‖ = |r|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Real
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‖
rw₅ rw₆ : |_y + -_r| = |_y + -_r|
⊢ dist _r _y = ‖-_r + _y‖

Tactic:
rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]

Premises used: abs_neg, neg_sub, sub_eq_add_neg, add_comm, Real.dist_eq, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ = r

Tactic:
abs_of_nonneg hr

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : r ≤ 0
⊢ ‖r‖ = -r

Tactic:
abs_of_nonpos hr

Premises used: abs_of_nonpos
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
⊢ r ≤ ‖r‖

Tactic:
le_abs_self r

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
n : ℕ
⊢ Norm.norm (E := ℝ) (↑n : ℝ) = (↑n : ℝ)

Tactic:
abs_of_nonneg n.cast_nonneg

Premises used: Nat.cast_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
n : ℕ
⊢ nnnorm (E := ℝ) (↑n : ℝ) = (↑n : ℝ≥0)

Tactic:
NNReal.eq <| norm_natCast _

Premises used: Real.norm_natCast, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
n : ℕ
⊢ enorm (E := ℝ) (↑n : ℝ) = (↑n : ℝ≥0∞)

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Norm.norm (E := ℝ) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
norm_natCast n

Premises used: Real.norm_natCast
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ nnnorm (E := ℝ) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
nnnorm_natCast n

Premises used: Real.nnnorm_natCast
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
⊢ Norm.norm (E := ℝ) 2 = 2

Tactic:
abs_of_pos zero_lt_two

Premises used: abs_of_pos, zero_lt_two
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
⊢ (↑(nnnorm (E := ℝ) 2) : ℝ) = (↑2 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
q : ℚ≥0
⊢ Norm.norm (E := ℝ) (↑q : ℝ) = (↑q : ℝ)

Tactic:
norm_of_nonneg q.cast_nonneg

Premises used: NNRat.cast_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
q : ℚ≥0
simp : NNReal.mk (↑q : ℝ) ⋯ = (↑q : ℝ≥0)
⊢ nnnorm (E := ℝ) (↑q : ℝ) = (↑q : ℝ≥0)

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
q : ℚ≥0
⊢ NNReal.mk (↑q : ℝ) ⋯ = (↑q : ℝ≥0)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
⊢ ‖r‖₊ = NNReal.mk r hr

Tactic:
NNReal.eq <| norm_of_nonneg hr

Premises used: NNReal.eq, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
simp [enorm, nnnorm_of_nonneg hr, ENNReal.ofReal, toNNReal, hr]

Premises used: ENNReal.ofReal, ENorm.enorm, Real.nnnorm_of_nonneg, Real.toNNReal
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
a : ℝ
ha : 0 ≤ a
⊢ ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ

Tactic:
simp [Real.enorm_of_nonneg, ha]

Premises used: Real.enorm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
⊢ ‖|r|‖₊ = ‖r‖₊

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
⊢ ‖|r|‖ₑ = ‖r‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
rw : ENNReal.ofReal ‖r‖ = ENNReal.ofReal r
rw₁ rw₂ : ENNReal.ofReal r = ENNReal.ofReal r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
rw [← ofReal_norm, norm_of_nonneg hr]

Premises used: ofReal_norm, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
rw : ‖r‖ₑ = ‖|r|‖ₑ
rw₁ rw₂ : ‖r‖ₑ = ‖r‖ₑ
⊢ ‖r‖ₑ = ENNReal.ofReal |r|

Tactic:
rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]

Premises used: Real.enorm_abs, Real.enorm_eq_ofReal, abs_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
rw : NNReal.mk r hr = ‖r‖₊
⊢ r.toNNReal = ‖r‖₊

Tactic:
rw [Real.toNNReal_of_nonneg hr]

Premises used: Real.toNNReal_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
e_x : r = ‖r‖
⊢ NNReal.mk r hr = ‖r‖₊

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
hr : 0 ≤ r
e_x : r = |r|
e_x₁ e_x₂ : r = r
⊢ r = ‖r‖

Tactic:
rw [Real.norm_eq_abs r, abs_of_nonneg hr]

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
rw : ENNReal.ofReal r ≤ ENNReal.ofReal |r|
⊢ ENNReal.ofReal r ≤ ‖r‖ₑ

Tactic:
rw [enorm_eq_ofReal_abs]

Premises used: Real.enorm_eq_ofReal_abs
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
h : r ≤ |r|
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
⊢ r ≤ |r|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
r : ℝ
⊢ r ≤ |r|

Tactic:
exact le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x : E
⊢ ‖‖x‖‖ = ‖x‖

Tactic:
Real.norm_of_nonneg (norm_nonneg' _)

Premises used: norm_nonneg', Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x : E
⊢ ‖‖x‖‖₊ = ‖x‖₊

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x : E
⊢ ‖‖x‖‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
ε : Type u_9
inst : ENorm ε
x : ε
⊢ ‖‖x‖ₑ‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Real
Goal:
⊢ Tendsto (α := ℝ) norm atTop atTop

Tactic:
tendsto_abs_atTop_atTop

Premises used: abs, Filter.tendsto_abs_atTop_atTop
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
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 ⋯)) :
              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)
⊢ f ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk ⋯ =
    0 ≫ mkHom (↑(Hom.hom f) : NormedAddGroupHom X.carrier Y.carrier).range.normedMk ⋯

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
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)
⊢ 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)

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]

Premises used: SemiNormedGrp₁.comp_apply, NormedAddGroupHom.mem_ker, NormedAddGroupHom.range, SemiNormedGrp₁.mkHom_apply, AddSubgroup.ker_normedMk, SemiNormedGrp₁.zero_apply, SemiNormedGrp₁.Hom.hom, CategoryTheory.Limits.zero_comp, NormedAddGroupHom.mem_range, Subtype.val
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x w : X.carrier
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)
⊢ ∃ (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:
use x
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
hom' : NormedAddGroupHom (cokernelCocone f).pt.carrier s.pt.carrier
normNoninc : (NormedAddGroupHom.lift f.hom'.range (Cofork.π s).hom' ⋯).NormNoninc
⊢ (cokernelCocone f).pt ⟶ s.pt

Tactic:
fconstructor
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
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)
⊢ NormedAddGroupHom (cokernelCocone f).pt.carrier s.pt.carrier

Tactic:
apply NormedAddGroupHom.lift _ s.π.1

Premises used: NormedAddGroupHom.lift, SemiNormedGrp₁.Hom.hom', CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
b : X.carrier
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)
⊢ 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)

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

Premises used: CategoryTheory.CategoryStruct.comp, SemiNormedGrp₁.Hom.hom, Subtype.val, 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)
    (((↑(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:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (NormedAddGroupHom.lift f.hom'.range (Cofork.π s).hom' ⋯).NormNoninc

Tactic:
NormedAddGroupHom.lift_normNoninc _ _ _ s.π.2

Premises used: Set.Mem, setOf, NormedAddGroupHom.lift_normNoninc, SemiNormedGrp₁.Hom.normNoninc, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
X Y : SemiNormedGrp₁
f : X ⟶ Y
s : CokernelCofork f
⊢ (NormedAddGroupHom.lift f.hom'.range (Cofork.π s).hom' ⋯).NormNoninc

Tactic:
exact NormedAddGroupHom.lift_normNoninc _ _ _ s.π.2

Premises used: NormedAddGroupHom.lift_normNoninc, SemiNormedGrp₁.Hom.normNoninc, CategoryTheory.Limits.Cofork.π
-- 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)) : 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)
⊢ (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 ∈ 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)
⊢ 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:
apply NormedAddGroupHom.lift_mk f.1.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)
    (((↑(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)
⊢ 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)

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

Premises used: CategoryTheory.CategoryStruct.comp, SemiNormedGrp₁.Hom.hom, Subtype.val, 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)
    (((↑(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:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
⊢ HasCokernels SemiNormedGrp₁

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
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)
⊢ ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f = ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g

Tactic:
ext v
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
v : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier
⊢ (↑v : V.carrier) ∈ (Hom.hom (f - g)).ker

Tactic:
have : v.1 ∈ (f - g).hom.ker := v.2
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
v : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier
this : (↑v : V.carrier) ∈ (Hom.hom (f - g)).ker
⊢ 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:
simpa [-SetLike.coe_mem, NormedAddGroupHom.mem_ker, sub_eq_zero] using this

Premises used: SetLike.coe_mem, sub_eq_zero, NormedAddGroupHom.mem_ker
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
Goal:
V W : SemiNormedGrp
f g : V ⟶ W
c : Fork f g
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)
⊢ 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)

Tactic:
rw [hom_sub, map_sub, AddMonoidHom.sub_apply, sub_eq_zero]

Premises used: SemiNormedGrp.hom_sub, map_sub, sub_eq_zero, AddMonoidHom.sub_apply
-- 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:
congr_arg Hom.hom c.condition

Premises used: SemiNormedGrp.Hom.hom, congr_arg, CategoryTheory.Limits.Fork.condition