awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h :
  F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X)
    (CategoryStruct.comp (Y := Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
      (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
        X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
      (Iso.inv (prodIsoPullback X X) :
        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
          Limits.prod.{v₂, u₂} X X))
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
⊢ ∃ (b : C) (snd : b ⟶ a') (fst : F.obj b ⟶ F.obj a), IsPullback fst (F.map snd) g g'
have obtain : ∀
  (toCommSq :
    CommSq (W := Limits.pullback g g') (Y :=
      Limits.pullback (Z := terminal.{v₂, u₂} D) (g ≫ terminal.from X) (g' ≫ terminal.from X)) (Z :=
      pullback.diagonalObj.{v₂, u₂} (Y := terminal.{v₂, u₂} D) (terminal.from X)) (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) sorry
        sorry)
      (pullback.diagonal (terminal.from X))
      (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g'
        (𝟙 (terminal.{v₂, u₂} D)) sorry sorry))
  (left :
    IsLimit
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) sorry
          sorry)
        sorry)),
  ∃ (b : C) (snd : b ⟶ a') (fst : F.obj b ⟶ F.obj a), IsPullback fst (F.map snd) g g'
Tactic: obtain ⟨_, ⟨left⟩⟩ := pullback_map_diagonal_isPullback g g' (terminal.from X)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst_8 : HasPullbacks.{v₁, u₁} C
inst_9 : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X)
pbIso : Limits.pullback (Z := terminal.{v₂, u₂} D)
    ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
    ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
  F.obj (limit.{0, 0, v₁, u₁} (pair a a)) :=
  Iso.trans (Y :=
    Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from (F.obj a)) (terminal.from (F.obj a)))
    (pullback.congrHom ⋯ ⋯ :
      Limits.pullback (Z := terminal.{v₂, u₂} D)
          ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X) ≅
        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from (F.obj a)) (terminal.from (F.obj a)))
    (Iso.trans (Y := Limits.prod.{v₂, u₂} (F.obj a) (F.obj a)) (Iso.symm (prodIsoPullback (F.obj a) (F.obj a)))
        (Iso.trans (Y := limit (pair a a ⋙ F))
          (Iso.symm (HasLimit.isoOfNatIso (pairComp a a F)) :
            limit.{0, 0, v₂, u₂} (pair (F.obj a) (F.obj a)) ≅ limit (pair a a ⋙ F))
          (Iso.symm (preservesLimitIso F (pair a a)) :
            limit (pair a a ⋙ F) ≅ F.obj (limit.{0, 0, v₁, u₁} (pair a a)))) :
      Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from (F.obj a)) (terminal.from (F.obj a)) ≅
        F.obj (limit.{0, 0, v₁, u₁} (pair a a)))
⊢ F.relativelyRepresentable (Y :=
    Limits.pullback (Z := terminal.{v₂, u₂} D)
      ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
      ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
    (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ :
      F.obj a ⟶
        Limits.pullback (Z := terminal.{v₂, u₂} D)
          ((g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X)
          ((g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X))
have rw : F.relativelyRepresentable ((pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) sorry ≫ pbIso.hom) ≫ pbIso.inv)
Tactic: rw [← comp_id (pullback.lift _ _), ← pbIso.hom_inv_id, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_8 : HasPullbacks.{v₁, u₁} C
inst_9 : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X) (Limits.diag X)
have rw : F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X)
  (CategoryStruct.comp (Y := Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
    (pullback.lift (𝟙 X) (𝟙 X) sorry :
      X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
    (Iso.inv (prodIsoPullback X X) :
      Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
        Limits.prod.{v₂, u₂} X X))
Tactic: rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_8 : HasPullbacks.{v₁, u₁} C
inst_9 : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X)
    (CategoryStruct.comp (Y := Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
      (pullback.lift (𝟙 X) (𝟙 X) ⋯ :
        X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
      (Iso.inv (prodIsoPullback X X) :
        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
          Limits.prod.{v₂, u₂} X X))
have suffices : F.relativelyRepresentable (Y := Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
  (pullback.lift (𝟙 X) (𝟙 X) sorry)
Tactic: suffices F.relativelyRepresentable (pullback.lift (𝟙 _) (𝟙 _)) from
    (respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _ this
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_8 : HasPullbacks.{v₁, u₁} C
inst_9 : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
g : F.obj a ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X)
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g
have obtain : ∀ (w : C) (w_1 : w ⟶ a) (w_2 : F.obj w ⟶ F.obj a)
  (pbRepr :
    IsPullback w_2 (F.map w_1) (g ≫ pullback.fst (terminal.from X) (terminal.from X))
      (g ≫ pullback.snd (terminal.from X) (terminal.from X))),
  ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) sorry) g
Tactic: obtain ⟨_, ⟨_, ⟨_, pbRepr⟩⟩⟩ := h (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Mono g
Z : C
α β : Z ⟶ x
w : α ≫ f = β ≫ f
⊢ α = β
have rw : α ≫ Arrow.Hom.left h.i = β ≫ Arrow.Hom.left h.i
Tactic: rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Mono g
Z : C
α β : Z ⟶ x
w : α ≫ f = β ≫ f
rw : α ≫ Arrow.Hom.left h.i = β ≫ Arrow.Hom.left h.i
⊢ α = β
have rw₁ : (α ≫ Arrow.Hom.left h.i) ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
Tactic: rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Mono g
Z : C
α β : Z ⟶ x
w : α ≫ f = β ≫ f
rw : α ≫ Arrow.Hom.left h.i = β ≫ Arrow.Hom.left h.i
rw₁ : (α ≫ Arrow.Hom.left h.i) ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
⊢ α = β
have rw₂ : α ≫ Arrow.Hom.left h.i ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
Tactic: rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Mono g
Z : C
α β : Z ⟶ x
w : α ≫ f = β ≫ f
rw : α ≫ Arrow.Hom.left h.i = β ≫ Arrow.Hom.left h.i
rw₁ : (α ≫ Arrow.Hom.left h.i) ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
rw₂ : α ≫ Arrow.Hom.left h.i ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
⊢ α = β
have rw₃ : α ≫ Arrow.Hom.left h.i ≫ g = β ≫ Arrow.Hom.left h.i ≫ g
Tactic: rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Mono g
Z : C
α β : Z ⟶ x
w : α ≫ f = β ≫ f
rw : α ≫ Arrow.Hom.left h.i = β ≫ Arrow.Hom.left h.i
rw₁ : (α ≫ Arrow.Hom.left h.i) ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
rw₂ : α ≫ Arrow.Hom.left h.i ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
rw₃ : α ≫ Arrow.Hom.left h.i ≫ g = β ≫ Arrow.Hom.left h.i ≫ g
⊢ α = β
have rw₄ : α ≫ f ≫ Arrow.Hom.right h.i = β ≫ f ≫ Arrow.Hom.right h.i
Tactic: rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Mono g
Z : C
α β : Z ⟶ x
w : α ≫ f = β ≫ f
rw : α ≫ Arrow.Hom.left h.i = β ≫ Arrow.Hom.left h.i
rw₁ : (α ≫ Arrow.Hom.left h.i) ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
rw₂ : α ≫ Arrow.Hom.left h.i ≫ g = (β ≫ Arrow.Hom.left h.i) ≫ g
rw₃ : α ≫ Arrow.Hom.left h.i ≫ g = β ≫ Arrow.Hom.left h.i ≫ g
rw₄ : α ≫ f ≫ Arrow.Hom.right h.i = β ≫ f ≫ Arrow.Hom.right h.i
⊢ α = β
have rw₅ : β ≫ f ≫ Arrow.Hom.right h.i = β ≫ f ≫ Arrow.Hom.right h.i
Tactic: rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
⊢ α = β
have rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
⊢ α = β
have rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
⊢ α = β
have rw₂ : (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₂ : (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
⊢ α = β
have rw₃ : (g ≫ Arrow.Hom.right h.r) ≫ α = (g ≫ Arrow.Hom.right h.r) ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₂ : (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₃ : (g ≫ Arrow.Hom.right h.r) ≫ α = (g ≫ Arrow.Hom.right h.r) ≫ β
⊢ α = β
have rw₄ : (Arrow.Hom.left h.r ≫ f) ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₂ : (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₃ : (g ≫ Arrow.Hom.right h.r) ≫ α = (g ≫ Arrow.Hom.right h.r) ≫ β
rw₄ : (Arrow.Hom.left h.r ≫ f) ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
⊢ α = β
have rw₅ : Arrow.Hom.left h.r ≫ f ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₂ : (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₃ : (g ≫ Arrow.Hom.right h.r) ≫ α = (g ≫ Arrow.Hom.right h.r) ≫ β
rw₄ : (Arrow.Hom.left h.r ≫ f) ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
rw₅ : Arrow.Hom.left h.r ≫ f ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
⊢ α = β
have rw₆ : Arrow.Hom.left h.r ≫ f ≫ α = Arrow.Hom.left h.r ≫ f ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x x_1 x_2 x_3 : C
f : x ⟶ x_1
g : x_2 ⟶ x_3
h : RetractArrow f g
hg : Epi g
Z : C
α β : x_1 ⟶ Z
w : f ≫ α = f ≫ β
rw : Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β
rw₁ : g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₂ : (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
rw₃ : (g ≫ Arrow.Hom.right h.r) ≫ α = (g ≫ Arrow.Hom.right h.r) ≫ β
rw₄ : (Arrow.Hom.left h.r ≫ f) ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
rw₅ : Arrow.Hom.left h.r ≫ f ≫ α = (Arrow.Hom.left h.r ≫ f) ≫ β
rw₆ : Arrow.Hom.left h.r ≫ f ≫ α = Arrow.Hom.left h.r ≫ f ≫ β
⊢ α = β
have rw₇ : Arrow.Hom.left h.r ≫ f ≫ β = Arrow.Hom.left h.r ≫ f ≫ β
Tactic: rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
⊢ MorphismProperty.isomorphisms C f
have refine_1 : f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
Tactic: refine ⟨h.i.right ≫ inv g ≫ h.r.left, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_1 : f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
⊢ MorphismProperty.isomorphisms C f
have refine_2 : (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
Tactic: refine ⟨h.i.right ≫ inv g ≫ h.r.left, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
⊢ f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
have refine_1 : Arrow.Hom.left h.i ≫ g ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
Tactic: rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_1 : Arrow.Hom.left h.i ≫ g ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
⊢ f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
have refine_1₁ : Arrow.Hom.left h.i ≫ Arrow.Hom.left h.r = 𝟙 X
Tactic: rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_1 : Arrow.Hom.left h.i ≫ g ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
refine_1₁ : Arrow.Hom.left h.i ≫ Arrow.Hom.left h.r = 𝟙 X
⊢ f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
have refine_1₂ : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
Tactic: rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
⊢ (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
have refine_2 : Arrow.Hom.right h.i ≫ (inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
Tactic: rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_2 : Arrow.Hom.right h.i ≫ (inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
⊢ (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
have refine_2₁ : Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r ≫ f = 𝟙 Y
Tactic: rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_2 : Arrow.Hom.right h.i ≫ (inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
refine_2₁ : Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r ≫ f = 𝟙 Y
⊢ (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
have refine_2₂ : Arrow.Hom.right h.i ≫ inv g ≫ g ≫ Arrow.Hom.right h.r = 𝟙 Y
Tactic: rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_2 : Arrow.Hom.right h.i ≫ (inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
refine_2₁ : Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r ≫ f = 𝟙 Y
refine_2₂ : Arrow.Hom.right h.i ≫ inv g ≫ g ≫ Arrow.Hom.right h.r = 𝟙 Y
⊢ (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
have refine_2₃ : Arrow.Hom.right h.i ≫ Arrow.Hom.right h.r = 𝟙 Y
Tactic: rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h_1 : IsIso g
refine_2 : Arrow.Hom.right h.i ≫ (inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
refine_2₁ : Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r ≫ f = 𝟙 Y
refine_2₂ : Arrow.Hom.right h.i ≫ inv g ≫ g ≫ Arrow.Hom.right h.r = 𝟙 Y
refine_2₃ : Arrow.Hom.right h.i ≫ Arrow.Hom.right h.r = 𝟙 Y
⊢ (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
have refine_2₄ : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) (𝟙 Y)
Tactic: rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
⊢ a.retracts ≤ b.retracts
have _ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), a.retracts f → b.retracts f
Tactic: _
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
⊢ a.retracts f → b.retracts f
have this : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (hg : RetractArrow f w_2) (hg' : a w_2), b.retracts f
Tactic: ⟨_, _, _, hg, hg'⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.IsStableUnderRetracts ↔ P.retracts ≤ P
have rw : (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f) ↔ P.retracts ≤ P
Tactic: rw [isStableUnderRetracts_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f) ↔ P.retracts ≤ P
have mp : (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f) → P.retracts ≤ P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
mp : (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f) → P.retracts ≤ P
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f) ↔ P.retracts ≤ P
have mpr : P.retracts ≤ P → ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
Tactic: constructor