awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (hypothesis)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ Eq (α := (↑F'.1 : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.e :
          (a : (↑G : Type)) → (↑F'.I : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑F'.I : Type))
    (0 : (↑F'.1 : Type))
have this : Mono F'.m
Tactic: haveI := F'.m_mono
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ Eq (α := (↑F'.1 : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.e :
          (a : (↑G : Type)) → (↑F'.I : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑F'.I : Type))
    (0 : (↑F'.1 : Type))
have a : Eq (α := (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
        (a : (↑F'.I : Type)) → (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦
                  Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                    ((↑0 : (↑H : Type)) : (↑H : Type)))
                sorry) :
            (↑G : Type)) :
        (↑F'.I : Type)) :
    (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
        (a : (↑F'.I : Type)) → (↑H : Type))
      0 :
    (↑H : Type))
Tactic: apply injective_of_mono F'.m
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                F'.e :
              (a : (↑G : Type)) → (↑F'.I : Type))
            (↑(Classical.indefiniteDescription
                  (fun (x : (↑G : Type)) ↦
                    Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                      ((↑0 : (↑H : Type)) : (↑H : Type)))
                  ⋯) :
              (↑G : Type)) :
          (↑F'.I : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        0 :
      (↑H : Type))
have a : Eq (α := (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x : (↑G : Type)) ↦
              Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                ((↑0 : (↑H : Type)) : (↑H : Type)))
            sorry) :
        (↑G : Type)) :
    (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
        (a : (↑F'.I : Type)) → (↑H : Type))
      0 :
    (↑H : Type))
Tactic: change (F'.e ≫ F'.m) _ = _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
            (F'.e ≫ F'.m) :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦
                Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                  ((↑0 : (↑H : Type)) : (↑H : Type)))
              ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
          (a : (↑F'.I : Type)) → (↑H : Type))
        0 :
      (↑H : Type))
have a : Eq (α := (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x : (↑G : Type)) ↦
              Eq (α := (↑H : Type)) ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
                ((↑0 : (↑H : Type)) : (↑H : Type)))
            sorry) :
        (↑G : Type)) :
    (↑H : Type))
  (0 : (↑H : Type))
Tactic: rw [F'.fac, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (hypothesis)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.e :
        (a : (↑G : Type)) → (↑F'.I : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑F'.1 : Type)) (β := (↑F'.1 : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑F'.I : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑F'.I : Type))
have this : Mono F'.m
Tactic: haveI := F'.m_mono
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.e :
        (a : (↑G : Type)) → (↑F'.I : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑F'.1 : Type)) (β := (↑F'.1 : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑F'.I : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑F'.I : Type))
have a : Eq (α := (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
        (a : (↑F'.I : Type)) → (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
                sorry) :
            (↑G : Type)) :
        (↑F'.I : Type)) :
    (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
        (a : (↑F'.I : Type)) → (↑H : Type))
      (HAdd.hAdd (α := (↑F'.1 : Type)) (β := (↑F'.1 : Type))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                F'.e :
              (a : (↑G : Type)) → (↑F'.I : Type))
            (↑(Classical.indefiniteDescription
                  (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type)))
                  sorry) :
              (↑G : Type)) :
          (↑F'.I : Type))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                F'.e :
              (a : (↑G : Type)) → (↑F'.I : Type))
            (↑(Classical.indefiniteDescription
                  (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) sorry) :
              (↑G : Type)) :
          (↑F'.I : Type))) :
    (↑H : Type))
Tactic: apply injective_of_mono F'.m
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              (F'.e ≫ F'.m) :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              (F'.e ≫ F'.m) :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
have a : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
      (a : (↑G : Type)) → (↑H : Type))
    (↑(Classical.indefiniteDescription
          (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type))) sorry) :
      (↑G : Type)) =
  HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) sorry) :
          (↑G : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) sorry) :
          (↑G : Type)) :
      (↑H : Type))
Tactic: rw [F'.fac]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
have a : (↑(x + y) : (↑H : Type)) =
  HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) sorry) :
          (↑G : Type)) :
      (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) sorry) :
          (↑G : Type)) :
      (↑H : Type))
Tactic: rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (↑(x + y) : (↑H : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
have a : (↑(x + y) : (↑H : Type)) =
  HAdd.hAdd (β := (↑H : Type)) (↑x : (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) sorry) :
          (↑G : Type)) :
      (↑H : Type))
Tactic: rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (↑(x + y) : (↑H : Type)) =
    HAdd.hAdd (β := (↑H : Type)) (↑x : (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) f :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
have a : (↑(x + y) : (↑H : Type)) = (↑x : (↑H : Type)) + (↑y : (↑H : Type))
Tactic: rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
have hf : ∀ (x : (↑(image f) : Type)),
  Eq (α := (↑H : Type)) ((Hom.hom (lift F' ≫ F'.m) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type)
⊢ Eq (α := (↑H : Type)) ((Hom.hom (lift F' ≫ F'.m) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
have hf : Eq (α := (↑H : Type))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) sorry) :
        (↑G : Type)) :
    (↑H : Type))
  ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
Tactic: change (F'.e ≫ F'.m) _ = _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type)
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
            (F'.e ≫ F'.m) :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))
have hf : (↑x : (↑H : Type)) = (Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x
Tactic: rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
I : Ideal ℤ
g : ↥I →ₗ[ℤ] A
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : x ∈ I),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A) ((g : (a : ↥I) → A) (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ I) x mem) : A)
have rcases : ∀ (m : ℤ) (g : ↥(ℤ ∙ m) →ₗ[ℤ] A),
  ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)
Tactic: rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩
Cleared hypotheses: I, g
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)
have inl : ∀ (g : ↥(ℤ ∙ 0) →ₗ[ℤ] A),
  ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) x mem) : A)
Tactic: obtain rfl | h0 := eq_or_ne m 0
Cleared hypotheses: m, g
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
inl :
  ∀ (g : ↥(ℤ ∙ 0) →ₗ[ℤ] A),
    ∃ (g' : ℤ →ₗ[ℤ] A),
      ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x),
        Eq (α := A) ((g' : (a : ℤ) → A) x : A)
          ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) x mem) : A)
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)
have inr : ∀ (h0 : m ≠ 0),
  ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)
Tactic: obtain rfl | h0 := eq_or_ne m 0
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) x mem) : A)
have inl : ∀ (n : ℤ) (hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) n),
  Eq.{u + 1} (α := A) ((0 : (a : ℤ) → A) n : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) n hn) : A)
Tactic: refine ⟨0, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (hypothesis)
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) n
⊢ Eq.{u + 1} (α := A) ((0 : (a : ℤ) → A) n : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) n hn) : A)
have hn₁ : Membership.mem (γ := Ideal ℤ) ⊥ n
Tactic: rw [Submodule.span_zero_singleton] at hn
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn_1 : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) n
hn : Membership.mem (γ := Ideal ℤ) ⊥ n
⊢ Eq.{u + 1} (α := A) ((0 : (a : ℤ) → A) n : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) n hn_1) : A)
have inl : ∀ (hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) 0),
  Eq (α := A) ((0 : (a : ℤ) → A) 0 : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) 0 hn) : A)
Tactic: subst hn
Cleared hypotheses: n, hn_1, hn