awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' S : C
mpr : ∀ {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'
⊢ ∀ {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' S : C
f : X ⟶ S
mpr : ∀ {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'
⊢ ∀ {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
mpr : ∀ {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'
⊢ ∀ {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
mpr : ∀ {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'
⊢ ∀ {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g), P g'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
h₁ : IsPullback f' g' g f
h₂ : P g
⊢ P g'

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

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pullbacks ≤ P
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
h₁ : IsPullback f' g' g f
h₂ : P g
⊢ P g'

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 rwa rwa₁ rwa₂ rwa₃ : P.IsStableUnderBaseChange
⊢ P.pullbacks ≤ P

Tactic:
rwa [← isStableUnderBaseChange_iff_pullbacks_le]

Premises used: CategoryTheory.MorphismProperty.isStableUnderBaseChange_iff_pullbacks_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : HasPullback f g], P g → P (X := pullback f g) (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
haveI : ∀ (this : HasPullback f g), P g'
⊢ P g'

Tactic:
haveI : HasPullback f g := sq.flip.hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : HasPullback f g], P g → P (X := pullback f g) (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
rw : P (X := pullback f g) (pullback.fst f g)
⊢ P g'

Tactic:
rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]

Premises used: CategoryTheory.IsPullback.isoPullback_inv_fst, CategoryTheory.IsPullback.flip, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : HasPullback f g], P g → P (X := pullback f g) (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
hP₂ _ _ _ f g hg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : HasPullback f g], P g → P (X := pullback f g) (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
exact hP₂ _ _ _ f g hg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
⊢ P.IsStableUnderBaseChange

Tactic:
.mk' fun X Y S f g _ hg ↦ ?_

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
refine :
  ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) (x : HasPullback f g) (hg : P g), P (X := pullback f g) (pullback.fst f g)
⊢ P.IsStableUnderBaseChange

Tactic:
refine .mk' fun X Y S f g _ hg ↦ ?_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
hg : P g
obtain :
  ∀ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y) (h_1 : IsPullback fst snd f g) (hfst : P fst),
    P (X := pullback f g) (pullback.fst f g)
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
obtain ⟨T, fst, snd, h, hfst⟩ := H f g hg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    P g → ∃ (T : C) (fst : T ⟶ X) (snd : T ⟶ Y), IsPullback fst snd f g ∧ P fst
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : P g
T : C
fst : T ⟶ X
snd : T ⟶ Y
h : IsPullback fst snd f g
hfst : P fst
rwa : P (X := pullback f g) (Iso.inv h.isoPullback ≫ fst)
rwa₁ rwa₂ rwa₃ rwa₄ : P fst
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
rwa [← h.isoPullback_inv_fst, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.IsPullback.isoPullback_inv_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
hP : ∀ (f g : Arrow.{v, u} C) (x : f ≅ g), P f.hom → P g.hom
⊢ P.RespectsIso

Tactic:
apply RespectsIso.of_respects_arrow_iso

Premises used: CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
f g : Arrow.{v, u} C
e : f ≅ g
⊢ P f.hom → P g.hom

Tactic:
of_isPullback (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w))

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.Arrow.Hom.w, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback, CategoryTheory.Iso.inv, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
f g : Arrow.{v, u} C
e : f ≅ g
⊢ P f.hom → P g.hom

Tactic:
exact of_isPullback (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w))

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.Arrow.Hom.w, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback, CategoryTheory.Iso.inv, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
inst_2 : P.IsStableUnderBaseChangeAlong f
H : P g
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
IsStableUnderBaseChangeAlong.of_isPullback (IsPullback.of_hasPullback f g).flip H

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong.of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
inst_2 : P.IsStableUnderBaseChangeAlong g
H : P f
⊢ P (X := pullback f g) (pullback.snd f g)

Tactic:
IsStableUnderBaseChangeAlong.of_isPullback (IsPullback.of_hasPullback f g) H

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
S S' : C
f : S' ⟶ S
inst_1 : HasPullbacksAlong f
inst_2 : P.IsStableUnderBaseChangeAlong f
X : Over.{v, u} S
H : P X.hom
⊢ P ((Over.pullback f).obj X).hom

Tactic:
pullback_snd X.hom f H

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.MorphismProperty.pullback_snd, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₁₂ : X ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
hv₁₂ : v₁₂ = g ≫ v₂₂
inst_2 : HasPullback v₁₂ f
inst_3 : HasPullback v₂₂ f
H : P g
⊢ Eq (α := pullback v₁₂ f ⟶ S) ((pullback.fst v₁₂ f ≫ g) ≫ v₂₂) (pullback.snd v₁₂ f ≫ f)

Tactic:
simp [pullback.condition, ← hv₁₂]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₁₂ : X ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
hv₁₂ : v₁₂ = g ≫ v₂₂
inst_2 : HasPullback v₁₂ f
inst_3 : HasPullback v₂₂ f
H : P g
subst :
  ∀ [inst_4 : HasPullback (g ≫ v₂₂) f],
    P (X := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f)
      (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯)
⊢ P (X := pullback v₁₂ f) (Y := pullback v₂₂ f) (pullback.lift (pullback.fst v₁₂ f ≫ g) (pullback.snd v₁₂ f) ⋯)

Tactic:
subst hv₁₂
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
⊢ P (X := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯)

Tactic:
of_isPullback (f' := pullback.fst (g ≫ v₂₂) f)
    (f := pullback.fst v₂₂ f) ?_ H

Premises used: CategoryTheory.MorphismProperty.of_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
refine :
  IsPullback (P := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f) (pullback.fst (g ≫ v₂₂) f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯) g (pullback.fst v₂₂ f)
⊢ P (X := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯)

Tactic:
refine of_isPullback (f' := pullback.fst (g ≫ v₂₂) f)
    (f := pullback.fst v₂₂ f) ?_ H

Premises used: CategoryTheory.MorphismProperty.of_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
⊢ Eq (α := pullback (g ≫ v₂₂) f ⟶ Y) (pullback.fst (g ≫ v₂₂) f ≫ g)
    (CategoryStruct.comp (Y := pullback v₂₂ f)
      (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯) (pullback.fst v₂₂ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
refine :
  IsPullback (P := pullback (g ≫ v₂₂) f) (pullback.fst (g ≫ v₂₂) f)
    (CategoryStruct.comp (Y := pullback v₂₂ f)
      (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯) (pullback.snd v₂₂ f))
    (g ≫ v₂₂) f
⊢ IsPullback (P := pullback (g ≫ v₂₂) f) (Y := pullback v₂₂ f) (pullback.fst (g ≫ v₂₂) f)
    (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯) g (pullback.fst v₂₂ f)

Tactic:
refine IsPullback.of_bot ?_ (by simp) (IsPullback.of_hasPullback v₂₂ f)

Premises used: CategoryTheory.IsPullback.of_bot, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst_2 : HasPullback v₂₂ f
H : P g
inst_3 : HasPullback (g ≫ v₂₂) f
⊢ IsPullback (P := pullback (g ≫ v₂₂) f) (pullback.fst (g ≫ v₂₂) f)
    (CategoryStruct.comp (Y := pullback v₂₂ f)
      (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯) (pullback.snd v₂₂ f))
    (g ≫ v₂₂) f

Tactic:
simpa using IsPullback.of_hasPullback (g ≫ v₂₂) f

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
S S' : C
f : S' ⟶ S
inst_2 : HasPullbacksAlong f
X Y : Over.{v, u} S
g : X ⟶ Y
H : P (Over.Hom.left g)
⊢ P (Over.Hom.left ((Over.pullback f).map g))

Tactic:
pullbackLift_fst_snd f (g.w.symm) H

Premises used: CategoryTheory.Limits.limit, CategoryTheory.MorphismProperty.pullbackLift_fst_snd, CategoryTheory.Over.Hom.w, CategoryTheory.Limits.limit.lift, Eq.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
have :
  ∀ (this : HasPullbacksAlong (Over.mk f).hom),
    P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
⊢ P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
have : HasPullbacksAlong (Over.mk f).hom := by cat_disch
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
h₀ :
  Eq (α := pullback f g ⟶ X')
    (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯) (pullback.fst f' g'))
    (CategoryStruct.comp (Y := pullback f' g')
      ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
            Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
          Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
            Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
        pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
      (pullback.fst f' g'))
h₃ :
  Eq (α := pullback f g ⟶ Y')
    (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯) (pullback.snd f' g'))
    (CategoryStruct.comp (Y := pullback f' g')
      ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
            Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
          Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
            Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
        pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
      (pullback.snd f' g'))
⊢ Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ Eq (α := pullback f g ⟶ X')
    (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯) (pullback.fst f' g'))
    (CategoryStruct.comp (Y := pullback f' g')
      ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
            Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
          Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
            Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
        pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
      (pullback.fst f' g'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ Eq (α := pullback f g ⟶ Y')
    (CategoryStruct.comp (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯) (pullback.snd f' g'))
    (CategoryStruct.comp (Y := pullback f' g')
      ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
            Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
          Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
            Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
        pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
      (pullback.snd f' g'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this : HasPullbacksAlong (Over.mk f).hom
⊢ Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))

Tactic:
have : pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁)
        ((Category.comp_id _).trans e₂) =
      ((pullbackSymmetry _ _).hom ≫
          ((Over.pullback _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
        (pullbackSymmetry _ _).hom ≫
          ((Over.pullback g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left := by
    ext <;> simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
rw :
  P (X := pullback f g) (Y := pullback f' g')
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)
⊢ P (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
hf :
  P (X := pullback f g) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
    (Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
      Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))
hg :
  P (X := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left) (Y := pullback f' g')
    (Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)
⊢ P (X := pullback f g) (Y := pullback f' g')
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
          Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
        Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
          Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      pullback (Over.mk f).hom (Over.mk g).hom ⟶ ((Over.pullback g').obj (Over.mk f')).left)

Tactic:
apply P.comp_mem

Premises used: CategoryTheory.MorphismProperty.comp_mem