awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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
⊢ 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

Premises used: CategoryTheory.Over.Hom.left, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, CategoryTheory.Over.Hom.w, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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
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
hy : x ∈ Scheme.Hom.smoothLocus f
⊢ False

Tactic:
hx hy
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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
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
hy : x ∈ Scheme.Hom.smoothLocus f
⊢ False

Tactic:
exact hx hy
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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
hsnd : Smooth (X := Limits.pullback f g) (Limits.pullback.snd f g)
⊢ Smooth f

Tactic:
apply MorphismProperty.of_pullback_snd_of_descendsAlong
    (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (g := g)

Premises used: CategoryTheory.MorphismProperty.of_pullback_snd_of_descendsAlong
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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 Ω))
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) g

Tactic:
⟨⟨inferInstance, inferInstance⟩, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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 Ω))
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) g

Tactic:
exact ⟨⟨inferInstance, inferInstance⟩, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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 Ω))
this : GrpObj (Over.mk (Y := Limits.pullback f g) (Limits.pullback.snd f g)) := Over.grpObjMkPullbackSnd
⊢ Smooth (X := Limits.pullback f g) (Limits.pullback.snd f g)

Tactic:
smooth_of_grpObj_of_isAlgClosed _

Premises used: _private.0.AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed
-- Module: Mathlib.AlgebraicGeometry.Group.Smooth
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 Ω))
this : GrpObj (Over.mk (Y := Limits.pullback f g) (Limits.pullback.snd f g)) := Over.grpObjMkPullbackSnd
⊢ Smooth (X := Limits.pullback f g) (Limits.pullback.snd f g)

Tactic:
exact smooth_of_grpObj_of_isAlgClosed _

Premises used: _private.0.AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : I.ideal = J.ideal
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 ⋯).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
⊢ I = J

Tactic:
obtain ⟨i, _, s, hs⟩ := I
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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
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 ⋯).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 }
⊢ { ideal := i, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := s, supportSet_eq_iInter_zeroLocus := hs :
      X.IdealSheafData } =
    J

Tactic:
obtain ⟨j, _, t, ht⟩ := J
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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 : s = t
⊢ { 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 }

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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
e_supportSet₁ 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)))
⊢ s = t

Tactic:
rw [hs, ht]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ I ≤ J ↔ ∀ (U : (↑X.affineOpens : Type u)), I.ideal U ≤ J.ideal U

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
s : Set X.IdealSheafData
rw :
  sSup
    (Set.range (ι := { x : X.IdealSheafData // x ∈ s }) (ideal ∘ Subtype.val (p := fun (x : X.IdealSheafData) ↦ x ∈ s)))
| sSup (ideal '' s)

Tactic:
rw [← Subtype.range_val (s := s), ← Set.range_comp]

Premises used: Set.range_comp, Subtype.range_val
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
s : Set X.IdealSheafData
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)
⊢ sSup (ideal '' s) = ⨆ (i : (↑s : Type u)), (↑i : X.IdealSheafData).ideal

Tactic:
conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]

Premises used: Set.range_comp, Subtype.range_val
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
s : Set X.IdealSheafData
⊢ 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:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
s : Set X.IdealSheafData
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
s : Set X.IdealSheafData
this : sSup (ideal '' s) = ⨆ (i : (↑s : Type u)), (↑i : X.IdealSheafData).ideal
⊢ ∀ (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)

Tactic:
simp only [this, iSup_apply, Ideal.map_iSup, map_ideal_basicOpen, implies_true]

Premises used: implies_true, iSup_apply, Ideal.map_iSup, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ (ofIdeals I).ideal ≤ I

Tactic:
sSup_le (Set.forall_mem_image.mpr fun _ ↦ id)

Premises used: Iff.mpr, Set.Mem, id, sSup_le, Set.forall_mem_image
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ StrictMono.{u, u} (α := X.IdealSheafData) ideal

Tactic:
IdealSheafData.gci.strictMono_l

Premises used: GaloisCoinsertion.strictMono_l, AlgebraicGeometry.Scheme.IdealSheafData.gci
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Monotone.{u, u} (α := X.IdealSheafData) ideal

Tactic:
strictMono_ideal.monotone

Premises used: StrictMono.monotone, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Monotone.{u, u} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) ofIdeals

Tactic:
IdealSheafData.gci.gc.monotone_u

Premises used: GaloisConnection.monotone_u, GaloisCoinsertion.gc, AlgebraicGeometry.Scheme.IdealSheafData.gci
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
⊢ ofIdeals I.ideal = I

Tactic:
IdealSheafData.gci.u_l_eq _

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gci, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
J : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ I ≤ ofIdeals J ↔ I.ideal ≤ J

Tactic:
IdealSheafData.gci.gc.le_iff_le.symm

Premises used: GaloisConnection.le_iff_le, GaloisCoinsertion.gc, Iff.symm, AlgebraicGeometry.Scheme.IdealSheafData.gci
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (⊤ U))
      (⊤ (X.affineBasicOpen f))

Tactic:
simp [Ideal.map_top]

Premises used: Ideal.map_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
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
⊢ Eq.{u + 1} (α := Set ↥X) ⊥
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(⊤ U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
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:
simpa using X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (⊥ U))
      (⊥ (X.affineBasicOpen f))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
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
⊢ Eq.{u + 1} (α := Set ↥X) ⊤
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(⊥ U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
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:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).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
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
have inst := U.2.isLocalization_basicOpen f
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
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))
⊢ 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))

Tactic:
rw [← I.map_ideal_basicOpen U f, ← J.map_ideal_basicOpen U f, this]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen