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
f g : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
sq : f ⟶ g
inst_3 : IsIso sq
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))
⊢ 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]
-- 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
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))
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))
⊢ 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.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
  ((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]
-- 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
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))
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))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv 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.ι f.hom) ((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]
-- 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
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))
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))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₃ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv 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.ι f.hom) (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]
-- 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
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))
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))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₃ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₄ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ Arrow.Hom.right sq ≫ Arrow.Hom.right (inv 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.ι f.hom) (image.ι f.hom ≫ (sq ≫ inv sq).right)
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]
-- 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
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))
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))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₃ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₄ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ Arrow.Hom.right sq ≫ Arrow.Hom.right (inv sq))
erw₅ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ (sq ≫ inv sq).right)
⊢ 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.ι f.hom) (image.ι f.hom ≫ CommaMorphism.right (𝟙 f))
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]
-- 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
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))
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))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₃ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₄ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ Arrow.Hom.right sq ≫ Arrow.Hom.right (inv sq))
erw₅ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ (sq ≫ inv sq).right)
erw₆ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ CommaMorphism.right (𝟙 f))
⊢ 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.ι f.hom) (image.ι f.hom ≫ 𝟙 f.right)
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]
-- 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
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))
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))
erw₂ :
  Eq (α := image f.hom ⟶ f.right)
    (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫
      ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)).m)
    ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₃ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) ((image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq))
erw₄ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ Arrow.Hom.right sq ≫ Arrow.Hom.right (inv sq))
erw₅ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ (sq ≫ inv sq).right)
erw₆ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ CommaMorphism.right (𝟙 f))
erw₇ : Eq (α := image f.hom ⟶ f.right) (image.ι f.hom) (image.ι f.hom ≫ 𝟙 f.right)
⊢ 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.ι f.hom) (image.ι f.hom)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
f g h : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
inst_3 : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst_4 : HasImageMap sq1
inst_5 : HasImageMap sq2
⊢ Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image h.hom)
      (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (ImageMap.map (imageMap sq2)))
      (image.ι h.hom))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
have rw : Eq (α := image f.hom ⟶ h.right)
  (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1))
    (CategoryStruct.comp (Y := image h.hom) (ImageMap.map (imageMap sq2)) (image.ι h.hom)))
  (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
Tactic: rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
f g h : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
inst_3 : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst_4 : HasImageMap sq1
inst_5 : HasImageMap sq2
rw :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1))
      (CategoryStruct.comp (Y := image h.hom) (ImageMap.map (imageMap sq2)) (image.ι h.hom)))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
⊢ Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image h.hom)
      (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (ImageMap.map (imageMap sq2)))
      (image.ι h.hom))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
have rw₁ : Eq (α := image f.hom ⟶ h.right)
  (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (image.ι g.hom ≫ Arrow.Hom.right sq2))
  (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
Tactic: rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
f g h : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
inst_3 : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst_4 : HasImageMap sq1
inst_5 : HasImageMap sq2
rw :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1))
      (CategoryStruct.comp (Y := image h.hom) (ImageMap.map (imageMap sq2)) (image.ι h.hom)))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
rw₁ :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (image.ι g.hom ≫ Arrow.Hom.right sq2))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
⊢ Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image h.hom)
      (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (ImageMap.map (imageMap sq2)))
      (image.ι h.hom))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
have rw₂ : Eq (α := image f.hom ⟶ h.right) (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
  (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
Tactic: rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
f g h : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImage g.hom
inst_3 : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst_4 : HasImageMap sq1
inst_5 : HasImageMap sq2
rw :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1))
      (CategoryStruct.comp (Y := image h.hom) (ImageMap.map (imageMap sq2)) (image.ι h.hom)))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
rw₁ :
  Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (image.ι g.hom ≫ Arrow.Hom.right sq2))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
rw₂ :
  Eq (α := image f.hom ⟶ h.right) (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
⊢ Eq (α := image f.hom ⟶ h.right)
    (CategoryStruct.comp (Y := image h.hom)
      (CategoryStruct.comp (Y := image g.hom) (ImageMap.map (imageMap sq1)) (ImageMap.map (imageMap sq2)))
      (image.ι h.hom))
    (image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2))
have rw₃ : Eq (α := image f.hom ⟶ h.right) (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
  (image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2)
Tactic: rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]
-- 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
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom
have rw : image.ι f.hom ≫ Arrow.Hom.right sq = map' ≫ image.ι g.hom
Tactic: rw [map_ι, map_ι']
-- 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
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
rw : image.ι f.hom ≫ Arrow.Hom.right sq = map' ≫ image.ι g.hom
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom
have rw₁ : Eq (α := image f.hom ⟶ g.right) (image.ι f.hom ≫ Arrow.Hom.right sq) (image.ι f.hom ≫ Arrow.Hom.right sq)
Tactic: rw [map_ι, map_ι']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (hypothesis)
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
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
⊢ map = map'
have this : map ≫ image.ι g.hom = map' ≫ image.ι g.hom
Tactic: have : map ≫ image.ι g.hom = map' ≫ image.ι g.hom := by rw [map_ι, map_ι']
-- 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 : HasImageMap sq
h : Arrow.{v, u} C
inst_4 : HasImage h.hom
sq' : g ⟶ h
inst_5 : HasImageMap sq'
inst_6 : HasImageMap (sq ≫ sq')
⊢ Eq (α := image f.hom ⟶ image h.hom) (ImageMap.map (HasImageMap.imageMap (sq ≫ sq')))
    (ImageMap.map (imageMapComp sq sq'))
have e_self : Eq (α := ImageMap (sq ≫ sq')) (HasImageMap.imageMap (sq ≫ sq')) (imageMapComp sq sq')
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
f : Arrow.{v, u} C
inst_1 : HasImage f.hom
inst_2 : HasImageMap (𝟙 f)
⊢ Eq (α := image f.hom ⟶ image f.hom) (ImageMap.map (HasImageMap.imageMap (𝟙 f))) (ImageMap.map (imageMapId f))
have e_self : Eq (α := ImageMap (𝟙 f)) (HasImageMap.imageMap (𝟙 f)) (imageMapId f)
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
F : StrongEpiMonoFactorisation f
G : MonoFactorisation f
⊢ G.e ≫ G.m = F.e ≫ F.m
have rw : G.e ≫ G.m = f
Tactic: rw [F.toMonoFactorisation.fac, G.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
F : StrongEpiMonoFactorisation f
G : MonoFactorisation f
rw : G.e ≫ G.m = f
⊢ G.e ≫ G.m = F.e ≫ F.m
have rw₁ : f = f
Tactic: rw [F.toMonoFactorisation.fac, G.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
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi F'.e
have rw : StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)
Tactic: rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasImages.{v, u} C
inst_2 : HasPullbacks.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
A B : C
h : A ⟶ B
h_mono : Mono h
x : X ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ (image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ : MonoFactorisation f } ≫
        pullback.fst h y) ≫
      h =
    y
have w : CategoryStruct.comp (Y := image f) (factorThruImage f)
    ((image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := sorry,
            e := pullback.lift x (factorThruImage f) sorry, fac := sorry : MonoFactorisation f } ≫
        pullback.fst h y) ≫
      h) =
  factorThruImage f ≫ y
Tactic: apply image.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrongEpiMonoFactorisations.{v, u} C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst_2 : StrongEpi e
inst_3 : Mono m
⊢ CategoryStruct.comp (Y := image f) (Iso.hom (isoStrongEpiMono e m comm) : I' ⟶ image f) (ι f : image f ⟶ Y) = m
have dsimp : CategoryStruct.comp (Y := image f)
    ({ I := I', m := m, m_mono := inst_3, e := e, fac := sorry, e_strong_epi := inst_2 :
            StrongEpiMonoFactorisation f }.toMonoIsImage.lift
      (Image.monoFactorisation f))
    (ι f) =
  m
Tactic: dsimp [isoStrongEpiMono]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
h : HasStrongEpiMonoFactorisations.{v_1, u_1} C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
⊢ Nonempty (StrongEpiMonoFactorisation f)
have this : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
Tactic: haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Images (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
h : HasStrongEpiMonoFactorisations.{v_1, u_1} C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
⊢ Nonempty (StrongEpiMonoFactorisation f)
have this₁ : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
Tactic: haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _