-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : Membership.mem (α := ↥(D.obj i)) (↑U : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
t : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)
hj :
  Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensCone D c i U).π.app j)) :
          (a : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
        t :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj j, ⊤) : Type u))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) s (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯ :
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))))
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1 :
  (↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u) =
    (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u)
⊢ Eq (α := (↑Γ(c.pt, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
            c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
            (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
        s :
      (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (c.pt.presheaf.map (homOfLE H).op) :
          (a : (↑Γ(c.pt, (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) →
            (↑Γ(c.pt, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
                c.pt.presheaf.obj (Opposite.op (⋯.functor.obj ⊤))) (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
                (↑(c.pt.presheaf.obj (Opposite.op (⋯.functor.obj ⊤))) : Type u))
            s :
          (↑(c.pt.presheaf.obj (Opposite.op (⋯.functor.obj ⊤))) : Type u)) :
      (↑Γ(c.pt, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
have h : Eq (α := (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤)) (Y :=
          c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
          (c.pt.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
          (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
      s :
    (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := c.pt.presheaf.obj (Opposite.op ⊤))
          (c.pt.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫ c.pt.presheaf.map (homOfLE H).op) :
        (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
          (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
      s :
    (↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤))) : Type u))
Tactic: change _ = (c.pt.presheaf.map (homOfLE _).op ≫ c.pt.presheaf.map (homOfLE _).op) s