awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Ulift (goal)
Goal:
J : Type w
x : Category.{w', w} J
F : CategoryTheory.Functor.{w', u, w, u + 1} J AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))
have rw : Function.Bijective (α := Colimits.Quot F) (β := (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))
  (⇑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) (Quot.desc F c)) :
    (a : Colimits.Quot F) → (↑(uliftFunctor.mapCocone c).pt : Type (max u v)))
Tactic: rw [isColimit_iff_bijective_desc, ← Function.Bijective.of_comp_iff _
          (quotQuotUliftAddEquiv F).bijective, ← AddEquiv.coe_toAddMonoidHom,
          ← AddMonoidHom.coe_comp, Quot.desc_quotQuotUliftAddEquiv]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.ZModuleEquivalence (goal)
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
⊢ AddHom.toFun
      {
        toFun :=
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) f) :
            (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
              (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u)),
        map_add' := ⋯ : (↑A : Type u) →ₙ+ (↑B : Type u) }
      (n • x) =
    HSMul.hSMul (α := ℤ) ((RingHom.id ℤ : (a : ℤ) → ℤ) n : ℤ)
      (AddHom.toFun
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) f) :
              (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
                (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u)),
          map_add' := ⋯ : (↑A : Type u) →ₙ+ (↑B : Type u) }
        x)
have h : (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u) →
  (↑A : Type u) =
      (↑(Functor.obj
            (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
              carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            A) :
        Type u) →
    Eq.{u + 1} (α := SMul ℤ (↑A : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
Tactic: convert! AddMonoidHom.map_zsmul f.hom n x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.ZModuleEquivalence (goal)
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
h :
  (↑B : Type u) =
      (↑(Functor.obj
            (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
              carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            B) :
        Type u) →
    (↑A : Type u) =
        (↑(Functor.obj
              (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              A) :
          Type u) →
      Eq.{u + 1} (α := SMul ℤ (↑A : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
⊢ AddHom.toFun
      {
        toFun :=
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) f) :
            (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
              (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u)),
        map_add' := ⋯ : (↑A : Type u) →ₙ+ (↑B : Type u) }
      (n • x) =
    HSMul.hSMul (α := ℤ) ((RingHom.id ℤ : (a : ℤ) → ℤ) n : ℤ)
      (AddHom.toFun
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) f) :
              (a : (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A) : Type u)) →
                (↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B) : Type u)),
          map_add' := ⋯ : (↑A : Type u) →ₙ+ (↑B : Type u) }
        x)
have h₁ : (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u) →
  Eq.{u + 1} (α := SMul ℤ (↑B : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
Tactic: convert! AddMonoidHom.map_zsmul f.hom n x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.ZModuleEquivalence (goal)
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
e_1 :
  (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u)
e_2 :
  (↑A : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          A) :
      Type u)
⊢ Eq.{u + 1} (α := SMul ℤ (↑A : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
have h : ∀ (x : ℤ) (x_1 : (↑A : Type u)), SMul.smul x x_1 = SMul.smul x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.ZModuleEquivalence (goal)
Goal:
A B : ModuleCat ℤ
f :
  Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      A ⟶
    Functor.obj
      (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      B
n : ℤ
x : (↑A : Type u)
e_1 :
  (↑B : Type u) =
    (↑(Functor.obj
          (forget₂ (ModuleCat ℤ) (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC := carrier)
            AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          B) :
      Type u)
⊢ Eq.{u + 1} (α := SMul ℤ (↑B : Type u)) (@SMulZeroClass.toSMul _ _ AddZero.toZero _) SubNegMonoid.toZSMul
have h : ∀ (x : ℤ) (x_1 : (↑B : Type u)), SMul.smul x x_1 = SMul.smul x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
⊢ IsZero G
have refine_1 : ∀ (X : GrpCat.{u_1}) (f : G ⟶ X), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
refine_1 : ∀ (X : GrpCat.{u_1}) (f : G ⟶ X), f = default
⊢ IsZero G
have refine_2 : ∀ (X : GrpCat.{u_1}) (f : X ⟶ G), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
⊢ f = default
have refine_1 : ∀ (x : (↑G : Type u_1)),
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (hypothesis)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
x : (↑G : Type u_1)
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have this : x = 1
Tactic: have : x = 1 := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have refine_1 : Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
  ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
Tactic: rw [this, map_one, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
refine_1 :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have refine_1₁ : Eq.{u_1 + 1} (α := (↑X : Type u_1)) (1 : (↑X : Type u_1))
  ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
Tactic: rw [this, map_one, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
refine_1 :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
refine_1₁ :
  Eq.{u_1 + 1} (α := (↑X : Type u_1)) (1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have refine_1₂ : Eq.{u_1 + 1} (α := (↑X : Type u_1)) 1 1
Tactic: rw [this, map_one, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : X ⟶ G
⊢ f = default
have refine_2 : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑G : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
⊢ IsZero G
have refine_1 : ∀ (X : CommGrpCat.{u_1}) (f : G ⟶ X), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
refine_1 : ∀ (X : CommGrpCat.{u_1}) (f : G ⟶ X), f = default
⊢ IsZero G
have refine_2 : ∀ (X : CommGrpCat.{u_1}) (f : X ⟶ G), f = default
Tactic: refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
⊢ f = default
have refine_1 : ∀ (x : (↑G : Type u_1)),
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (hypothesis)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
x : (↑G : Type u_1)
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have this : x = 1
Tactic: have : x = 1 := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have refine_1 : Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
  ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
Tactic: rw [this, map_one, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
refine_1 :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have refine_1₁ : Eq.{u_1 + 1} (α := (↑X : Type u_1)) (1 : (↑X : Type u_1))
  ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
Tactic: rw [this, map_one, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
refine_1 :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
refine_1₁ :
  Eq.{u_1 + 1} (α := (↑X : Type u_1)) (1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have refine_1₂ : Eq.{u_1 + 1} (α := (↑X : Type u_1)) 1 1
Tactic: rw [this, map_one, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Zero (goal)
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : X ⟶ G
⊢ f = default
have refine_2 : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑G : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.GrpWithZero (goal)
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
⊢ CategoryStruct.comp (Y := β) (ofHom (↑e : α.carrier →*₀ β.carrier)) (ofHom (↑e.symm : β.carrier →*₀ α.carrier)) = 𝟙 α
have h : ∀ (x : α.carrier),
  Eq (α := α.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := α)
            (Y := α)
            (CategoryStruct.comp (Y := β) (ofHom (↑e : α.carrier →*₀ β.carrier))
              (ofHom (↑e.symm : β.carrier →*₀ α.carrier))) :
          (a : α.carrier) → α.carrier)
        x :
      α.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 α) :
          (a : α.carrier) → α.carrier)
        x :
      α.carrier)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.GrpWithZero (goal)
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
⊢ CategoryStruct.comp (Y := α) (ofHom (↑e.symm : β.carrier →*₀ α.carrier)) (ofHom (↑e : α.carrier →*₀ β.carrier)) = 𝟙 β
have h : ∀ (x : β.carrier),
  Eq (α := β.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := β)
            (Y := β)
            (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : β.carrier →*₀ α.carrier))
              (ofHom (↑e : α.carrier →*₀ β.carrier))) :
          (a : β.carrier) → β.carrier)
        x :
      β.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 β) :
          (a : β.carrier) → β.carrier)
        x :
      β.carrier)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.AB (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
X Y : ModuleCat.{v, u} R
f g : X ⟶ Y
h : ∀ (G : ModuleCat.{v, u} R), ObjectProperty.singleton (of R (Shrink.{v, u} R)) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
have h₁ : ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R),
  Eq (α := (↑Y : Type v))
    ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v))
        ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
      (↑Y : Type v))
    ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v))
        ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
      (↑Y : Type v))
Tactic: simp only [ObjectProperty.singleton_iff, ModuleCat.hom_ext_iff, hom_comp,
    LinearMap.ext_iff, LinearMap.coe_comp, Function.comp_apply, forall_eq'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.AB (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
X Y : ModuleCat.{v, u} R
f g : X ⟶ Y
h :
  ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R),
    Eq (α := (↑Y : Type v))
      ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
      ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
⊢ f = g
have hf : ∀ (x : (↑X : Type v)),
  Eq (α := (↑Y : Type v)) ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
    ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Abelian (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
hf : Mono f
⊢ (LinearEquiv.toModuleIso
          (((Hom.hom f).ker.quotEquivOfEqBot ⋯).symm ≪≫ₗ
            ((Hom.hom f).quotKerEquivRange ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker ⋯))).hom ≫
      Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ)) =
    f
have hf₁ : ∀ (x : (↑(of R (↑M : Type v)) : Type v)),
  Eq (α := (↑N : Type v))
    ((Hom.hom
            ((LinearEquiv.toModuleIso
                  (((Hom.hom f).ker.quotEquivOfEqBot sorry).symm ≪≫ₗ
                    ((Hom.hom f).quotKerEquivRange ≪≫ₗ
                      LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker sorry))).hom ≫
              Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ))) :
          (a : (↑(of R (↑M : Type v)) : Type v)) → (↑N : Type v))
        x :
      (↑N : Type v))
    ((Hom.hom f : (a : (↑(of R (↑M : Type v)) : Type v)) → (↑N : Type v)) x : (↑N : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Abelian (goal)
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
hf : Epi f
⊢ Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
      (LinearEquiv.toModuleIso
          ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker ⋯ ≪≫ₗ
              (Hom.hom f).quotKerEquivRange ≪≫ₗ
            LinearEquiv.ofTop (Hom.hom f).range ⋯)).hom =
    f
have hf₁ : ∀ (x : (↑M : Type v)),
  Eq (α := (↑(of R (↑N : Type v)) : Type v))
    ((Hom.hom
            (Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
              (LinearEquiv.toModuleIso
                  ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker sorry ≪≫ₗ
                      (Hom.hom f).quotKerEquivRange ≪≫ₗ
                    LinearEquiv.ofTop (Hom.hom f).range sorry)).hom) :
          (a : (↑M : Type v)) → (↑(of R (↑N : Type v)) : Type v))
        x :
      (↑(of R (↑N : Type v)) : Type v))
    ((Hom.hom f : (a : (↑M : Type v)) → (↑(of R (↑N : Type v)) : Type v)) x : (↑(of R (↑N : Type v)) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
⊢ Eq (α := (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (freeDesc f) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))
        x :
      (fun (X : Type u) ↦ X) (↑M : Type u))
have dsimp : Eq (α := (↑M : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
          Functor.obj (free R) X) (Y := M)
          (↟((Finsupp.lift (↑M : Type u) R X : (a : X → (↑M : Type u)) → (X →₀ R) →ₗ[R] (↑M : Type u))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → (↑M : Type u)))) :
        (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
      (freeMk x) :
    (↑M : Type u))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u))
Tactic: dsimp [freeDesc]