-- 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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this_1 : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
this_2 : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)
r : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u)
hrU : (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r ≤ U
hxr :
  (↑(Subtype.mk (p := fun (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) ↦ x ∈ U) x hxU) :
      ↥(((Functor.const I).obj c.pt).obj i)) ∈
    (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r
j : Over i
s : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)
hs :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const (Over i)ᵒᵖ)
          ((Scheme.Γ ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).mapCocone
              (opensCone D c i V).op).pt)
        (Opposite.op j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Scheme.Γ ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).mapCocone
                    (opensCone D c i V).op).ι.app
              (Opposite.op j)) :
          (a : (fun (X : Type u) ↦ X) (((opensDiagram D i V).op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj (Opposite.op j))) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Over i)ᵒᵖ).obj
                    ((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).pt).obj
                (Opposite.op j)))
        (((D.map j.hom ⁻¹ᵁ V).topIso.symm.commRingCatIsoToRingEquiv :
            (a : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)) → (↑Γ((↑(D.map j.hom ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
          s) :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Over i)ᵒᵖ)
            ((Scheme.Γ ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).mapCocone
                (opensCone D c i V).op).pt)
          (Opposite.op j)))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (c.π.app i ⁻¹ᵁ V).topIso.inv :
          (a : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u)) →
            (↑Γ((↑(c.π.app i ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
        r :
      (↑Γ((↑(c.π.app i ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
h : c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V = c.π.app i ⁻¹ᵁ V
this :
  r =
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE (c.π.app j.left) (D.map j.hom ⁻¹ᵁ V) (c.π.app i ⁻¹ᵁ V) ⋯) :
        (a : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)) → (↑Γ(c.pt, c.π.app i ⁻¹ᵁ V) : Type u))
      s
rw : x ∈ c.pt.basicOpen r ∧ c.pt.basicOpen r ≤ U
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥c.pt)
      (c.pt.basicOpen (U := c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V))
              (Scheme.Hom.app (c.π.app j.left) (D.map j.hom ⁻¹ᵁ V)) :
            (a : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)) →
              (↑Γ(c.pt, c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V) : Type u))
          s))
      x ∧
    c.pt.basicOpen (U := c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V))
              (Scheme.Hom.app (c.π.app j.left) (D.map j.hom ⁻¹ᵁ V)) :
            (a : (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ V) : Type u)) →
              (↑Γ(c.pt, c.π.app j.left ⁻¹ᵁ D.map j.hom ⁻¹ᵁ V) : Type u))
          s) ≤
      U

Tactic:
rw [← c.pt.basicOpen_res_eq _ (eqToHom h.symm).op, ← CommRingCat.comp_apply,
    Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map, ← this]

Premises used: Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.basicOpen_res_eq, CategoryTheory.Limits.Cone.pt, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CommRingCat.comp_apply, Eq.symm, AlgebraicGeometry.Scheme.Hom.appLE_map