awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ v ≫ q ≫ g = v ≫ q ≫ h
have rw : v ≫ equalizer.ι g h ≫ h = v ≫ q ≫ h
Tactic: rw [equalizer.condition g h]
-- 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)
⊢ v ≫ q ≫ h = 𝟙 (image f) ≫ h
have rw : (v ≫ q) ≫ h = 𝟙 (image f) ≫ h
Tactic: rw [← Category.assoc, t]
-- 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) ≫ h = 𝟙 (image f) ≫ h
⊢ v ≫ q ≫ h = 𝟙 (image f) ≫ h
have rw₁ : 𝟙 (image f) ≫ h = 𝟙 (image f) ≫ h
Tactic: rw [← Category.assoc, t]
-- 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) ≫ h = h
have rw : h = h
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)
⊢ g = h
have g₁ : g = 𝟙 (image f) ≫ g
Tactic: calc
    g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by 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)
g₁ : g = 𝟙 (image f) ≫ g
⊢ g = h
have g₂ : 𝟙 (image f) ≫ g = v ≫ q ≫ g
Tactic: calc
    g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by 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)
g₁ : g = 𝟙 (image f) ≫ g
g₂ : 𝟙 (image f) ≫ g = v ≫ q ≫ g
⊢ g = h
have g₃ : v ≫ q ≫ g = v ≫ q ≫ h
Tactic: calc
    g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by 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)
g₁ : g = 𝟙 (image f) ≫ g
g₂ : 𝟙 (image f) ≫ g = v ≫ q ≫ g
g₃ : v ≫ q ≫ g = v ≫ q ≫ h
⊢ g = h
have g₄ : v ≫ q ≫ h = 𝟙 (image f) ≫ h
Tactic: calc
    g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by 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)
g₁ : g = 𝟙 (image f) ≫ g
g₂ : 𝟙 (image f) ≫ g = v ≫ q ≫ g
g₃ : v ≫ q ≫ g = v ≫ q ≫ h
g₄ : v ≫ q ≫ h = 𝟙 (image f) ≫ h
⊢ g = h
have g₅ : 𝟙 (image f) ≫ h = h
Tactic: calc
    g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by rw [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
E : Epi f
⊢ Epi (X := image f) (image.ι f)
have E₁ : Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
Tactic: rw [← image.fac f] at E
Cleared hypotheses: E
-- 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
inst_2 : Epi (X := image f) (image.ι f)
inst_3 : Epi (Y := image f) (factorThruImage f)
⊢ Epi f
have rw : Epi (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
Tactic: rw [← image.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 f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
⊢ CategoryStruct.comp (Y := image f') (factorThruImage f') (ι f') = f
have rw : CategoryStruct.comp (Y := image f') (factorThruImage f') (ι f') = f'
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
⊢ CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f') (image.eqToHom h) (image.eqToHom ⋯))
      (image.ι f) =
    𝟙 (image f) ≫ image.ι f
have subst : ∀ [inst_3 : HasImage f],
  CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f) (image.eqToHom sorry) (image.eqToHom sorry))
      (image.ι f) =
    𝟙 (image f) ≫ image.ι f
Tactic: subst h
Cleared hypotheses: f', inst_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
h : f = f'
⊢ CategoryStruct.comp (Y := image f') (CategoryStruct.comp (Y := image f) (image.eqToHom ⋯) (image.eqToHom h))
      (image.ι f') =
    𝟙 (image f') ≫ image.ι f'
have subst : ∀ [inst_3 : HasImage f],
  CategoryStruct.comp (Y := image f) (CategoryStruct.comp (Y := image f) (image.eqToHom sorry) (image.eqToHom sorry))
      (image.ι f) =
    𝟙 (image f) ≫ image.ι f
Tactic: subst h
Cleared hypotheses: f', inst_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
inst_3 : HasEqualizers.{v, u} C
h : f = f'
⊢ Eq (α := image f ⟶ Y) (ι f) (CategoryStruct.comp (Y := image f') (Iso.hom (eqToIso h)) (ι f'))
have w : CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
  CategoryStruct.comp (Y := image f) (factorThruImage f)
    (CategoryStruct.comp (Y := image f') (Iso.hom (eqToIso h)) (ι f'))
Tactic: apply image.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst_1 : HasImage f
inst_2 : HasImage f'
inst_3 : HasEqualizers.{v, u} C
h : f = f'
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
    CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image f') (Iso.hom (eqToIso h)) (ι f'))
have w : ∀ [inst_4 : HasImage f],
  CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f) =
    CategoryStruct.comp (Y := image f) (factorThruImage f)
      (CategoryStruct.comp (Y := image f) (Iso.hom (eqToIso sorry)) (ι f))
Tactic: subst h
Cleared hypotheses: f', inst_2, h
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasImage g
inst_2 : HasImage (f ≫ g)
⊢ Mono (X := image (f ≫ g)) (Y := image g) (preComp f g)
have refine : Mono (X := image (f ≫ g)) (CategoryStruct.comp (Y := image g) (preComp f g) (ι g))
Tactic: refine @mono_of_mono _ _ _ _ _ _ (image.ι g) ?_
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasImage g
inst_2 : HasImage (f ≫ g)
⊢ Mono (X := image (f ≫ g)) (CategoryStruct.comp (Y := image g) (preComp f g) (ι g))
have simp : Mono (X := image (f ≫ g)) (ι (f ≫ g))
Tactic: simp only [image.preComp_ι]
-- 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
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst_1 : HasImage (g ≫ h)
inst_2 : HasImage (f ≫ g ≫ h)
inst_3 : HasImage h
inst_4 : HasImage ((f ≫ g) ≫ h)
⊢ Eq (α := image (f ≫ g ≫ h) ⟶ image h) (CategoryStruct.comp (Y := image (g ≫ h)) (preComp f (g ≫ h)) (preComp g h))
    (CategoryStruct.comp (Y := image ((f ≫ g) ≫ h)) (eqToHom ⋯) (preComp (f ≫ g) h))
have apply : Eq (α := image (f ≫ g ≫ h) ⟶ W)
  (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image (g ≫ h)) (preComp f (g ≫ h)) (preComp g h))
    (ι h))
  (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image ((f ≫ g) ≫ h)) (eqToHom sorry) (preComp (f ≫ g) h))
    (ι h))
Tactic: apply (cancel_mono (image.ι h)).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
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst_1 : HasImage (g ≫ h)
inst_2 : HasImage (f ≫ g ≫ h)
inst_3 : HasImage h
inst_4 : HasImage ((f ≫ g) ≫ h)
⊢ Eq (α := image (f ≫ g ≫ h) ⟶ W)
    (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image (g ≫ h)) (preComp f (g ≫ h)) (preComp g h))
      (ι h))
    (CategoryStruct.comp (Y := image h) (CategoryStruct.comp (Y := image ((f ≫ g) ≫ h)) (eqToHom ⋯) (preComp (f ≫ g) h))
      (ι h))
have simp : Eq (α := image (f ≫ g ≫ h) ⟶ W) (ι (f ≫ g ≫ h))
  (lift
      { I := image ((f ≫ g) ≫ h), m := ι ((f ≫ g) ≫ h), m_mono := sorry, e := factorThruImage ((f ≫ g) ≫ h), fac := sorry :
        MonoFactorisation (f ≫ g ≫ h) } ≫
    ι ((f ≫ g) ≫ h))
Tactic: simp only [preComp, Category.assoc, fac, lift_mk_comp, eqToHom]
-- 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
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst_1 : HasImage (g ≫ h)
inst_2 : HasImage (f ≫ g ≫ h)
inst_3 : HasImage h
inst_4 : HasImage ((f ≫ g) ≫ h)
⊢ Eq (α := image (f ≫ g ≫ h) ⟶ W) (ι (f ≫ g ≫ h))
    (lift
        { I := image ((f ≫ g) ≫ h), m := ι ((f ≫ g) ≫ h), m_mono := ⋯, e := factorThruImage ((f ≫ g) ≫ h), fac := ⋯ :
          MonoFactorisation (f ≫ g ≫ h) } ≫
      ι ((f ≫ g) ≫ h))
have rw : Eq (α := image (f ≫ g ≫ h) ⟶ W) (ι (f ≫ g ≫ h)) (ι (f ≫ g ≫ h))
Tactic: rw [image.lift_fac]
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage g
inst_3 : HasImage (f ≫ g)
inst_4 : Epi f
⊢ Epi (X := image (f ≫ g)) (Y := image g) (preComp f g)
have apply : Epi (Y := image g) (f ≫ factorThruImage g)
Tactic: apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = ((Image.monoFactorisation g).isoComp f).m
have dsimp : Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m) (image.ι g)
Tactic: dsimp
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m) (image.ι g)
have this : (MonoFactorisation.ofIsoComp f F').m = F'.m
Tactic: have : (MonoFactorisation.ofIsoComp f F').m = F'.m := rfl
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
⊢ Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m) (image.ι g)
have rw : Eq (α := (Image.monoFactorisation g).I ⟶ Z)
  (image.lift (MonoFactorisation.ofIsoComp f F') ≫ (MonoFactorisation.ofIsoComp f F').m) (image.ι g)
Tactic: rw [← this, image.lift_fac (MonoFactorisation.ofIsoComp f 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : IsIso f
inst_3 : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
rw :
  Eq (α := (Image.monoFactorisation g).I ⟶ Z)
    (image.lift (MonoFactorisation.ofIsoComp f F') ≫ (MonoFactorisation.ofIsoComp f F').m) (image.ι g)
⊢ Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m) (image.ι g)
have rw₁ : Eq (α := (Image.monoFactorisation g).I ⟶ Z) (image.ι g) (image.ι g)
Tactic: rw [← this, image.lift_fac (MonoFactorisation.ofIsoComp f 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_1 : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : IsIso f
inst_3 : HasImage g
⊢ CategoryStruct.comp (Y := image g) (preComp f g)
      (lift { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ }) =
    𝟙 (image (f ≫ g))
have w : CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g))
    (CategoryStruct.comp (Y := image g) (preComp f g)
      (lift
        { I := image (f ≫ g), m := ι (f ≫ g), m_mono := sorry, e := inv f ≫ factorThruImage (f ≫ g), fac := sorry :
          MonoFactorisation g })) =
  factorThruImage (f ≫ g) ≫ 𝟙 (image (f ≫ g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
f : X ⟶ Y
inst_2 : IsIso f
inst_3 : HasImage g
⊢ lift
        { I := image (f ≫ g), m := ι (f ≫ g), m_mono := ⋯, e := inv f ≫ factorThruImage (f ≫ g), fac := ⋯ :
          MonoFactorisation g } ≫
      preComp f g =
    𝟙 (image g)
have w : CategoryStruct.comp (Y := image g) (factorThruImage g)
    (lift
        { I := image (f ≫ g), m := ι (f ≫ g), m_mono := sorry, e := inv f ≫ factorThruImage (f ≫ g), fac := sorry :
          MonoFactorisation g } ≫
      preComp f g) =
  factorThruImage g ≫ 𝟙 (image g)
Tactic: ext
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift F'.ofCompIso ≫ F'.m = ((Image.monoFactorisation f).compMono g).m
have rw : ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m
Tactic: rw [← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m),
            ← IsIso.inv_hom_id g, ← 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m
have refine : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
Tactic: refine congrArg (· ≫ g) ?_
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
have this : Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)
Tactic: have : (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
            image.lift (MonoFactorisation.ofCompIso F') ≫
            ((MonoFactorisation.ofCompIso F').m) := by
              simp only [MonoFactorisation.ofCompIso_I, Category.assoc,
                MonoFactorisation.ofCompIso_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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
this : Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
have rw : image.lift F'.ofCompIso ≫ F'.ofCompIso.m = (Image.monoFactorisation f).m
Tactic: rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι]
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
this : Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)
rw : image.lift F'.ofCompIso ≫ F'.ofCompIso.m = (Image.monoFactorisation f).m
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
have rw₁ : image.ι f = (Image.monoFactorisation f).m
Tactic: rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι]
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
F' : MonoFactorisation (f ≫ g)
this : Eq (α := image f ⟶ Y) ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) (image.lift F'.ofCompIso ≫ F'.ofCompIso.m)
rw : image.lift F'.ofCompIso ≫ F'.ofCompIso.m = (Image.monoFactorisation f).m
rw₁ : image.ι f = (Image.monoFactorisation f).m
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
have rw₂ : Eq (α := image f ⟶ Y) (image.ι f) (image.ι f)
Tactic: rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι]
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
⊢ Eq (α := image f ⟶ Z)
    (CategoryStruct.comp (Y := image (f ≫ g)) (Iso.hom (compIso f g) : image f ⟶ image (f ≫ g))
      (ι (f ≫ g) : image (f ≫ g) ⟶ Z))
    (ι f ≫ g)
have w : CategoryStruct.comp (Y := image f) (factorThruImage f)
    (CategoryStruct.comp (Y := image (f ≫ g)) (Iso.hom (compIso f g) : image f ⟶ image (f ≫ g))
      (ι (f ≫ g) : image (f ≫ g) ⟶ Z)) =
  CategoryStruct.comp (Y := image f) (factorThruImage f) (ι f ≫ g)
Tactic: ext
-- 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
Z : C
g : Y ⟶ Z
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasImage f
inst_3 : IsIso g
⊢ Eq (α := image (f ≫ g) ⟶ Y) (CategoryStruct.comp (Y := image f) (Iso.inv (compIso f g)) (ι f) : image (f ≫ g) ⟶ Y)
    (ι (f ≫ g) ≫ inv g : image (f ≫ g) ⟶ Y)
have w : CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g) : X ⟶ image (f ≫ g))
    (CategoryStruct.comp (Y := image f) (Iso.inv (compIso f g)) (ι f) : image (f ≫ g) ⟶ Y) =
  CategoryStruct.comp (Y := image (f ≫ g)) (factorThruImage (f ≫ g)) (ι (f ≫ g) ≫ inv g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : IsIso sq
⊢ Eq (α := image f.hom ⟶ g.right) (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom)
    (image.ι f.hom ≫ Arrow.Hom.right sq)
have erw : Eq (α := image f.hom ⟶ f.right)
  ((image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom) ≫ Arrow.Hom.right (inv sq))
  ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
Tactic: erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m,
          image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right,
          Category.comp_id]