awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
j : κ.ord.ToType
hj : ¬IsMax j
this :
  pushouts
    (coproducts.{w, v, u}
      (ofHoms (ι := (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (homFamily (generatingMonomorphisms G))))
    (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
⊢ monomorphisms C (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
have this₁ : pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)) (Y :=
  hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
          (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
    (Order.succ j))
  (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
          (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
    (homOfLE sorry))
Tactic: simp only [ofHoms_homFamily] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
j : κ.ord.ToType
hj : ¬IsMax j
this :
  pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)) (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
⊢ monomorphisms C (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
have refine : LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))) (monomorphisms C)
Tactic: refine (?_ : _ ≤ monomorphisms C) _ this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
j : κ.ord.ToType
hj : ¬IsMax j
this :
  pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)) (Y :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.obj
      (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
            (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F.map
      (homOfLE ⋯))
⊢ LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))) (monomorphisms C)
have simp : LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)
Tactic: simp only [pushouts_le_iff, coproducts_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
⊢ PreservesColimit
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
        (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F
    (Functor.obj coyoneda (Opposite.op A))
have this₁ : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
Tactic: have (j j' : κ.ord.ToType) (φ : j ⟶ j') : Mono (hf'.F.map φ) := hf'.mem_map φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
⊢ PreservesColimit
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
        (↑(toSet (generatingMonomorphisms G)) : Type (max u v))).F
    (Functor.obj coyoneda (Opposite.op A))
have hXκ : HasCardinalLT (Subobject.{v, u} A) κ
Tactic: apply preservesColimit_coyoneda_obj_of_mono (Y := hf'.F) (κ := κ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject.{v, u} G) κ
this_1 : Fact κ.IsRegular
this_2 : Nonempty.{w + 1} κ.ord.ToType
this_3 : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf :
  HomotopicalAlgebra.RelativeCellComplex (α := fun (x : κ.ord.ToType) ↦
    (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) (A :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).left) (B :=
    fun (x : κ.ord.ToType) (i : (↑(toSet (generatingMonomorphisms G)) : Type (max u v))) ↦ (↑i : Arrow C).right)
    (fun (x : κ.ord.ToType) ↦ homFamily (generatingMonomorphisms G)) f
hf' : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} (monomorphisms C) κ.ord.ToType f :=
  let __TransfiniteCompositionOfShape :=
    hf.toTransfiniteCompositionOfShape (α := fun (x : κ.ord.ToType) ↦
      (↑(toSet (generatingMonomorphisms G)) : Type (max u v)));
  MorphismProperty.TransfiniteCompositionOfShape.mk (W := monomorphisms C) __TransfiniteCompositionOfShape ⋯
this : ∀ (j j' : κ.ord.ToType) (φ : j ⟶ j'), Mono (hf'.toTransfiniteCompositionOfShape (W := monomorphisms C).F.map φ)
⊢ HasCardinalLT (Subobject.{v, u} A) κ
have hXκ : ∀ ⦃X Y : C⦄ (S : Subobject.{v, u} G), HasCardinalLT (Subobject.{v, u} (Functor.obj Subobject.underlying S)) κ
Tactic: obtain ⟨S⟩ := hi
Cleared hypotheses: A, B, i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ Eq (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)
have refine : LE.le (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)
Tactic: refine le_antisymm ?_ (le_llp_rlp _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C) (llp (rlp (monomorphisms C))) (monomorphisms C)
have rw : LE.le (α := MorphismProperty.{v, u} C)
  (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
  (monomorphisms C)
Tactic: rw [← generatingMonomorphisms_rlp hG, llp_rlp_of_hasSmallObjectArgument]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (monomorphisms C)
have trans : LE.le (α := MorphismProperty.{v, u} C)
  (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
  (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C)))))
Tactic: trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
trans :
  LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C)))))
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (monomorphisms C)
have trans₁ : LE.le (α := MorphismProperty.{v, u} C)
  (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))) (monomorphisms C)
Tactic: trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))))
    (retracts (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C)))))
have a : LE.le (α := MorphismProperty.{v, u} C)
  (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))))
  (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))
Tactic: apply retracts_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C)
    (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G))))
    (transfiniteCompositions.{w, v, u} (pushouts (coproducts.{w, v, u} (monomorphisms C))))
have a : LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))
  (pushouts (coproducts.{w, v, u} (monomorphisms C)))
Tactic: apply transfiniteCompositions_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C) (pushouts (coproducts.{w, v, u} (generatingMonomorphisms G)))
    (pushouts (coproducts.{w, v, u} (monomorphisms C)))
have a : LE.le (α := MorphismProperty.{v, u} C) (coproducts.{w, v, u} (generatingMonomorphisms G))
  (coproducts.{w, v, u} (monomorphisms C))
Tactic: apply pushouts_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} G
⊢ LE.le (α := MorphismProperty.{v, u} C) (coproducts.{w, v, u} (generatingMonomorphisms G))
    (coproducts.{w, v, u} (monomorphisms C))
have a : LE.le (α := MorphismProperty.{v, u} C) (generatingMonomorphisms G) (monomorphisms C)
Tactic: apply coproducts_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
⊢ HasFunctorialFactorization.{v, u} (monomorphisms C) (rlp (monomorphisms C))
have hG : IsSeparator.{v, u} (separator.{v, u} C)
Tactic: have hG := isSeparator_separator C
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator.{v, u} (separator.{v, u} C)
⊢ HasFunctorialFactorization.{v, u} (monomorphisms C) (rlp (monomorphisms C))
have rw : HasFunctorialFactorization.{v, u} (llp (rlp (generatingMonomorphisms (separator.{v, u} C))))
  (rlp (generatingMonomorphisms (separator.{v, u} C)))
Tactic: rw [← generatingMonomorphisms_rlp hG, ← llp_rlp_monomorphisms hG,
    ← generatingMonomorphisms_rlp hG]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
⊢ h ≫
      pullback.fst
          (∑ a ∈ F.attach,
            Sigma.π (fun (a : ↥F) ↦ G) a ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
          (kernel.ι (d g)) ≫
        CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
          (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
            Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
          (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B) =
    0
have rw : Eq (α := G ⟶ B)
  (∑ j ∈ F.attach,
    CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
      (h ≫
          pullback.fst
              (∑ a ∈ F.attach,
                Sigma.π (fun (a : ↥F) ↦ G) a ≫
                  Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
              (kernel.ι (d g)) ≫
            Sigma.π (fun (a : ↥F) ↦ G) j ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑j : Discrete (↑M : Type v)).as :
        G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
      (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B))
  0
Tactic: rw [Preadditive.comp_sum_assoc, Preadditive.comp_sum_assoc, Preadditive.sum_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
⊢ Eq (α := G ⟶ B)
    (∑ j ∈ F.attach,
      CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
        (h ≫
            pullback.fst
                (∑ a ∈ F.attach,
                  Sigma.π (fun (a : ↥F) ↦ G) a ≫
                    Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
                (kernel.ι (d g)) ≫
              Sigma.π (fun (a : ↥F) ↦ G) j ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑j : Discrete (↑M : Type v)).as :
          G ⟶ ∐ fun (x : (↑M : Type v)) ↦ G)
        (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B))
    0
have simp : Eq (α := G ⟶ B)
  (∑ x ∈ F.attach,
    h ≫
      pullback.fst
          (∑ a ∈ F.attach,
            Sigma.π (fun (a : ↥F) ↦ G) a ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
          (kernel.ι (d g)) ≫
        Sigma.π (fun (a : ↥F) ↦ G) x ≫
          (ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (↑x : Discrete (↑M : Type v)).as)
  0
Tactic: simp only [Category.assoc, ι_d]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete (↑M : Type v))
h :
  G ⟶
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
      (kernel.ι (d g) :
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
          ∐ fun (x : (↑M : Type v)) ↦ G)
r : (x : ↥F) → (End G)ᵐᵒᵖ :=
  fun (x : ↥F) ↦
    MulOpposite.op
      (h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (x : ↥F) ↦ G) x)
⊢ Eq (α := G ⟶ B)
    (∑ x ∈ F.attach,
      h ≫
        pullback.fst
            (∑ a ∈ F.attach,
              Sigma.π (fun (a : ↥F) ↦ G) a ≫
                Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
            (kernel.ι (d g)) ≫
          Sigma.π (fun (a : ↥F) ↦ G) x ≫
            (ModuleCat.Hom.hom f : (a : (↑M : Type v)) → G ⟶ B) (↑x : Discrete (↑M : Type v)).as)
    0
have suffices : Eq (α := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
  (∑ x ∈ F.attach,
    HSMul.hSMul (β := (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)) (r x)
      ((ModuleCat.Hom.hom f : (a : (↑M : Type v)) → (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v))
          (↑x : Discrete (↑M : Type v)).as :
        (↑(ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)) : Type v)))
  0
Tactic: suffices ∑ x ∈ F.attach, r x • f.hom x.1.as = 0 by simpa [End.smul_left, r] using this