awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
mp :
  Mono f →
    Mono (X :=
      Functor.obj.{v, w, u, w + 1}
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        X)
      (Functor.map
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        f)
⊢ Mono f ↔
    Mono (X :=
      Functor.obj.{v, w, u, w + 1}
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        X)
      (Functor.map
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        f)
have mpr : Mono (X :=
    Functor.obj.{v, w, u, w + 1}
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      X)
    (Functor.map
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      f) →
  Mono f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔
    Function.Injective.{w + 1, w + 1} (α := CC X) (β := CC Y)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
have simp : Mono (X :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          X) :
      Type w))
    (Y :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          Y) :
      Type w))
    (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj.{v, w, u, w + 1}
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              X)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              f)) :
        (a : (↑((forget₂ C Ab).obj X) : Type w)) → (↑((forget₂ C Ab).obj Y) : Type w))) ↔
  Mono.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
Tactic: simp only [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔
    Function.Surjective (α :=
      (↑(Functor.obj.{v, w, u, w + 1}
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            X) :
        Type w))
      (β :=
      (↑(Functor.obj.{v, w, u, w + 1}
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            Y) :
        Type w))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj.{v, w, u, w + 1}
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              X)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              f)) :
        (a : (↑((forget₂ C Ab).obj X) : Type w)) → (↑((forget₂ C Ab).obj Y) : Type w))
have rw : Epi f ↔
  Epi (X :=
    Functor.obj.{v, w, u, w + 1}
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      X)
    (Functor.map
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      f)
Tactic: rw [← AddCommGrpCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔
    Epi (X :=
      Functor.obj.{v, w, u, w + 1}
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        X)
      (Functor.map
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        f)
have mp : Epi f →
  Epi (X :=
    Functor.obj.{v, w, u, w + 1}
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      X)
    (Functor.map
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
mp :
  Epi f →
    Epi (X :=
      Functor.obj.{v, w, u, w + 1}
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        X)
      (Functor.map
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        f)
⊢ Epi f ↔
    Epi (X :=
      Functor.obj.{v, w, u, w + 1}
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        X)
      (Functor.map
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        f)
have mpr : Epi (X :=
    Functor.obj.{v, w, u, w + 1}
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      X)
    (Functor.map
      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      f) →
  Epi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_7 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔
    Function.Surjective.{w + 1, w + 1} (α := CC X) (β := CC Y)
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
have simp : Epi (X :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          X) :
      Type w))
    (Y :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          Y) :
      Type w))
    (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj.{v, w, u, w + 1}
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              X)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              f)) :
        (a : (↑((forget₂ C Ab).obj X) : Type w)) → (↑((forget₂ C Ab).obj Y) : Type w))) ↔
  Epi.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
Tactic: simp only [epi_iff_surjective, ← CategoryTheory.ofHom_epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
S : ShortComplex.{v, u} C
inst_7 : HasZeroObject.{v, u} C
hS : S.ShortExact
⊢ Function.Injective (α :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          S.X₁) :
      Type w))
    (β :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          S.X₂) :
      Type w))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (X :=
          Functor.obj.{v, w, u, w + 1}
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            S.X₁)
          (Functor.map
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            S.f)) :
      (a : (↑((forget₂ C Ab).obj S.X₁) : Type w)) → (↑((forget₂ C Ab).obj S.X₂) : Type w))
have rw : Mono S.f
Tactic: rw [← Preadditive.mono_iff_injective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
S : ShortComplex.{v, u} C
inst_7 : HasZeroObject.{v, u} C
hS : S.ShortExact
⊢ Function.Surjective (α :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          S.X₂) :
      Type w))
    (β :=
    (↑(Functor.obj.{v, w, u, w + 1}
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
            (CD := AddCommGrpCat.carrier))
          S.X₃) :
      Type w))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (X :=
          Functor.obj.{v, w, u, w + 1}
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            S.X₂)
          (Functor.map
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            S.g)) :
      (a : (↑((forget₂ C Ab).obj S.X₂) : Type w)) → (↑((forget₂ C Ab).obj S.X₃) : Type w))
have rw : Epi S.g
Tactic: rw [← Preadditive.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
⊢ Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁) x₃ : CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₂₃.τ₁ : (a : CC D.L₂.X₁) → CC D.L₃.X₁) x₁ : CC D.L₃.X₁)
have this : PreservesFiniteLimits
  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
    AddCommGrpCat.carrier))
Tactic: have := (forget₂ C Ab).preservesFiniteLimits_of_preservesHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
⊢ PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
have this₁ : Eq (α := C ⥤ Type v)
  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
      AddCommGrpCat.carrier) ⋙
    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier))
  (forget C (FC := FC) (CC := CC))
Tactic: have : forget₂ C Ab ⋙ forget Ab = forget C := HasForget₂.forget_comp