-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
inst_5 : IsQuasiAffine.{u} c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : Membership.mem (γ := Set (TopologicalSpace.Opens ↥(D.obj i))) (D.obj i).affineOpens U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
j : I
r : (↑Γ(D.obj j, ⊤) : Type u)
hr :
  IsAffineOpen.{u} (X := c.pt)
    (c.pt.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
        r))
hxr :
  x ∈
    (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt)
hrU :
  (↑(c.pt.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (c.π.app j)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj j, ⊤) : Type u))
            r)) :
      Set ↥c.pt) ⊆
    (↑(c.π.app i ⁻¹ᵁ U) : Set ↥(((Functor.const I).obj c.pt).obj i))
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
h :
  (D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r) =
    D.map (flk ≫ fki) ⁻¹ᵁ U ⊓
      (D.obj l).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
          r)
h₁ :
  D.map (flk ≫ fki) ⁻¹ᵁ U ⊓
      (D.obj l).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
          r) =
    (D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r)
h₂ :
  (D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r) ≤
    D.map (flk ≫ fki) ⁻¹ᵁ U
h₃ :
  (D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map flk ≫ D.map fkj)) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r) ≤
    D.map (flk ≫ fki) ⁻¹ᵁ U
h₄ :
  (D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map flk)) :
          (a : (↑Γ(D.obj k, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
            r :
          (↑Γ(D.obj k, ⊤) : Type u))) ≤
    D.map (flk ≫ fki) ⁻¹ᵁ U
h₅ :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map (flk ≫ fki) ⁻¹ᵁ U
h₆ :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    (D.map flk ≫ D.map fki) ⁻¹ᵁ U
h₇ h₈ h₉ h₁₀ :
  D.map flk ⁻¹ᵁ
      (D.obj k).basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop (D.map fkj)) :
            (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
          r) ≤
    D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ Eq.{u + 1} (α := (D.obj l).Opens)
    ((D.obj l).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
          (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
        r))
    ((D.obj l).basicOpen (U := D.map (flk ≫ fki) ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := (D.obj l).presheaf.obj (Opposite.op ⊤)) (Y :=
            (D.obj l).presheaf.obj (Opposite.op (D.map (flk ≫ fki) ⁻¹ᵁ U)))
            ((D.obj l).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑((D.obj l).presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑((D.obj l).presheaf.obj (Opposite.op (D.map (flk ≫ fki) ⁻¹ᵁ U))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop (D.map (flk ≫ fkj))) :
              (a : (↑Γ(D.obj j, ⊤) : Type u)) → (↑Γ(D.obj l, ⊤) : Type u))
            r :
          (↑Γ(D.obj l, ⊤) : Type u))))

Tactic:
rwa [Scheme.basicOpen_res, eq_comm, inf_eq_right, Functor.map_comp,
        elementwise_of% Scheme.Hom.comp_appTop, ← Scheme.preimage_basicOpen_top, Functor.map_comp,
        Scheme.Hom.comp_preimage]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen_top, eq_comm, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.basicOpen_res, CategoryTheory.Functor.map_comp, AlgebraicGeometry.Scheme.Hom.comp_appTop, inf_eq_right