awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
e_a :
  f = (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫ Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g)
⊢ Eq (α := G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (G.map { base := f, fiber := g : X.Hom Y } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
    (CategoryStruct.comp (Y := colimit (J := (↑(F.obj Y.base) : Type u_1)) (Grothendieck.ι F Y.base ⋙ G))
        (CategoryStruct.comp (Y := obj (Grothendieck.ι F Y.base ⋙ G) Y.fiber)
          (G.map (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber ≫ map (Grothendieck.ι F Y.base) g))
          (colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber))
        (c.ι.app Y.base) :
      G.obj X ⟶ c.pt)
have e_a₁ : HEq g (β :=
  obj
      (Cat.Hom.toFunctor
        (F.map
          ((NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).base ≫
            Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g))))
      { base := X.base, fiber := X.fiber : Grothendieck F }.fiber ⟶
    (obj (Grothendieck.ι F Y.base) Y.fiber).fiber)
  (eqToHom sorry ≫
    map (Cat.Hom.toFunctor (F.map (Grothendieck.Hom.base (map (Grothendieck.ι F Y.base) g))))
        (NatTrans.app (Grothendieck.ιNatTrans f) X.fiber).fiber ≫
      Grothendieck.Hom.fiber (map (Grothendieck.ι F Y.base) g))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
hm : ∀ (j : Grothendieck F), (coconeOfCoconeFiberwiseColimit c).ι.app j ≫ m = s.ι.app j
X : C
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc
        { pt := s.pt,
          ι :=
            { app := fun (X : C) ↦ colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s),
              naturality := ⋯ } }
have simp : c.ι.app X ≫ m = colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)
Tactic: simp only [fiberwiseColimit_obj, Functor.const_obj_obj, IsColimit.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
hm : ∀ (j : Grothendieck F), (coconeOfCoconeFiberwiseColimit c).ι.app j ≫ m = s.ι.app j
X : C
⊢ c.ι.app X ≫ m = colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)
have hm₁ : ∀ (j : Grothendieck F),
  CategoryStruct.comp (Y := colimit (J := (↑(F.obj j.base) : Type u_1)) (Grothendieck.ι F j.base ⋙ G))
      (colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber) (c.ι.app j.base ≫ m) =
    s.ι.app j
Tactic: simp only [coconeOfCoconeFiberwiseColimit_pt, Functor.const_obj_obj,
      coconeOfCoconeFiberwiseColimit_ι_app, Category.assoc] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
X : C
hm :
  ∀ (j : Grothendieck F),
    CategoryStruct.comp (Y := colimit (J := (↑(F.obj j.base) : Type u_1)) (Grothendieck.ι F j.base ⋙ G))
        (colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber) (c.ι.app j.base ≫ m) =
      s.ι.app j
⊢ c.ι.app X ≫ m = colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)
have w : ∀ (d : (↑(F.obj X) : Type u_1)),
  colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ c.ι.app X ≫ m =
    CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s))
Tactic: ext d
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst_3 : HasColimit (fiberwiseColimit G)
X : Grothendieck F
⊢ Eq (α := G.obj X ⟶ colimit (fiberwiseColimit G)) (colimit.ι G X ≫ Iso.inv (colimitFiberwiseColimitIso G))
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base)
have rw : Eq (α := G.obj X ⟶ colimit G) (colimit.ι G X : G.obj X ⟶ colimit G)
  (CategoryStruct.comp (Y := colimit (fiberwiseColimit G))
      (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base)
      (Iso.hom (colimitFiberwiseColimitIso G)) :
    G.obj X ⟶ colimit G)
Tactic: rw [Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
⊢ Eq (α := obj (fiberwiseColim F H ⋙ colim) X ⟶ obj colim Y)
    (map (fiberwiseColim F H ⋙ colim) x ≫
      Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) Y))
    (Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) X) ≫
      map colim x)
have w : ∀ (j : C),
  Eq (α := (obj (fiberwiseColim F H) X).obj j ⟶ obj colim Y)
    (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
      (map (fiberwiseColim F H ⋙ colim) x ≫
        Iso.hom
          ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
            Y)))
    (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
      (Iso.hom
          ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
            X) ≫
        map colim x))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
j : C
⊢ Eq (α := (obj (fiberwiseColim F H) X).obj j ⟶ obj colim Y)
    (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
      (map (fiberwiseColim F H ⋙ colim) x ≫
        Iso.hom
          ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
            Y)))
    (CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
      (Iso.hom
          ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
            X) ≫
        map colim x))
have w : ∀ (j_1 : (↑(F.obj j) : Type u_1)),
  Eq (α := (Grothendieck.ι F j ⋙ X).obj j_1 ⟶ obj colim Y)
    (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
      CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (map (fiberwiseColim F H ⋙ colim) x ≫
          Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              Y)))
    (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
      CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              X) ≫
          map colim x))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ (c : C), HasColimitsOfShape.{u_2, u_1, v₂, u₂} (↑(F.obj c) : Type u_1) H
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
X Y : Grothendieck F ⥤ H
x : X ⟶ Y
⊢ Eq (α := obj (fiberwiseColim F H ⋙ colim) X ⟶ obj colim Y)
    (map (fiberwiseColim F H ⋙ colim) x ≫
      Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) Y))
    (Iso.hom
        ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G)) X) ≫
      map colim x)
have w : ∀ (j : C) (j_1 : (↑(F.obj j) : Type u_1)),
  Eq (α := (Grothendieck.ι F j ⋙ X).obj j_1 ⟶ obj colim Y)
    (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
      CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (map (fiberwiseColim F H ⋙ colim) x ≫
          Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              Y)))
    (colimit.ι (Grothendieck.ι F j ⋙ X) j_1 ≫
      CategoryStruct.comp (Y := colimit (obj (fiberwiseColim F H) X)) (colimit.ι (obj (fiberwiseColim F H) X) j)
        (Iso.hom
            ((fun (G : Grothendieck F ⥤ H) ↦ (colimitFiberwiseColimitIso G : colimit (fiberwiseColimit G) ≅ colimit G))
              X) ≫
          map colim x))
Tactic: iterate 2 apply colimit.hom_ext; intro
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hI : F.I = F'.I
hm : F.m = eqToHom hI ≫ F'.m
⊢ F = F'
have obtain : ∀ (I : C) (Fm : I ⟶ Y) [m_mono : Mono Fm] (e : X ⟶ I) (Ffac : e ≫ Fm = f)
  (hI : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I = F'.I)
  (hm : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m = eqToHom hI ≫ F'.m),
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } = F'
Tactic: obtain ⟨_, Fm, _, Ffac⟩ := F
Cleared hypotheses: F, hI, hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
hI : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I = F'.I
hm : { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m = eqToHom hI ≫ F'.m
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } = F'
have obtain : ∀ (I_1 : C) (Fm' : I_1 ⟶ Y) [m_mono_1 : Mono Fm'] (e_1 : X ⟶ I_1) (Ffac' : e_1 ≫ Fm' = f)
  (hI :
    { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I =
      { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.I)
  (hm :
    { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
      eqToHom hI ≫ { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m),
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }
Tactic: obtain ⟨_, Fm', _, Ffac'⟩ := F'
Cleared hypotheses: F', hI, hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
I_1 : C
Fm' : I_1 ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I_1
Ffac' : e_1 ≫ Fm' = f
hI :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.I =
    { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.I
hm :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
    eqToHom hI ≫ { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I_1, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }
have refl : ∀ (Fm' : I ⟶ Y) [m_mono_2 : Mono Fm'] (e_2 : X ⟶ I) (Ffac' : e_2 ≫ Fm' = f)
  (hm :
    { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
      eqToHom sorry ≫ { I := I, m := Fm', m_mono := m_mono_2, e := e_2, fac := Ffac' : MonoFactorisation f }.m),
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I, m := Fm', m_mono := m_mono_2, e := e_2, fac := Ffac' }
Tactic: cases hI
Cleared hypotheses: I_1, Fm', m_mono_1, e_1, Ffac', hI, hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm :
  { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f }.m =
    eqToHom ⋯ ≫ { I := I, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' : MonoFactorisation f }.m
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }
have hm₁ : Fm = Fm'
Tactic: replace hm : Fm = Fm' := by simpa using hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
⊢ { I := I, m := Fm, m_mono := m_mono, e := e, fac := Ffac : MonoFactorisation f } =
    { I := I, m := Fm', m_mono := m_mono_1, e := e_1, fac := Ffac' }
have refl : e = e_1
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
⊢ e = e_1
have refl : e ≫ Fm = e_1 ≫ Fm
Tactic: apply (cancel_mono Fm).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
⊢ e ≫ Fm = e_1 ≫ Fm
have refl : f = e_1 ≫ Fm
Tactic: rw [Ffac, hm, Ffac']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
refl : f = e_1 ≫ Fm
⊢ e ≫ Fm = e_1 ≫ Fm
have refl₁ : f = e_1 ≫ Fm'
Tactic: rw [Ffac, hm, Ffac']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
I : C
Fm : I ⟶ Y
m_mono : Mono Fm
e : X ⟶ I
Ffac : e ≫ Fm = f
Fm' : I ⟶ Y
m_mono_1 : Mono Fm'
e_1 : X ⟶ I
Ffac' : e_1 ≫ Fm' = f
hm : Fm = Fm'
refl : f = e_1 ≫ Fm
refl₁ : f = e_1 ≫ Fm'
⊢ e ≫ Fm = e_1 ≫ Fm
have refl₂ : f = f
Tactic: rw [Ffac, hm, Ffac']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono m
have rw : Mono F.m
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
F' : MonoFactorisation f
⊢ Mono (X := image f) (lift F')
have refine : Mono (X := image f) (lift F' ≫ F'.m)
Tactic: refine @mono_of_mono _ _ _ _ _ _ F'.m ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Eq (α := image f ⟶ Y) (Iso.hom (imageMonoIsoSource f) ≫ f : image f ⟶ Y) (image.ι f : image f ⟶ Y)
have simp : Eq (α := image f ⟶ Y)
  (Iso.hom (imageMonoIsoSource f) ≫
      CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) :
    image f ⟶ Y)
  (image.ι f : image f ⟶ Y)
Tactic: simp only [← imageMonoIsoSource_inv_ι f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Eq (α := image f ⟶ Y)
    (Iso.hom (imageMonoIsoSource f) ≫
        CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
have rw : Eq (α := image f ⟶ Y)
  (CategoryStruct.comp (Y := image f)
      (Iso.hom (imageMonoIsoSource f) ≫ Iso.inv (imageMonoIsoSource f) : image f ⟶ image f) (image.ι f : image f ⟶ Y) :
    image f ⟶ Y)
  (image.ι f : image f ⟶ Y)
Tactic: rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
rw :
  Eq (α := image f ⟶ Y)
    (CategoryStruct.comp (Y := image f)
        (Iso.hom (imageMonoIsoSource f) ≫ Iso.inv (imageMonoIsoSource f) : image f ⟶ image f)
        (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
⊢ Eq (α := image f ⟶ Y)
    (Iso.hom (imageMonoIsoSource f) ≫
        CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
have rw₁ : 𝟙 (image f) ≫ image.ι f = image.ι f
Tactic: rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
rw :
  Eq (α := image f ⟶ Y)
    (CategoryStruct.comp (Y := image f)
        (Iso.hom (imageMonoIsoSource f) ≫ Iso.inv (imageMonoIsoSource f) : image f ⟶ image f)
        (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
rw₁ : 𝟙 (image f) ≫ image.ι f = image.ι f
⊢ Eq (α := image f ⟶ Y)
    (Iso.hom (imageMonoIsoSource f) ≫
        CategoryStruct.comp (Y := image f) (Iso.inv (imageMonoIsoSource f) : X ⟶ image f) (image.ι f : image f ⟶ Y) :
      image f ⟶ Y)
    (image.ι f : image f ⟶ Y)
have rw₂ : Eq (α := image f ⟶ Y) (image.ι f) (image.ι f)
Tactic: rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
⊢ g = h
have t₀ : v ≫ q ≫ ι f = ι f
Tactic: have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = ι f
have h₁ : (v ≫ q) ≫ ι f = v ≫ q ≫ ι f
Tactic: convert! t₀ using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = v ≫ q ≫ ι f
have h₁ : v ≫ q ≫ ι f = v ≫ q ≫ ι f
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ g = h
have t : v ≫ q = 𝟙 (image f)
Tactic: have t : v ≫ q = 𝟙 (image f) :=
    (cancel_mono_id (image.ι f)).1
      (by
        convert! t₀ using 1
        rw [Category.assoc])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = 𝟙 (image f) ≫ g
have rw : g = g
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ g = v ≫ q ≫ g
have rw : (v ≫ q) ≫ g = v ≫ q ≫ g
Tactic: rw [← t, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
W : C
g h : image f ⟶ W
inst_2 : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
rw : (v ≫ q) ≫ g = v ≫ q ≫ g
⊢ 𝟙 (image f) ≫ g = v ≫ q ≫ g
have rw₁ : v ≫ q ≫ g = v ≫ q ≫ g
Tactic: rw [← t, Category.assoc]