-- 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 : I), IsAffine.{u} (D.obj i)
i : I
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
this : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const Iᵒᵖ)
          ((Scheme.Γ ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).mapCocone
              c.op).pt)
        (Opposite.op i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Scheme.Γ ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).mapCocone
                    c.op).ι.app
              (Opposite.op i)) :
          (a : (fun (X : Type u) ↦ X) ((D.op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj (Opposite.op i))) →
            (fun (X : Type u) ↦ X)
              (((Functor.const Iᵒᵖ).obj ((Scheme.Γ ⋙ forget CommRingCat).mapCocone c.op).pt).obj (Opposite.op i)))
        s :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const Iᵒᵖ)
            ((Scheme.Γ ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).mapCocone
                c.op).pt)
          (Opposite.op i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Scheme.Γ ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).mapCocone
                    c.op).ι.app
              (Opposite.op i)) :
          (a : (fun (X : Type u) ↦ X) ((D.op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj (Opposite.op i))) →
            (fun (X : Type u) ↦ X)
              (((Functor.const Iᵒᵖ).obj ((Scheme.Γ ⋙ forget CommRingCat).mapCocone c.op).pt).obj (Opposite.op i)))
        0 :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const Iᵒᵖ)
            ((Scheme.Γ ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).mapCocone
                c.op).pt)
          (Opposite.op i)))
have dsimp : Eq (α :=
  ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) Γ(c.pt, ⊤))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
        (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(c.pt, ⊤) : Type u))
      s :
    (↑Γ(c.pt, ⊤) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
        (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(c.pt, ⊤) : Type u))
      0 :
    (↑Γ(c.pt, ⊤) : Type u))
Tactic: dsimp at hs ⊢