Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case right
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
hc' : IsLimit c' :=
  (IsLimit.postcomposeHomEquiv
      (Functor.isoWhiskerRight
        (NatIso.op
          (NatIso.ofComponents
              (fun x ↦
                match x with
                | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
                | Pairwise.pair i j => eqToIso ⋯)
              ⋯).symm)
        Y.presheaf)
      c')
    (⋯.some.ofIsoLimit
      (Cone.ext
        (Iso.refl
          (Functor.mapCone Y.presheaf
              ((Cocone.precompose
                      (NatIso.ofComponents
                          (fun x ↦
                            match x with
                            | Pairwise.single i => Iso.refl ((D ⋙ G).obj (Pairwise.single i))
                            | Pairwise.pair i j => eqToIso ⋯)
                          ⋯).inv).obj
                  c'₀).op).pt)
        ⋯))
HαF₂ : ∀ (i j : ι), Mono (αF.app (op (Pairwise.pair i j)))
f₁ : c.pt ⟶ c'.pt := hc'.lift ((Cone.postcompose αF).obj c)
i j : ι
⊢ (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c'.pt).map (Quiver.Hom.op (Pairwise.Hom.right i j)) ≫
      match op (Pairwise.pair i j) with
      | op (Pairwise.single i) => c'.π.app (op (Pairwise.single i)) ≫ inv (αF.app (op (Pairwise.single i)))
      | op (Pairwise.pair i j) =>
        c'.π.app (op (Pairwise.single i)) ≫
          inv (αF.app (op (Pairwise.single i))) ≫ F.map (Quiver.Hom.op (Pairwise.Hom.left i j))) =
    (match op (Pairwise.single j) with
      | op (Pairwise.single i) => c'.π.app (op (Pairwise.single i)) ≫ inv (αF.app (op (Pairwise.single i)))
      | op (Pairwise.pair i j) =>
        c'.π.app (op (Pairwise.single i)) ≫
          inv (αF.app (op (Pairwise.single i))) ≫ F.map (Quiver.Hom.op (Pairwise.Hom.left i j))) ≫
      F.map (Quiver.Hom.op (Pairwise.Hom.right i j))

Tactic:
rw [← cancel_mono (αF.app _)]
      simpa using (c'.w (Quiver.Hom.op <| Pairwise.Hom.left i j)).trans
        (c'.w (Quiver.Hom.op <| Pairwise.Hom.right i j)).symm

Goal state after: