-- Module: Mathlib.AlgebraicGeometry.Cover.Over
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
Q : MorphismProperty Scheme
inst_6 : Q.HasOfPostcompProperty Q
inst_7 : Q.IsStableUnderBaseChange
inst_8 : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
            (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X x).asOverProp (P := Q) S ⋯) (Z :=
              X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))).left,
      f := fun (x : 𝒰.I₀) ↦
        CommaMorphism.left
          (MorphismProperty.Comma.Hom.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤)
            (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f x) S))) }
refine_2 :
  P (X :=
    pullback (X :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (W.asOverProp (P := Q) S hW))
      (Y :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        ((𝒰.X j).asOverProp (P := Q) S ⋯))
      (Z :=
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (X.asOverProp (P := Q) S hX))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) f S))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) (𝒰.f j) S)))
    (pullback.fst
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) f S))
      (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (Hom.asOverProp (P := Q) (𝒰.f j) S)))
⊢ P (X :=
    (MorphismProperty.Comma.toComma (P := Q) (Q := ⊤) (W := ⊤)
        (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S ⋯) (Z :=
          X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S))).left)
    (Y := W)
    (CategoryTheory.Functor.map (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
        (pullback.fst (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S)) :
      Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
          (pullback (X := W.asOverProp (P := Q) S hW) (Y := (𝒰.X j).asOverProp (P := Q) S ⋯) (Z :=
            X.asOverProp (P := Q) S hX) (Hom.asOverProp (P := Q) f S) (Hom.asOverProp (P := Q) (𝒰.f j) S)) ⟶
        Functor.obj (MorphismProperty.Comma.forget (𝟭 Scheme) (Functor.fromPUnit S) Q ⊤ ⊤ ⋙ Over.forget S)
          (W.asOverProp (P := Q) S hW))

Tactic:
rw [← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Limits.PreservesPullback.iso_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso