-- 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₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((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)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
this_1 : IsOpenImmersion α
this : α y = x
⊢ ∃ (U_1 : (pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).Opens),
    x ∈ U_1 ∧
      U_1.ι ≫
          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)) ≫
              F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2 =
        U_1.ι ≫
          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)) ≫
              F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2
have H : (Hom.opensRange α).ι ≫
    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)) ≫
        F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2 =
  (Hom.opensRange α).ι ≫
    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)) ≫
        F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2
Tactic: refine ⟨α.opensRange, ⟨y, this⟩, ?_⟩