-- Mathlib/CategoryTheory/Limits/MorphismProperty.lean
/-- Let `P` be stable under composition and base change. If `P` satisfies cancellation on the right,
the subcategory of `Over X` defined by `P` is closed under pullbacks.

Without the cancellation property, this does not in general. Consider for example
`P = Function.Surjective` on `Type`. -/
lemma Over.closedUnderLimitsOfShape_pullback [HasPullbacks T]
    [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] :
    ClosedUnderLimitsOfShape WalkingCospan (fun f : Over X ↦ P f.hom)

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ c.pt.hom = (c.π.app WalkingCospan.left).left ≫ (D.obj WalkingCospan.left).hom

Tactic:
simp

Result:
no goals

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P (D.map WalkingCospan.Hom.inr).left

Tactic:
exact P.of_postcomp _ (D.obj WalkingCospan.one).hom (hf .one) (by simpa using hf .right)

Result:
no goals

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P ((c.π.app WalkingCospan.left).left ≫ (D.obj WalkingCospan.left).hom)

Tactic:
apply P.comp_mem _ _ (P.of_isPullback h.flip ?_) (hf _)

Result:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P (D.map WalkingCospan.Hom.inr).left

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
⊢ ClosedUnderLimitsOfShape WalkingCospan fun f => P f.hom

Tactic:
intro D c hc hf

Result:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
⊢ P c.pt.hom

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P ((D.map WalkingCospan.Hom.inr).left ≫ (D.obj WalkingCospan.one).hom)

Tactic:
simpa using hf .right

Result:
no goals

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
⊢ P c.pt.hom

Tactic:
have h : IsPullback (c.π.app .left).left (c.π.app .right).left (D.map WalkingCospan.Hom.inl).left
      (D.map WalkingCospan.Hom.inr).left := IsPullback.of_isLimit_cone <|
  Limits.isLimitOfPreserves (CategoryTheory.Over.forget X) hc

Result:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P c.pt.hom

Proof state:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P c.pt.hom

Tactic:
rw [show c.pt.hom = (c.π.app .left).left ≫ (D.obj .left).hom by simp]

Result:
T : Type u_1
inst✝⁴ : Category.{u_2, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPullbacks T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
D : WalkingCospan ⥤ Over X
c : Cone D
hc : IsLimit c
hf : ∀ (j : WalkingCospan), (fun f => P f.hom) (D.obj j)
h :
  IsPullback (c.π.app WalkingCospan.left).left (c.π.app WalkingCospan.right).left (D.map WalkingCospan.Hom.inl).left
    (D.map WalkingCospan.Hom.inr).left
⊢ P ((c.π.app WalkingCospan.left).left ≫ (D.obj WalkingCospan.left).hom)