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)))
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 ⋯)
⊢ CategoryStruct.comp (Y := (↑(V F (↓k) ↓i) : Scheme)) (IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) ⋯)
      (tAux F (↓k) ↓i) =
    Iso.hom (Hom.isoOpensRange (F.map fi)) ≫ (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)
have h₂ : Subset (α := Set ↥(F.obj ↓k)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fk))
  (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
Tactic: generalize_proofs 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
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 ⋯)
h₂ :
  Subset (α := Set ↥(F.obj ↓k)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fk))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
⊢ IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) h₂ =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fk)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fk)))
      ((F.obj ↓k).homOfLE ⋯)
have rw : (Hom.opensRange (F.map fk)).ι =
  CategoryStruct.comp (Y := (↑(V F (↓k) ↓i) : Scheme)) ((F.obj ↓k).homOfLE sorry) (Opens.ι (V F (↓k) ↓i))
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 (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_1 :
  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 ⋯)
h₂ :
  Subset (α := Set ↥(F.obj ↓k)) (Set.range (ι := ↥(F.obj l)) ⇑(F.map fk))
    (Set.range (ι := ↥(↑(V F (↓k) ↓i) : Scheme)) ⇑(Opens.ι (V F (↓k) ↓i)))
this :
  IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) h₂ =
    CategoryStruct.comp (Y := (↑(Hom.opensRange (F.map fk)) : Scheme)) (Iso.hom (Hom.isoOpensRange (F.map fk)))
      ((F.obj ↓k).homOfLE ⋯)
⊢ IsOpenImmersion.lift (Opens.ι (V F (↓k) ↓i)) (F.map fk) h₂ ≫ 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 : (Hom.opensRange (F.map fi)).ι = (F.obj ↓i).homOfLE pf_5 ≫ Opens.ι (V F (↓i) ↓k)
Tactic: simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fk fi, Iso.hom_inv_id_assoc,
      ← 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 : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
⊢ IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
have this : Eq (α := (F.obj ↓i).Opens) (V F (↓i) ↓j) ⊤
Tactic: have : V F ↓i ↓j = ⊤ :=
      top_le_iff.mp (le_iSup_of_le ⟨_, 𝟙 _, f⟩ (by simp [Scheme.Hom.opensRange_of_isIso]))
-- 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 : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
⊢ Eq (α := F.obj ↓i ⟶ (glueData F).glued) (F.map f ≫ (glueData F).ι j) ((glueData F).ι i)
have this : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
Tactic: have : IsIso (V F ↓i ↓j).ι := by
    have : V F ↓i ↓j = ⊤ :=
      top_le_iff.mp (le_iSup_of_le ⟨_, 𝟙 _, f⟩ (by simp [Scheme.Hom.opensRange_of_isIso]))
    exact this ▸ (topIso _).isIso_hom
-- 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 : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
this : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
⊢ Eq (α := F.obj ↓i ⟶ (glueData F).glued) (F.map f ≫ (glueData F).ι j) ((glueData F).ι i)
have this₁ : Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (t F (↓i) ↓j ≫ Opens.ι (V F (↓j) ↓i) ≫ (glueData F).ι j)
  (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
Tactic: have : t F ↓i ↓j ≫ (V F ↓j ↓i).ι ≫ _ = (V F ↓i ↓j).ι ≫ _ :=
    (glueData F).glue_condition i j
-- 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 : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
this_1 : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
this :
  Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (t F (↓i) ↓j ≫ Opens.ι (V F (↓j) ↓i) ≫ (glueData F).ι j)
    (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
⊢ Eq (α := F.obj ↓i ⟶ (glueData F).glued) (F.map f ≫ (glueData F).ι j) ((glueData F).ι i)
have this₁ : Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (tAux F (↓i) ↓j ≫ (glueData F).ι j)
  (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
Tactic: simp only [t, IsOpenImmersion.lift_fac_assoc] at this
Cleared hypotheses: this
-- 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 : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
this_1 : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
this :
  Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (tAux F (↓i) ↓j ≫ (glueData F).ι j)
    (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
⊢ Eq (α := F.obj ↓i ⟶ (glueData F).glued) (F.map f ≫ (glueData F).ι j) ((glueData F).ι i)
have rw : Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued)
  (CategoryStruct.comp (Y :=
    (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    (CategoryStruct.comp (Y :=
        (↑(Hom.opensRange (X :=
              F.obj
                (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                  (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f))))
              (F.map
                (Sigma.snd.{w, v} (α := J) (β := fun (k : J) ↦ Prod.{v, v} (k ⟶ ↓i) (k ⟶ ↓j))
                    (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f) :
                      (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j))).1)) :
          Scheme))
        (Opens.ι (V F (↓i) ↓j) ≫ Iso.hom (Hom.isoOpensRange (F.map (𝟙 ↓i)))) ((F.obj ↓i).homOfLE sorry) :
      (↑(V F (↓i) ↓j) : Scheme) ⟶
        (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
          Scheme))
    (tAux F (↓i) ↓j ≫ (glueData F).ι j :
      (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
          Scheme) ⟶
        (glueData F).glued))
  (tAux F (↓i) ↓j ≫ (glueData F).ι j)
Tactic: rw [← cancel_epi (V F ↓i ↓j).ι, ← this, ← Category.assoc,
    ← (Iso.eq_inv_comp _).mp (homOfLE_tAux F ↓i ↓j (𝟙 _) f),
    ← Category.assoc, ← Category.assoc, Category.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 : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
this_1 : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
this :
  Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (tAux F (↓i) ↓j ≫ (glueData F).ι j)
    (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
⊢ Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued)
    (CategoryStruct.comp (Y :=
      (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
      (CategoryStruct.comp (Y :=
          (↑(Hom.opensRange (X :=
                F.obj
                  (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                    (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f))))
                (F.map
                  (Sigma.snd.{w, v} (α := J) (β := fun (k : J) ↦ Prod.{v, v} (k ⟶ ↓i) (k ⟶ ↓j))
                      (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f) :
                        (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j))).1)) :
            Scheme))
          (Opens.ι (V F (↓i) ↓j) ≫ Iso.hom (Hom.isoOpensRange (F.map (𝟙 ↓i)))) ((F.obj ↓i).homOfLE ⋯) :
        (↑(V F (↓i) ↓j) : Scheme) ⟶
          (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme))
      (tAux F (↓i) ↓j ≫ (glueData F).ι j :
        (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme) ⟶
          (glueData F).glued))
    (tAux F (↓i) ↓j ≫ (glueData F).ι j)
have h : (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme) =
    (↑(V F (↓i) ↓j) : Scheme) →
  CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (X :=
            F.obj
              (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f))))
            (F.map
              (Sigma.snd.{w, v} (α := J) (β := fun (k : J) ↦ Prod.{v, v} (k ⟶ ↓i) (k ⟶ ↓j))
                  (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f) :
                    (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j))).1)) :
        Scheme))
      (Opens.ι (V F (↓i) ↓j) ≫ Iso.hom (Hom.isoOpensRange (F.map (𝟙 ↓i)))) ((F.obj ↓i).homOfLE sorry) =
    𝟙 (↑(V F (↓i) ↓j) : Scheme)
Tactic: convert! Category.id_comp _
-- 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
s : Cocone F
i j : (glueData F).J
⊢ Eq (α := (glueData F).diagram.left (i, j) ⟶ s.pt)
    ((glueData F).diagram.fst (i, j) ≫
      (fun (i : (MultispanShape.prod (glueData F).J).R) ↦
          (s.ι.app ↓i : F.obj ↓i ⟶ Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) s.pt) ↓i))
        ((MultispanShape.prod (glueData F).J).fst (i, j)))
    ((glueData F).diagram.snd (i, j) ≫
      (fun (i : (MultispanShape.prod (glueData F).J).R) ↦
          (s.ι.app ↓i : F.obj ↓i ⟶ Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) s.pt) ↓i))
        ((MultispanShape.prod (glueData F).J).snd (i, j)))
have dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp [glueData, GlueData.diagram]
-- 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
s : Cocone F
i j : (glueData F).J
⊢ 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 [t, IsOpenImmersion.lift_fac]
-- 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
s : Cocone F
i j : (glueData F).J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have apply : ∀
  (k :
    PreZeroHypercover.I₀ (S :=
      (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))),
  PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
        k ≫
      Opens.ι (V F (↓i) ↓j) ≫ s.ι.app ↓i =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
        k ≫
      tAux F (↓i) ↓j ≫ s.ι.app ↓j
Tactic: apply (Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_
-- 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
s : Cocone F
i j : (glueData F).J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
⊢ PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
        k ≫
      Opens.ι (V F (↓i) ↓j) ≫ s.ι.app ↓i =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
        k ≫
      tAux F (↓i) ↓j ≫ s.ι.app ↓j
have simp : (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
  CategoryStruct.comp (Y :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    ((F.obj ↓i).homOfLE sorry :
      (↑(Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme) ⟶
        (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
          Scheme))
    (tAux F (↓i) ↓j ≫ s.ι.app ↓j :
      (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
          Scheme) ⟶
        s.pt)
Tactic: simp only [Opens.iSupOpenCover, V, Scheme.homOfLE_ι_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
s : Cocone F
i j : (glueData F).J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
⊢ (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
    CategoryStruct.comp (Y :=
      (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
      ((F.obj ↓i).homOfLE ⋯ :
        (↑(Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme) ⟶
          (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme))
      (tAux F (↓i) ↓j ≫ s.ι.app ↓j :
        (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme) ⟶
          s.pt)
have rw : Iso.hom (Hom.isoOpensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) ≫
    (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
  F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).2 ≫ s.ι.app ↓j
Tactic: rw [homOfLE_tAux_assoc F ↓i ↓j k.2.1 k.2.2, Iso.eq_inv_comp]