-- 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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
y₁ : ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))
hy₁ :
  Eq (α := ↥(F.obj i)) ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) y₁ : ↥(F.obj i))
    ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
y₂ : ↥(F.obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))
hy₂ :
  Eq (α := ↥(F.obj i)) ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1) y₂ : ↥(F.obj i))
    ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))
⊢ ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)),
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι =
          CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
            ((F.obj i).homOfLE ⋯) ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj i).homOfLE ⋯) ∧
          α z = x
have obtain : ∀ (l : J) (hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))
  (hlk : l ⟶ k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))) (z : (F ⋙ forget).obj l)
  (hy₁ :
    Eq (α := ↥(F.obj i))
      ((F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)
          ((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))
              z :
            (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
        ↥(F.obj i))
      ((↑((pullback.fst (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i)))
  (hy₂ :
    Eq (α := ↥(F.obj i))
      ((F.map k₂.snd (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k)).1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlk) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
              z :
            (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k_1 : J) ↦ (k_1 ⟶ i) × (k_1 ⟶ k))))) :
        ↥(F.obj i))
      ((↑((pullback.snd (V F i j).ι (V F i k).ι) x) : ↥(F.obj i)) : ↥(F.obj i))),
  ∃ (l : J) (fi : l ⟶ i) (fj : l ⟶ j) (fk : l ⟶ k) (α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι) (z : ↥(F.obj l)),
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι =
          CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
            ((F.obj i).homOfLE sorry) ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι =
            CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
              ((F.obj i).homOfLE sorry) ∧
          α z = x
Tactic: obtain ⟨l, hli, hlk, z, rfl, rfl⟩ :=
    (F ⋙ forget).exists_map_eq_of_isLocallyDirected k₁.2.1 k₂.2.1 y₁ y₂
      (by simpa [hy₁, hy₂] using congr($(pullback.condition (f := (V F i j).ι)) x))
Cleared hypotheses: y₁, hy₁, y₂, hy₂