awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (hypothesis)
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑((gluedCover 𝒰).U (idx 𝒰 x)).toPresheafedSpace : TopCat))
          (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x)))) ≫ (fromGlued 𝒰).base) :
        (a : ↥((gluedCover 𝒰).U (idx 𝒰 x))) → ↥X)
      y =
    x
have h₁ : ((gluedCover 𝒰).ι (idx 𝒰 x) ≫ fromGlued 𝒰) y = x
Tactic: rw [← 𝒰.ι_fromGlued (𝒰.idx x)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
F : Scheme ⥤ PresheafedSpace CommRingCat :=
  forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
⊢ IsIso (F.map (fromGlued 𝒰))
have change : IsIso (fromGlued 𝒰).toPshHom
Tactic: change IsIso 𝒰.fromGlued.toPshHom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
⊢ X ⟶ Y
have refine : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued ⟶ Y
Tactic: refine inv 𝒰.ulift.fromGlued ≫ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
⊢ (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued ⟶ Y
have k : (b : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) →
  (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.right b ⟶ Y
Tactic: fapply Multicoequalizer.desc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
k :
  (b : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) →
    (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.right b ⟶ Y
⊢ (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued ⟶ Y
have h : ∀ (a : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).L),
  (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst a ≫
      f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).fst a)) =
    (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd a ≫
      f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).snd a))
Tactic: fapply Multicoequalizer.desc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
i j : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J
⊢ Eq (α := (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.left (i, j) ⟶ Y)
    ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst (i, j) ≫
      f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).fst (i, j))))
    ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd (i, j) ≫
      f (idx 𝒰 ((MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).snd (i, j))))
have h : Eq (α := pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
  (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 i)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst (i, j))
      (f (idx 𝒰 i)) :
    pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
  (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 j)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd (i, j))
      (f (idx 𝒰 j)) :
    pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
i j : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J
⊢ Eq (α := pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
    (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 i)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.fst (i, j))
        (f (idx 𝒰 i)) :
      pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
    (CategoryStruct.comp (Y := 𝒰.X (idx 𝒰 j)) ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram.snd (i, j))
        (f (idx 𝒰 j)) :
      pullback (X := 𝒰.X (idx 𝒰 i)) (Y := 𝒰.X (idx 𝒰 j)) (𝒰.f (idx 𝒰 i)) (𝒰.f (idx 𝒰 j)) ⟶ Y)
have h : pullback.fst ((ulift (P := IsOpenImmersion) 𝒰).f i) ((ulift (P := IsOpenImmersion) 𝒰).f j) ≫ f (idx 𝒰 i) =
  ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.t i j ≫ (ulift (P := IsOpenImmersion) 𝒰).gluedCover.f j i) ≫ f (idx 𝒰 j)
Tactic: change pullback.fst _ _ ≫ f _ = (_ ≫ _) ≫ f _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ f₁ = f₂
have rw : (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂
Tactic: rw [← cancel_epi 𝒰.ulift.fromGlued]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂
have h₁ : ∀ (b : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R),
  Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram b ≫
      (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ =
    Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram b ≫
      (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂
Tactic: apply Multicoequalizer.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
x : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R
⊢ Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram x ≫
      (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₁ =
    Multicoequalizer.π (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram x ≫
      (ulift (P := IsOpenImmersion) 𝒰).fromGlued ≫ f₂
have h₁ : (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₁ = (ulift (P := IsOpenImmersion) 𝒰).f x ≫ f₂
Tactic: rw [fromGlued, Multicoequalizer.π_desc_assoc, Multicoequalizer.π_desc_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
⊢ 𝒰.f x ≫ glueMorphisms 𝒰 f hf = f x
have refine : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀),
  (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf =
    (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ f x
Tactic: refine Cover.hom_ext (𝒰.ulift.pullback₁ (𝒰.f x)) _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf =
    (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).f i ≫ f x
have dsimp : Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
  (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf) (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x)
Tactic: dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, ulift_X, ulift_f, PreZeroHypercover.pullback₁_f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
x : 𝒰.I₀
i : (Precoverage.ZeroHypercover.pullback₁ (𝒰.f x) (ulift (P := IsOpenImmersion) 𝒰)).I₀
⊢ Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
    (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ 𝒰.f x ≫ glueMorphisms 𝒰 f hf) (pullback.fst (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f x)
have simp_rw : Eq (α := pullback (Y := 𝒰.X (idx 𝒰 i)) (𝒰.f x) (𝒰.f (idx 𝒰 i)) ⟶ Y)
  (pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫
    CategoryStruct.comp (Y := (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued)
      ((ulift (P := IsOpenImmersion) 𝒰).gluedCover.ι i)
      (Multicoequalizer.desc (ulift (P := IsOpenImmersion) 𝒰).gluedCover.diagram Y
        (fun (i : (MultispanShape.prod (ulift (P := IsOpenImmersion) 𝒰).gluedCover.J).R) ↦ f (idx 𝒰 i)) sorry))
  (pullback.snd (𝒰.f x) (𝒰.f (idx 𝒰 i)) ≫ f (idx 𝒰 i))
Tactic: simp_rw [pullback.condition_assoc, ← ulift_f, ← ι_fromGlued, Category.assoc, glueMorphisms,
    IsIso.hom_inv_id_assoc, ulift_f, hf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
H : ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
⊢ f = g
have choose : ∀ (U : (x : ↥X) → X.Opens) (hxU : ∀ (x : ↥X), x ∈ U x) (hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g), f = g
Tactic: choose U hxU hU using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X Y : Scheme
f g : X ⟶ Y
U : (x : ↥X) → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ PreZeroHypercover.presieve₀ { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι } ∈
    (precoverage IsOpenImmersion).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X } i))
          ⇑(PreZeroHypercover.f
              { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X } i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := ↥X, X := fun (i : ↥X) ↦ (↑(U i) : Scheme), f := fun (i : ↥X) ↦ (U i).ι : PreZeroHypercover X } i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ X)
    (fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) i)
    (snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) j)
have rw : Eq (α := pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f j)) (fst f (𝒰.f i)) (fst f (𝒰.f j)) ⟶ X)
  (CategoryStruct.comp (Y := pullback (𝒰.f i) (𝒰.f j))
    (Iso.hom (pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))) ≫
      map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) sorry sorry)
    (fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) i))
  (CategoryStruct.comp (Y := pullback (𝒰.f i) (𝒰.f j))
    (Iso.hom (pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))) ≫
      map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) sorry sorry)
    (snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦ CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (snd f (𝒰.f i))) (fst f (𝒰.f i))) j))
Tactic: rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ map (fst f (𝒰.f i) ≫ f)
      (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd _ _) (𝟙 _) (𝟙 _) (by simp) (by simp))]
-- 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).ι)
⊢ ∃ (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 : ∀ (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))),
  ∃ (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 ⟨k₁, y₁, hy₁⟩ := mem_iSup.mp ((pullback.fst (C := Scheme) _ _) x).2
-- 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))
⊢ ∃ (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 : ∀ (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 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 ⟨k₂, y₂, hy₂⟩ := mem_iSup.mp ((pullback.snd (C := Scheme) _ _) x).2
-- 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)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
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))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
⊢ IsOpenImmersion α
have inst : IsOpenImmersion (X := pullback (V F i j).ι (V F i k).ι) (pullback.fst (V F i j).ι (V F i k).ι)
Tactic: apply +allowSynthFailures IsOpenImmersion.of_comp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst_1 : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_3 : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
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))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
inst : IsOpenImmersion (X := pullback (V F i j).ι (V F i k).ι) (pullback.fst (V F i j).ι (V F i k).ι)
⊢ IsOpenImmersion α
have inst₁ : IsOpenImmersion (α ≫ pullback.fst (V F i j).ι (V F i k).ι)
Tactic: apply +allowSynthFailures IsOpenImmersion.of_comp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst_1 : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_3 : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
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))
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    (CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) : Scheme))
      (Iso.hom (Hom.isoOpensRange (F.map (hli ≫ k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
      ((F.obj i).homOfLE ⋯))
    ⋯
inst : IsOpenImmersion (X := pullback (V F i j).ι (V F i k).ι) (pullback.fst (V F i j).ι (V F i k).ι)
inst₁ : IsOpenImmersion (α ≫ pullback.fst (V F i j).ι (V F i k).ι)
⊢ IsOpenImmersion α
have Z : Scheme
Tactic: apply +allowSynthFailures IsOpenImmersion.of_comp