awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
⊢ ∃ (U :
    (pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
        (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2))).Opens),
    x ∈ U ∧
      U.ι ≫
          pullback.lift
              (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
                (pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)) ≫
                  tAux F (↓i) ↓j)
                ⋯)
              (pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)) ≫
                t F (↓(i, j).1) ↓(i, j).2)
              ⋯ ≫
            pullback.lift
                (IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
                  (pullback.fst (Opens.ι (V F (↓(j, k).1) ↓(j, k).2)) (Opens.ι (V F (↓(j, i).1) ↓(j, i).2)) ≫
                    tAux F (↓j) ↓k)
                  ⋯)
                (pullback.fst (Opens.ι (V F (↓(j, k).1) ↓(j, k).2)) (Opens.ι (V F (↓(j, i).1) ↓(j, i).2)) ≫
                  t F (↓(j, k).1) ↓(j, k).2)
                ⋯ ≫
              pullback.lift
                (IsOpenImmersion.lift (Opens.ι (V F (↓i) ↓j))
                  (pullback.fst (Opens.ι (V F (↓(k, i).1) ↓(k, i).2)) (Opens.ι (V F (↓(k, j).1) ↓(k, j).2)) ≫
                    tAux F (↓k) ↓i)
                  ⋯)
                (pullback.fst (Opens.ι (V F (↓(k, i).1) ↓(k, i).2)) (Opens.ι (V F (↓(k, j).1) ↓(k, j).2)) ≫
                  t F (↓(k, i).1) ↓(k, i).2)
                ⋯ =
        U.ι ≫
          𝟙
            (pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
              (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
have this : ∃ (l : J) (fi : l ⟶ ↓(i, j).1) (fj : l ⟶ ↓(i, j).2) (fk : l ⟶ ↓(i, k).2) (α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)))
  (z : ↥(F.obj l)),
  IsOpenImmersion α ∧
    α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
        CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
          ((F.obj ↓(i, j).1).homOfLE sorry) ∧
      α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
          CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
            ((F.obj ↓(i, j).1).homOfLE sorry) ∧
        α z = x
Tactic: have := exists_of_pullback_V_V F x
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
⊢ (Hom.opensRange α).ι ≫
      pullback.lift
          (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
            (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ tAux F (↓i) ↓j) ⋯)
          (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫
            IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓i)) (tAux F (↓i) ↓j) ⋯)
          ⋯ ≫
        IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
            (pullback.fst (Opens.ι (V F (↓j) ↓k)) (Opens.ι (V F (↓j) ↓i)) ≫ tAux F (↓j) ↓k) ⋯ ≫
          tAux F (↓k) ↓i =
    (Hom.opensRange α).ι ≫ pullback.snd (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ Opens.ι (V F (↓i) ↓k)
have rw : (Hom.opensRange α).ι ≫
    IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
        (CategoryStruct.comp (Y :=
          pullback (X := (↑(V F (↓j) ↓k) : Scheme)) (Y := (↑(V F (↓j) ↓i) : Scheme)) (Opens.ι (V F (↓j) ↓k))
            (Opens.ι (V F (↓j) ↓i)))
          (pullback.lift
            (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
              (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ tAux F (↓i) ↓j) sorry)
            (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫
              IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓i)) (tAux F (↓i) ↓j) sorry)
            sorry)
          (pullback.fst (Opens.ι (V F (↓j) ↓k)) (Opens.ι (V F (↓j) ↓i)) ≫ tAux F (↓j) ↓k))
        sorry ≫
      tAux F (↓k) ↓i =
  (Hom.opensRange α).ι ≫ pullback.snd (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ Opens.ι (V F (↓i) ↓k)
Tactic: rw [IsOpenImmersion.comp_lift_assoc]
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
⊢ (Hom.opensRange α).ι ≫
      IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
          (CategoryStruct.comp (Y :=
            pullback (X := (↑(V F (↓j) ↓k) : Scheme)) (Y := (↑(V F (↓j) ↓i) : Scheme)) (Opens.ι (V F (↓j) ↓k))
              (Opens.ι (V F (↓j) ↓i)))
            (pullback.lift
              (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k))
                (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ tAux F (↓i) ↓j) ⋯)
              (pullback.fst (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫
                IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓i)) (tAux F (↓i) ↓j) ⋯)
              ⋯)
            (pullback.fst (Opens.ι (V F (↓j) ↓k)) (Opens.ι (V F (↓j) ↓i)) ≫ tAux F (↓j) ↓k))
          ⋯ ≫
        tAux F (↓k) ↓i =
    (Hom.opensRange α).ι ≫ pullback.snd (Opens.ι (V F (↓i) ↓j)) (Opens.ι (V F (↓i) ↓k)) ≫ Opens.ι (V F (↓i) ↓k)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app]
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← cancel_epi α.isoOpensRange.hom]
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp_rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp_rw [Scheme.Hom.isoOpensRange_hom_ι_assoc, IsOpenImmersion.comp_lift_assoc]
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [reassoc_of% hα₁, homOfLE_tAux F _ _ fi fj, Iso.hom_inv_id_assoc, reassoc_of% hα₂]
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
pf : IsOpenImmersion (X := (↑(V F (↓j) ↓k) : Scheme)) (Opens.ι (V F (↓j) ↓k))
h₁ :
  Subset (α := Set ↥(F.obj ↓j)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fj))
    (Set.range (ι := ↥(↑(V F (↓j) ↓k) : Scheme)) ⇑(Opens.ι (V F (↓j) ↓k)))
pf_1 : IsOpenImmersion (X := (↑(V F (↓k) ↓i) : Scheme)) (Opens.ι (V F (↓k) ↓i))
pf_2 :
  Subset (α := Set ↥(F.obj ↓k))
    (Set.range (ι := ↥(F.obj l)) ⇑(IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ ≫ tAux F (↓j) ↓k))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
pf_3 : IsOpenImmersion (F.map fi)
pf_4 :
  ∀ (k_1 : (k_1 : J) × (k_1 ⟶ ↓i) × (k_1 ⟶ ↓k)),
    IsOpenImmersion (F.map k_1.snd (β := fun (k_2 : J) ↦ (k_2 ⟶ ↓i) × (k_2 ⟶ ↓k)).1)
pf_5 : Hom.opensRange (F.map fi) ≤ V F (↓i) ↓k
⊢ IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fj)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fj)))
      ((F.obj ↓j).homOfLE ⋯)
have rw : (Hom.opensRange (F.map fj)).ι =
  CategoryStruct.comp (Y := (↑(V F (↓j) ↓k) : Scheme)) ((F.obj ↓j).homOfLE sorry) (Opens.ι (V F (↓j) ↓k))
Tactic: rw [← cancel_mono (Scheme.Opens.ι _), Category.assoc, IsOpenImmersion.lift_fac,
        ← Iso.inv_comp_eq, Scheme.Hom.isoOpensRange_inv_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
pf : IsOpenImmersion (X := (↑(V F (↓j) ↓k) : Scheme)) (Opens.ι (V F (↓j) ↓k))
h₁ :
  Subset (α := Set ↥(F.obj ↓j)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fj))
    (Set.range (ι := ↥(↑(V F (↓j) ↓k) : Scheme)) ⇑(Opens.ι (V F (↓j) ↓k)))
pf_1 : IsOpenImmersion (X := (↑(V F (↓k) ↓i) : Scheme)) (Opens.ι (V F (↓k) ↓i))
pf_2 :
  Subset (α := Set ↥(F.obj ↓k))
    (Set.range (ι := ↥(F.obj l)) ⇑(IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ ≫ tAux F (↓j) ↓k))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
pf_3 : IsOpenImmersion (F.map fi)
pf_4 :
  ∀ (k_1 : (k_1 : J) × (k_1 ⟶ ↓i) × (k_1 ⟶ ↓k)),
    IsOpenImmersion (F.map k_1.snd (β := fun (k_2 : J) ↦ (k_2 ⟶ ↓i) × (k_2 ⟶ ↓k)).1)
pf_5 : Hom.opensRange (F.map fi) ≤ V F (↓i) ↓k
⊢ IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
        (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ ≫ tAux F (↓j) ↓k) pf_2 ≫
      tAux F (↓k) ↓i =
    Iso.hom (Hom.isoOpensRange (F.map fi)) ≫ (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)
have this : IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ =
  CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fj)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fj)))
    ((F.obj ↓j).homOfLE sorry)
Tactic: have : IsOpenImmersion.lift (V F ↓j ↓k).ι (F.map fj) h₁ = (F.map fj).isoOpensRange.hom ≫
        (F.obj ↓j).homOfLE (le_iSup_of_le ⟨l, fj, fk⟩ le_rfl) := by
      rw [← cancel_mono (Scheme.Opens.ι _), Category.assoc, IsOpenImmersion.lift_fac,
        ← Iso.inv_comp_eq, Scheme.Hom.isoOpensRange_inv_comp]
      exact (Scheme.homOfLE_ι _ _).symm
-- 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
inst_4 : Small.{u, w} J
i j k : Shrink.{u, w} J
x :
  ↥(pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, k).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, k).1) ↓(i, k).2)))
l : J
fi : l ⟶ ↓(i, j).1
fj : l ⟶ ↓(i, j).2
fk : l ⟶ ↓(i, k).2
α :
  F.obj l ⟶
    pullback (X := (↑(V F (↓(i, j).1) ↓(i, j).2) : Scheme)) (Y := (↑(V F (↓(i, j).1) ↓(i, k).2) : Scheme))
      (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2))
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ :
  α ≫ pullback.fst (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
hα₂ :
  α ≫ pullback.snd (Opens.ι (V F (↓(i, j).1) ↓(i, j).2)) (Opens.ι (V F (↓(i, j).1) ↓(i, k).2)) =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fi)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fi)))
      ((F.obj ↓(i, j).1).homOfLE ⋯)
e : α z = x
pf : IsOpenImmersion (X := (↑(V F (↓j) ↓k) : Scheme)) (Opens.ι (V F (↓j) ↓k))
h₁ :
  Subset (α := Set ↥(F.obj ↓j)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fj))
    (Set.range (ι := ↥(↑(V F (↓j) ↓k) : Scheme)) ⇑(Opens.ι (V F (↓j) ↓k)))
pf_1 : IsOpenImmersion (X := (↑(V F (↓k) ↓i) : Scheme)) (Opens.ι (V F (↓k) ↓i))
pf_2 :
  Subset (α := Set ↥(F.obj ↓k))
    (Set.range (ι := ↥(F.obj l)) ⇑(IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ ≫ tAux F (↓j) ↓k))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
pf_3 : IsOpenImmersion (F.map fi)
pf_4 :
  ∀ (k_1 : (k_1 : J) × (k_1 ⟶ ↓i) × (k_1 ⟶ ↓k)),
    IsOpenImmersion (F.map k_1.snd (β := fun (k_2 : J) ↦ (k_2 ⟶ ↓i) × (k_2 ⟶ ↓k)).1)
pf_5 : Hom.opensRange (F.map fi) ≤ V F (↓i) ↓k
this :
  IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fj)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fj)))
      ((F.obj ↓j).homOfLE ⋯)
⊢ IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i))
        (IsOpenImmersion.lift (Opens.ι (V F (↓j) ↓k)) (F.map fj) h₁ ≫ tAux F (↓j) ↓k) pf_2 ≫
      tAux F (↓k) ↓i =
    Iso.hom (Hom.isoOpensRange (F.map fi)) ≫ (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)
have simp_rw : CategoryStruct.comp (Y := (↑(V F (↓k) ↓i) : Scheme)) (IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) sorry)
    (tAux F (↓k) ↓i) =
  Iso.hom (Hom.isoOpensRange (F.map fi)) ≫ (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)
Tactic: simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fj fk, Iso.hom_inv_id_assoc]