Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, u_2} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, u_2} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
a : J
i : 𝒰.I₀
pf✝¹³ : ⊤.IsMultiplicative
pf✝¹² : ⊤.IsMultiplicative
pf✝¹¹ : HasPullback (D.obj a).hom (𝒰.f i)
pf✝¹⁰ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
pf✝⁹ : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).hom (𝒰.f i)
pf✝⁸ : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).hom (𝒰.f i)
pf✝⁷ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀), P.HasPullbacksAlong (𝒰.f i)
pf✝⁶ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀), P.IsStableUnderBaseChangeAlong (𝒰.f i)
pf✝⁵ : ⊤.IsStableUnderBaseChange
pf✝⁴ : HasColimit d.relativeGluingData.functor
pf✝³ : ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀}, P.HasPullbacksAlong (𝒰.f j)
pf✝² : ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀}, P.IsStableUnderBaseChangeAlong (𝒰.f j)
h1 :
  ∀ {i j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀} (hij : i ⟶ j),
    Cover.trans (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰) hij ≫
        ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
h2 :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀),
    (((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ≫
        Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).f i ≫ Over.hom (D.obj a).toComma
pf✝¹ : P.HasPullbacksAlong (𝒰.f i)
pf✝ : P.IsStableUnderBaseChangeAlong (𝒰.f i)
⊢ pullback.fst (D.obj a).hom (𝒰.f i) ≫
      (OpenCover.glueMorphismsOverOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰)
          (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) h1 h2).left =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
let 𝒱 : (D.obj a).left.OpenCover := 𝒰.pullback₁ (D.obj a).hom

Goal state after:
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, u_2} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, u_2} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
a : J
i : 𝒰.I₀
pf✝¹³ : ⊤.IsMultiplicative
pf✝¹² : ⊤.IsMultiplicative
pf✝¹¹ : HasPullback (D.obj a).hom (𝒰.f i)
pf✝¹⁰ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
pf✝⁹ : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).hom (𝒰.f i)
pf✝⁸ : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).hom (𝒰.f i)
pf✝⁷ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀), P.HasPullbacksAlong (𝒰.f i)
pf✝⁶ : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀), P.IsStableUnderBaseChangeAlong (𝒰.f i)
pf✝⁵ : ⊤.IsStableUnderBaseChange
pf✝⁴ : HasColimit d.relativeGluingData.functor
pf✝³ : ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀}, P.HasPullbacksAlong (𝒰.f j)
pf✝² : ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀}, P.IsStableUnderBaseChangeAlong (𝒰.f j)
h1 :
  ∀ {i j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀} (hij : i ⟶ j),
    Cover.trans (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰) hij ≫
        ((d.cocone j).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor j =
      ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i
h2 :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).I₀),
    (((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) ≫
        Over.hom (((Functor.const J).obj d.glued).obj a).toComma =
      (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰).f i ≫ Over.hom (D.obj a).toComma
pf✝¹ : P.HasPullbacksAlong (𝒰.f i)
pf✝ : P.IsStableUnderBaseChangeAlong (𝒰.f i)
𝒱 : (D.obj a).left.OpenCover := Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
⊢ pullback.fst (D.obj a).hom (𝒰.f i) ≫
      (OpenCover.glueMorphismsOverOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰)
          (fun i ↦ ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i) h1 h2).left =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i