Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
c : Cone F :=
  (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)).mapCone
    (Under.liftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX))
this : PreservesFiniteLimits (Under.pushout (Scheme.Hom.appLE f US UT hUST))
val✝ : Fintype ι
hc : IsLimit c :=
  isLimitOfPreserves (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT))
    (Under.isLimitLiftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX) ⋯.some)
c'₀ : Cocone (D ⋙ G) := (colimit.cocone (D ⋙ G)).extend (eqToIso ⋯).hom
c' : Cone (D.op ⋙ G.op ⋙ Y.presheaf) := Functor.mapCone Y.presheaf c'₀.op
e : D ⋙ G ≅ Pairwise.diagram fun i ↦ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT :=
  NatIso.ofComponents
    (fun x ↦
      match x with
      | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
      | Pairwise.pair i j => eqToIso ⋯)
    ⋯
⊢ IsLimit c'

Tactic:
haveI HX := ((TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections _).mp
      Y.IsSheaf (fun i ↦ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT)).preserves
        (c := ((Cocone.precompose e.inv).obj c'₀).op)

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf :=
  { app := fun i ↦ (pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection H hUST ⋯ ⋯, naturality := ⋯ }
c : Cone F :=
  (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)).mapCone
    (Under.liftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX))
this : PreservesFiniteLimits (Under.pushout (Scheme.Hom.appLE f US UT hUST))
val✝ : Fintype ι
hc : IsLimit c :=
  isLimitOfPreserves (Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT))
    (Under.isLimitLiftCone (Functor.mapCone X.presheaf c₀.op) (Scheme.Hom.appLE iX US UX hUSX) ⋯.some)
c'₀ : Cocone (D ⋙ G) := (colimit.cocone (D ⋙ G)).extend (eqToIso ⋯).hom
c' : Cone (D.op ⋙ G.op ⋙ Y.presheaf) := Functor.mapCone Y.presheaf c'₀.op
e : D ⋙ G ≅ Pairwise.diagram fun i ↦ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT :=
  NatIso.ofComponents
    (fun x ↦
      match x with
      | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
      | Pairwise.pair i j => eqToIso ⋯)
    ⋯
HX :
  ∀ (hc : IsLimit ((Cocone.precompose e.inv).obj c'₀).op),
    Nonempty (IsLimit (Functor.mapCone Y.presheaf ((Cocone.precompose e.inv).obj c'₀).op))
⊢ IsLimit c'