awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₃ =
    (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₃

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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) (Limits.diag X)
a : C
g : F.obj a ⟶ X
rw :
  ∀
    (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), F.relativelyRepresentable g
⊢ F.relativelyRepresentable g

Tactic:
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)] at h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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
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) ⋯
          ⋯)
        (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)) ⋯ ⋯))
    (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)
            ⋯ ⋯)
          ⋯)),
    ∃ (b : C) (snd : b ⟶ a') (fst : F.obj b ⟶ F.obj a), IsPullback fst (F.map snd) g g'
⊢ ∃ (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)

Premises used: CategoryTheory.Limits.terminal.from, CategoryTheory.Limits.pullback_map_diagonal_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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)))
rw : F.relativelyRepresentable ((pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom) ≫ pbIso.inv)
⊢ 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))

Tactic:
rw [← comp_id (pullback.lift _ _), ← pbIso.hom_inv_id, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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 (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom)

Tactic:
map_preimage F (_ ≫ pbIso.hom) ▸ map F (F.preimage _)

Premises used: CategoryTheory.Functor.preimage, Eq.rec, CategoryTheory.Functor.relativelyRepresentable.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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 (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯ ≫ pbIso.hom)

Tactic:
exact map_preimage F (_ ≫ pbIso.hom) ▸ map F (F.preimage _)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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
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) ⋯ :
        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))
⊢ F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X) (Limits.diag X)

Tactic:
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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
suffices :
  F.relativelyRepresentable (Y :=
    Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
    (pullback.lift (𝟙 X) (𝟙 X) ⋯)
⊢ 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))

Tactic:
suffices F.relativelyRepresentable (pullback.lift (𝟙 _) (𝟙 _)) from
    (respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _ this
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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)
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) ⋯) g
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g

Tactic:
obtain ⟨_, ⟨_, ⟨_, pbRepr⟩⟩⟩ := h (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Representable
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
inst_8 : HasPullbacks.{v₁, u₁} C
inst_9 : PreservesLimitsOfShape WalkingCospan F
⊢ F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X) (Limits.diag X) ↔
    ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g

Tactic:
⟨fun h _ g => of_diag h g, fun h => diag_of_map_from_obj h⟩

Premises used: CategoryTheory.Functor.relativelyRepresentable.of_diag, Iff.intro, CategoryTheory.Functor.relativelyRepresentable.diag_of_map_from_obj
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
hg : P g
⊢ P f

Tactic:
IsStableUnderRetracts.of_retract h hg

Premises used: CategoryTheory.MorphismProperty.IsStableUnderRetracts.of_retract
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
rw₅ 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.RetractArrow.i_w, CategoryTheory.Retract.i, CategoryTheory.cancel_mono, CategoryTheory.Arrow.Hom.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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 ≫ β
rw₇ 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Arrow.Hom.right, CategoryTheory.RetractArrow.r_w, CategoryTheory.Retract.r, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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

Tactic:
⟨h.i.right ≫ inv g ≫ h.r.left, ?_, ?_⟩

Premises used: CategoryTheory.Arrow.Hom.right, CategoryTheory.Retract.i, CategoryTheory.Retract.r, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.Arrow.Hom.left, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
refine_2 : (Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r) ≫ f = 𝟙 Y
⊢ MorphismProperty.isomorphisms C f

Tactic:
refine ⟨h.i.right ≫ inv g ≫ h.r.left, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
refine_1₂ refine_1₃ : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
⊢ f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X

Tactic:
rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]

Premises used: CategoryTheory.RetractArrow.retract_left, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.RetractArrow.i_w_assoc
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
refine_2₄ refine_2₅ : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) (𝟙 Y)
⊢ (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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.RetractArrow.r_w, CategoryTheory.RetractArrow.retract_right, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.retracts f

Tactic:
⟨_, _, f, { i := 𝟙 _, r := 𝟙 _}, hf⟩

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.retracts, Exists.intro, CategoryTheory.Retract.mk, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.retracts f

Tactic:
exact ⟨_, _, f, { i := 𝟙 _, r := 𝟙 _}, hf⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
a : MorphismProperty.{v, u} C
_ : ∀ ⦃b : MorphismProperty.{v, u} C⦄, a ≤ b → a.retracts ≤ b.retracts
⊢ ∀ ⦃b : MorphismProperty.{v, u} C⦄, a ≤ b → a.retracts ≤ b.retracts

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
⊢ a.retracts ≤ b.retracts

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), a.retracts f → b.retracts f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), a.retracts f → b.retracts f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
⊢ ∀ (f : X ⟶ Y), a.retracts f → b.retracts f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
this : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (hg : RetractArrow f w_2) (hg' : a w_2), b.retracts f
⊢ a.retracts f → b.retracts f

Tactic:
⟨_, _, _, hg, hg'⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
hg : RetractArrow f w_2
hg' : a w_2
⊢ b.retracts f

Tactic:
⟨_, _, _, hg, h _ hg'⟩

Premises used: CategoryTheory.MorphismProperty.retracts, Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
hg : RetractArrow f w_2
hg' : a w_2
⊢ b.retracts f

Tactic:
exact ⟨_, _, _, hg, h _ hg'⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
rw : (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f) ↔ P.retracts ≤ P
⊢ P.IsStableUnderRetracts ↔ P.retracts ≤ P

Tactic:
rw [isStableUnderRetracts_iff]

Premises used: CategoryTheory.MorphismProperty.isStableUnderRetracts_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
mpr : P.retracts ≤ P → ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ (∀ {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
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
X Y : C
f : X ⟶ Y
mp : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (h₂ : RetractArrow f w_2) (h₃ : P w_2), P f
⊢ P.retracts f → P f

Tactic:
⟨_, _, _, h₂, h₃⟩