-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
        ((pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
              Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
            x :
          ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
        ((pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
              Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
            x :
          ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
have simp : Eq (α := ↥(F.obj i))
  ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
      ((TopCat.Hom.hom
              (Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (Hom.toLRSHom'
                    (Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
            (a : ↥(↑(Hom.opensRange (F.map k₁.snd.1)) : Scheme)) → ↥(F.obj k₁.fst))
          ((TopCat.Hom.hom
                  (Hom.base
                    (LocallyRingedSpace.Hom.toHom
                      (Hom.toLRSHom' (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))))) :
                (a : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))) →
                  ↥(↑(Hom.opensRange (F.map k₁.snd.1)) : Scheme))
              x :
            ↥(↑(Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme)) :
        ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
    ↥(F.obj i))
  ((F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
      ((TopCat.Hom.hom
              (Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (Hom.toLRSHom'
                    (Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
            (a : ↥(↑(Hom.opensRange (F.map k₂.snd.1)) : Scheme)) → ↥(F.obj k₂.fst))
          ((TopCat.Hom.hom
                  (Hom.base
                    (LocallyRingedSpace.Hom.toHom
                      (Hom.toLRSHom' (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))))) :
                (a : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))) →
                  ↥(↑(Hom.opensRange (F.map k₂.snd.1)) : Scheme))
              x :
            ↥(↑(Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme)) :
        ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
    ↥(F.obj i))
Tactic: simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, Hom.comp_base, TopCat.hom_comp, ContinuousMap.comp_apply,
        TypeCat.Fun.coe_mk]