Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofiltered I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U x).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ U (σi x)).carrier
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
hiS : ∀ {x : ↥c.pt}, x ∈ σ → i x ∈ S
hjS : ∀ {x y : ↥c.pt}, x ∈ σ → y ∈ σ → j x y ∈ S
k : I
fk : {X : I} → X ∈ S → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ S) (mY : Y ∈ S) {f : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈
        Finset.image₂ (fun x y ↦ ⟨j ↑x ↑y, ⟨i ↑x, ⟨⋯, ⟨⋯, fjx ↑x ↑y⟩⟩⟩⟩) σ.attach σ.attach ∪
          Finset.image₂ (fun x y ↦ ⟨j ↑x ↑y, ⟨i ↑y, ⟨⋯, ⟨⋯, fjy ↑x ↑y⟩⟩⟩⟩) σ.attach σ.attach →
      fk mX ≫ f = fk mY
hk₁ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjx x y = fk ⋯
hk₂ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjy x y = fk ⋯
k' : I
fk'k : k' ⟶ k
hk' : D.map fk'k ⁻¹ᵁ ⨆ x, ⨆ (hx : x ∈ σ), D.map (fk ⋯) ⁻¹ᵁ U x = ⊤
this :
  ∀ (x : (i_1 : ↥σ) → ((D.obj k').presheaf ⋙ forget CommRingCat).obj (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U ↑i_1))),
    Presieve.Arrows.Compatible ((D.obj k').presheaf ⋙ forget CommRingCat) (fun x ↦ homOfLE ⋯) x →
      ∃! t,
        ∀ (i_1 : ↥σ), (ConcreteCategory.hom (((D.obj k').presheaf ⋙ forget CommRingCat).map (homOfLE ⋯).op)) t = x i_1
x y : ↥σ
V : TopologicalSpace.Opens ↥(D.obj k')
fVx : V ⟶ (fun x ↦ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U ↑x) x
fVy : V ⟶ (fun x ↦ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U ↑x) y
x✝ : fVx ≫ (fun x ↦ homOfLE ⋯) x = fVy ≫ (fun x ↦ homOfLE ⋯) y
⊢ (ConcreteCategory.hom (((D.obj k').presheaf ⋙ forget CommRingCat).map fVx.op))
      ((fun x ↦ (ConcreteCategory.hom (Scheme.Hom.app (D.map (fk'k ≫ fk ⋯)) (U ↑x))) (t ↑x)) x) =
    (ConcreteCategory.hom (((D.obj k').presheaf ⋙ forget CommRingCat).map fVy.op))
      ((fun x ↦ (ConcreteCategory.hom (Scheme.Hom.app (D.map (fk'k ≫ fk ⋯)) (U ↑x))) (t ↑x)) y)

Tactic:
by
    have H : V ≤ D.map (fk'k ≫ fk (hjS x.2 y.2)) ⁻¹ᵁ
        (D.map (fjx ↑x ↑y) ⁻¹ᵁ U ↑x ⊓ D.map (fjy ↑x ↑y) ⁻¹ᵁ U ↑y) := by
      change V ≤ (D.map (fk'k ≫ fk (hjS x.2 y.2)) ≫ D.map (fjx ↑x ↑y)) ⁻¹ᵁ U x ⊓
        (D.map (fk'k ≫ fk (hjS x.2 y.2)) ≫ D.map (fjy x y)) ⁻¹ᵁ U y
      rw [← Functor.map_comp, ← Functor.map_comp, Category.assoc, Category.assoc,
        hk₁ x.2 y.2, hk₂ x.2 y.2, le_inf_iff]
      exact ⟨fVx.le, fVy.le⟩
    convert!
      congr(((D.map (fk'k ≫ fk (hjS x.2 y.2))).app _ ≫ (D.obj k').presheaf.map (homOfLE H).op)
        $(hj x y)) using 1
    · dsimp [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]
      simp only [← ConcreteCategory.comp_apply]
      congr 2
      simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE,
        -Scheme.Hom.comp_appLE, ← Functor.map_comp, hk₁]
    · dsimp [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]
      simp only [← ConcreteCategory.comp_apply]
      congr 2
      simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE,
        -Scheme.Hom.comp_appLE, ← Functor.map_comp, hk₂]

Goal state after: