awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (hypothesis)
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
⊢ False
have hα' : (Over.Hom.left α.hom) x = y
Tactic: have hα' : α.hom.left x = y := by
    simpa [x', y', pointEquivClosedPoint] using congr(($hα).left (IsLocalRing.closedPoint K))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (hypothesis)
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : IsReduced G
inst_4 : IsAlgClosed K
this_1 : JacobsonSpace.{u} ↥G
this : Nonempty.{u + 1} ↥G
H : (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f) : Set ↥G)ᶜ
hxc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) x
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : Membership.mem (γ := Set ↥G) (closedPoints ↥G) y
x' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) x hxc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
y' : (𝟙_ (Over (Spec (CommRingCat.of K)))) (𝒞 := instCategoryOver) ⟶ Over.mk f :=
  Over.homMk
    (↑(((pointEquivClosedPoint f).symm :
            (a : (↑(closedPoints ↥G) : Type u)) →
              { p : Spec (CommRingCat.of K) ⟶ G // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) })
          (Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Set ↥G) (closedPoints ↥G) x) y hyc)) :
      Spec (CommRingCat.of K) ⟶ G)
    ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
hα₁ : x' ≫ α.hom = y'
hα'₁ : (Over.Hom.left α.hom) x = y
⊢ False
have hy₁ : x ∈ Scheme.Hom.smoothLocus f
Tactic: rw! [← hα', ← α.hom.left.mem_preimage, Scheme.Hom.preimage_smoothLocus_eq,
    show α.hom.left ≫ f = f from α.hom.w] at hy
Cleared hypotheses: hy, hα, hα'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : GeometricallyReduced f
Ω : Type u := AlgebraicClosure K
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom (algebraMap K Ω))
⊢ Smooth f
have hg : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) g
Tactic: apply MorphismProperty.of_pullback_snd_of_descendsAlong
    (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (g := g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Group.Smooth (goal)
Goal:
K : Type u
inst : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst_1 : LocallyOfFiniteType f
inst_2 : GrpObj (Over.mk f)
inst_3 : GeometricallyReduced f
Ω : Type u := AlgebraicClosure K
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom (algebraMap K Ω))
hg : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) g
⊢ Smooth f
have hsnd : Smooth (X := Limits.pullback f g) (Limits.pullback.snd f g)
Tactic: apply MorphismProperty.of_pullback_snd_of_descendsAlong
    (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (g := g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I.ideal = J.ideal
⊢ I = J
have obtain : ∀ (i : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  (map_ideal_basicOpen :
    ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (i U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (i (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)))
  (s : Set ↥X) (hs : s = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
  (h :
    { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
          X.IdealSheafData }.ideal =
      J.ideal),
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    J
Tactic: obtain ⟨i, _, s, hs⟩ := I
Cleared hypotheses: I, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
J : X.IdealSheafData
i : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (i (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s : Set ↥X
hs : s = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
h :
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
        X.IdealSheafData }.ideal =
    J.ideal
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    J
have obtain : ∀ (j : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  (map_ideal_basicOpen_1 :
    ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
      Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (j U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (j (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)))
  (t : Set ↥X) (ht : t = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(j U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
  (h :
    { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
          X.IdealSheafData }.ideal =
      { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := t,
          supportSet_eq_iInter_zeroLocus := ht }.ideal),
  { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    { ideal := j, map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }
Tactic: obtain ⟨j, _, t, ht⟩ := J
Cleared hypotheses: J, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
i : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (i (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s : Set ↥X
hs : s = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
t : Set ↥X
map_ideal_basicOpen_1 :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
          ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
            U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          (X.affineBasicOpen f) :
        Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
ht :
  t =
    ⋂ (U : (↑X.affineOpens : Type u)),
      X.zeroLocus
        (↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                  supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    {
      ideal :=
        { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
            supportSet_eq_iInter_zeroLocus := hs }.ideal,
      map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := t, supportSet_eq_iInter_zeroLocus := ht }
have e_supportSet : s = t
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
i : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (i (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s : Set ↥X
hs : s = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
t : Set ↥X
map_ideal_basicOpen_1 :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
          ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
            U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          (X.affineBasicOpen f) :
        Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
ht :
  t =
    ⋂ (U : (↑X.affineOpens : Type u)),
      X.zeroLocus
        (↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                  supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ s = t
have e_supportSet : ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) = t
Tactic: rw [hs, ht]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
i : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (i U) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (i (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s : Set ↥X
hs : s = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
t : Set ↥X
map_ideal_basicOpen_1 :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
          ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
            U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      ({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
              supportSet_eq_iInter_zeroLocus := hs }.ideal
          (X.affineBasicOpen f) :
        Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
ht :
  t =
    ⋂ (U : (↑X.affineOpens : Type u)),
      X.zeroLocus
        (↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                  supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))
e_supportSet : ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) = t
⊢ s = t
have e_supportSet₁ : Eq.{u + 1} (α := Set ↥X)
  (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(i U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
  (⋂ (U : (↑X.affineOpens : Type u)),
    X.zeroLocus
      (↑({ ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s,
                supportSet_eq_iInter_zeroLocus := hs : X.IdealSheafData }.ideal
            U) :
        Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: rw [hs, ht]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
s : Set X.IdealSheafData
| sSup (ideal '' s)
have rw : sSup
  (Set.range (ι := { x : X.IdealSheafData // x ∈ s }) (ideal ∘ Subtype.val (p := fun (x : X.IdealSheafData) ↦ x ∈ s)))
Tactic: rw [← Subtype.range_val (s := s), ← Set.range_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
s : Set X.IdealSheafData
⊢ sSup (ideal '' s) = ⨆ (i : (↑s : Type u)), (↑i : X.IdealSheafData).ideal
have conv_lhs : Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  (sSup
    (Set.range (ι := { x : X.IdealSheafData // x ∈ s })
      (ideal ∘ Subtype.val (p := fun (x : X.IdealSheafData) ↦ x ∈ s))))
  (⨆ (i : (↑s : Type u)), (↑i : X.IdealSheafData).ideal)
Tactic: conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
s : Set X.IdealSheafData
⊢ ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (sSup (ideal '' s) U) =
      sSup (ideal '' s) (X.affineBasicOpen f)
have this : sSup (ideal '' s) = ⨆ (i : (↑s : Type u)), (↑i : X.IdealSheafData).ideal
Tactic: have : sSup (ideal '' s) = ⨆ i : s, ideal i.1 := by
        conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]
        rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := Set ↥X) ⊥
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(⊤ U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have h : ∀ (x : ↥X),
  Membership.mem (γ := Set ↥X) ⊥ x ↔
    Membership.mem (γ := Set ↥X)
      (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(⊤ U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := Set ↥X) ⊤
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(⊥ U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have h : ∀ (x : ↥X),
  Membership.mem (γ := Set ↥X) ⊤ x ↔
    Membership.mem (γ := Set ↥X)
      (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(⊥ U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) :
      Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
have this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op) =
  algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have : (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom = algebraMap _ _ := rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) :
      Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
have inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have inst := U.2.isLocalization_basicOpen f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) :
      Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, X.basicOpen f) : Type u))
have rw : Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
  (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U ⊓ J.ideal U))
  (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U) ⊓
    Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (J.ideal U))
Tactic: rw [← I.map_ideal_basicOpen U f, ← J.map_ideal_basicOpen U f, this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U ⊓ J.ideal U))
    (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
        (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U) ⊓
      Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
        (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (J.ideal U))
have h : ∀ (x : (↑Γ(X, X.basicOpen f) : Type u)),
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
        (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U ⊓ J.ideal U))
      x ↔
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U) ⊓
        Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (J.ideal U))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
⊢ Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
        (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U ⊓ J.ideal U))
      x ↔
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U) ⊓
        Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (J.ideal U))
      x
have h : ∀ (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) (s : ↥(Submonoid.powers f)),
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
        (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U ⊓ J.ideal U))
      (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s) ↔
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (I.ideal U) ⊓
        Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
          (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)) (J.ideal U))
      (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (.powers f) x
Cleared hypotheses: x