awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ (∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
    f₁ = f₂
have mpr : ∀ (f : ↥X) (snd : X.residueField f ⟶ CommRingCat.of K),
  (∃ (e :
      Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
    Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd = f₂
Tactic: obtain ⟨f, _⟩ := f₁
Cleared hypotheses: f₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
f : ↥X
snd : X.residueField f ⟶ CommRingCat.of K
⊢ (∃ (e :
      Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
    Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd = f₂
have mpr : ∀ (g : ↥X) (snd_1 : X.residueField g ⟶ CommRingCat.of K),
  (∃ (e :
      Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) g snd_1)),
      Eq (α :=
        X.residueField
            (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
              (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
          CommRingCat.of K)
        (Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) :
          X.residueField
              (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
            CommRingCat.of K)
        ((residueFieldCongr e).hom ≫
            Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
              (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) g snd_1) :
          X.residueField
              (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
            CommRingCat.of K)) →
    Eq (α := (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
      (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)
      (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) g snd_1)
Tactic: obtain ⟨g, _⟩ := f₂
Cleared hypotheses: f₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f_1 : X_2 ⟶ Y
K : Type u
inst : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ (fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
        (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
          (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
      ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
          Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
            X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
        f) =
    f
have rw : ∃ (e :
  Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
      ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
              (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
            (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
        ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
            Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
              X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          f)) =
    f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
  Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
      ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
              (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
            (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
        ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
            Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
              X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          f)) =
    (residueFieldCongr e).hom ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
Tactic: rw [SpecToEquivOfField_eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f_1 : X_2 ⟶ Y
K : Type u
inst : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ ∃ (e :
    Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
              (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
          ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
              Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
                X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            f)) =
      f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
    Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
              (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
          ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
              Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
                X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            f)) =
      (residueFieldCongr e).hom ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
have simp : Eq (α :=
  X.residueField
      ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
        ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
          ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))) ⟶
    CommRingCat.of K)
  (descResidueField
    (stalkClosedPointTo
      (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
        X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))
  (Iso.hom (residueFieldCongr sorry) ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))
Tactic: simp only [CommRingCat.coe_of, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply,
      Scheme.fromSpecResidueField_apply, exists_true_left]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ResidueField (goal)
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f_1 : X_2 ⟶ Y
K : Type u
inst : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ Eq (α :=
    X.residueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))) ⟶
      CommRingCat.of K)
    (descResidueField
      (stalkClosedPointTo
        (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
          X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))
    (Iso.hom (residueFieldCongr ⋯) ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))
have rw : CategoryStruct.comp (Y :=
    Spec
      (X.residueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))))
    (Spec.map
      (descResidueField
        (stalkClosedPointTo
          (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
            X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))
    (X.fromSpecResidueField
      ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
        ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
          ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))) =
  CategoryStruct.comp (Y :=
    Spec
      (X.residueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))))
    (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
      Spec.map (Iso.hom (residueFieldCongr sorry)))
    (X.fromSpecResidueField
      ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
        ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
          ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))))
Tactic: rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U V : X.Opens
W : (↑U : Scheme).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op
have simp : X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (homOfLE sorry)) = X.presheaf.map (homOfLE sorry).op
Tactic: simp only [Hom.appLE, ι_app, toScheme_presheaf_map, Quiver.Hom.unop_op,
    Hom.opensFunctor_map_homOfLE, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
W : (↑U : Scheme).Opens
⊢ U.ι ''ᵁ W ≤ U
have simp_rw : U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤
Tactic: simp_rw [← U.ι_image_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (Hom.appLE U.ι U ⊤ ⋯)
have simp : IsIso (X := Γ(X, U)) (Y := Γ((↑U : Scheme), ⊤)) (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: simp only [ι, ofRestrict_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (X := Γ(X, U)) (Y := Γ((↑U : Scheme), ⊤)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have change : IsIso (X.presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso sorry))))
Tactic: change IsIso (X.presheaf.map (eqToIso U.ι_image_top).hom.op)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
⊢ Nonempty.{u + 1} ↥(↑U : Scheme) ↔ (↑U : Set ↥X).Nonempty
have simp : (∃ (x : ↥X), x ∈ U) ↔ (↑U : Set ↥X).Nonempty
Tactic: simp only [toScheme_carrier, SetLike.coe_sort_coe, nonempty_subtype]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥U
⊢ (U.stalkIso x).inv = Hom.stalkMap U.ι x
have rw : 𝟙 ((↑U : Scheme).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
Tactic: rw [← Category.comp_id (U.stalkIso x).inv, Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥U
⊢ 𝟙 ((↑U : Scheme).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
have ih : ∀ (U_1 : TopologicalSpace.Opens ↥(↑U : Scheme)) (hxU : x ∈ U_1),
  (↑U : Scheme).presheaf.germ U_1 x hxU ≫ 𝟙 ((↑U : Scheme).presheaf.stalk x) =
    (↑U : Scheme).presheaf.germ U_1 x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
Tactic: apply TopCat.Presheaf.stalk_hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
⊢ (↑U : Scheme).presheaf.germ W x hxW ≫ 𝟙 ((↑U : Scheme).presheaf.stalk x) =
    (↑U : Scheme).presheaf.germ W x hxW ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
have ih : (↑U : Scheme).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) (↑x : ↥X) sorry ≫ Hom.stalkMap U.ι x
Tactic: simp only [Category.comp_id, U.germ_stalkIso_hom_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
⊢ (↑U : Scheme).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) (↑x : ↥X) ⋯ ≫ Hom.stalkMap U.ι x
have h : ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
    (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x) →
  Eq (α := (↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) ((↑U : Scheme).presheaf.germ W x hxW)
    (Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x sorry)
Tactic: convert! (Scheme.Hom.germ_stalkMap U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
e_1 :
  ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
    (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x)
⊢ Eq (α := (↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) ((↑U : Scheme).presheaf.germ W x hxW)
    (Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯)
have h : (Opens.map (Opens.inclusion' U)).1 (unop (op (U.ι ''ᵁ W))) ≤ W
Tactic: refine (U.toScheme.presheaf.germ_res (homOfLE ?_) _ _).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι } ∈
    (precoverage IsOpenImmersion).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
        { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                PreZeroHypercover.{u_1, u, u + 1} X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                PreZeroHypercover.{u_1, u, u + 1} X }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
        { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
          PreZeroHypercover.{u_1, u, u + 1} X }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
            PreZeroHypercover.{u_1, u, u + 1} X }
          i)
have refine : ∀ (x : ↥X),
  ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x
Tactic: refine ⟨fun x ↦ ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x
have hx : Membership.mem (γ := X.Opens) (⨆ (i : s), U i) x
Tactic: have hx : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : X.Opens) by trivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
hx : Membership.mem (γ := X.Opens) (⨆ (i : s), U i) x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x
have hx₁ : ∃ (i : s), x ∈ U i
Tactic: rw [Opens.mem_iSup] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
hx : ∃ (i : s), x ∈ U i
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x
have obtain : ∀ (i : s) (hi : x ∈ U i),
  ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x
Tactic: obtain ⟨i, hi⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Restrict (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
x : ↥X
i : s
hi : x ∈ U i
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
              PreZeroHypercover.{u_1, u, u + 1} X }
            i))
      x
have h : Membership.mem (γ := Set ↥X)
  (Set.range (ι :=
    ↥(PreZeroHypercover.X (S := X)
        { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
          PreZeroHypercover.{u_1, u, u + 1} X }
        i))
    ⇑(PreZeroHypercover.f { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι } i))
  x
Tactic: use i