mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
this✝ : (span {x}).IsPrime
this : p.FiniteHeight
hne : p ≠ span {x}
⊢ (span {x}).height = 0

Tactic:
← Order.lt_one_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
h1 : p.height = 1
x : R
hx : x ∈ p
hxp : Prime x
this✝ : (span {x}).IsPrime
this : p.FiniteHeight
hne : p ≠ span {x}
⊢ (span {x}).height < 1
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ IsReduced X

Tactic:
constructor
  intro U
  rcases U.1.eq_empty_or_nonempty with h | h
  · have : U = ⊥ := SetLike.ext' h
    have : Subsingleton Γ(X, U) :=
      CommRingCat.subsingleton_of_isTerminal (X.sheaf.isTerminalOfEqEmpty this)
    infer_instance
  · have : Nonempty U := by simpa
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
H : ¬∀ (z₁ z₂ : Set ↥X), IsClosed z₁ → IsClosed z₂ → Set.univ ⊆ z₁ ∪ z₂ → Set.univ ⊆ z₁ ∨ Set.univ ⊆ z₂
⊢ False

Tactic:
not_forall,

Goal state after:
X : Scheme
inst✝ : IsIntegral X
H : ∃ x x_1, ∃ (_ : IsClosed x) (_ : IsClosed x_1) (_ : Set.univ ⊆ x ∪ x_1), ¬(Set.univ ⊆ x ∨ Set.univ ⊆ x_1)
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE h ≫ 𝟙 ↑↑V = X.homOfLE h

Tactic:
Category.comp_id

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE h = X.homOfLE h
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f

Tactic:
rw [X.toRingedSpace.mem_basicOpen f x.1 x.2, ← not_iff_not, not_not]

Goal state after:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ ¬(ConcreteCategory.hom (X.evaluation x)) f = 0 ↔
    IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U ↑x ⋯)) f)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom ≫ 𝟙 R = (Scheme.ΓSpecIso R).hom

Tactic:
Category.comp_id

Goal state after:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom = (Scheme.ΓSpecIso R).hom
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫ 𝟙 S = φ

Tactic:
Category.comp_id

Goal state after:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ = φ
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ ∀ f_1 ∈ (ker f).ideal ⟨U, hU⟩, f x ∉ Y.basicOpen f_1

Tactic:
intro s hs hxs

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ (ker f).ideal ⟨U, hU⟩
hxs : f x ∈ Y.basicOpen s
⊢ False
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case refine_1
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ⟨x, ⟨f, hf⟩⟩.fst =
    ((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
        ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).fst

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint,
        Scheme.fromSpecStalk_closedPoint]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ 𝟙 ↑↑V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
Category.comp_id

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInl =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl

Tactic:
rw [← cancel_mono <| X.fromSpecResidueField T.x]
    simp_rw [Category.assoc, ← T.specTensorTo_fst, tensorCongr_SpecTensorTo_assoc]
    rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ IsIso X.toSpecΓ

Tactic:
refine HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
    (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ PrimeSpectrum.basicOpen ↑i ∈ (Spec Γ(X, ⊤)).affineOpens

case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
⊢ ⨆ i, ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩ = ⊤

case refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffine ↑(X.toSpecΓ ⁻¹ᵁ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩)

case refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x).1
h2 : (pullback.snd f g) z = (↑x).2
⊢ (↑((⇑(ConcreteCategory.hom (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) ∘
            ⇑(ConcreteCategory.hom (pullbackComparison forget f g)))
          z)).2 =
    (↑x).2

Tactic:
simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_snd]

Goal state after:
case h.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun X ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x).1
h2 : (pullback.snd f g) z = (↑x).2
⊢ (ConcreteCategory.hom (pullback.snd (forget.map f) (forget.map g)))
      ((ConcreteCategory.hom (pullbackComparison forget f g)) z) =
    (↑x).2
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hg : Surjective g
⊢ Surjective (pullback.fst f g)

Tactic:
simp only [surjective_iff, ← Set.range_eq_univ, Scheme.Pullback.range_fst] at hg ⊢

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hg : Set.range ⇑g = Set.univ
⊢ ⇑f ⁻¹' Set.range ⇑g = Set.univ
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ Submonoid.powers ↑r ≤ (adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))).toSubmonoid

pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)

Tactic:
· rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
      apply Algebra.subset_adjoin
      exact Or.inl (Or.inr r.2)

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = Hom.ker (pullback.fst f i ≫ 𝟙 X)

Tactic:
Category.comp_id

Goal state after:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = Hom.ker (pullback.fst f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ (MorphismProperty.Comma.Hom.hom f.unop).left ≫ Scheme.Hom.toImage (unop X).hom =
    Scheme.Hom.toImage (unop Y).hom ≫ Scheme.IdealSheafData.inclusion ⋯

Tactic:
← cancel_mono (Scheme.IdealSheafData.subschemeι _)

Goal state after:
X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ ((MorphismProperty.Comma.Hom.hom f.unop).left ≫ Scheme.Hom.toImage (unop X).hom) ≫
      (Scheme.Hom.ker (Over.hom (unop X).toComma)).subschemeι =
    (Scheme.Hom.toImage (unop Y).hom ≫ Scheme.IdealSheafData.inclusion ⋯) ≫
      (Scheme.Hom.ker (Over.hom (unop X).toComma)).subschemeι
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ fn i * g)) = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ Finset.univ.sup fn * g)) = 0

Tactic:
rw [map_mul, map_pow, map_mul, map_pow]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ fn i * g)) = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ Finset.univ.sup fn *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
⊢ (geometrically P).IsStableUnderBaseChange

Tactic:
rw [geometrically_eq_universally]

Goal state after:
P : ObjectProperty Scheme
⊢ (MorphismProperty.universally fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
⊢ IsZariskiLocalAtTarget (geometrically P)

Tactic:
rw [geometrically_eq_universally]

Goal state after:
P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
⊢ IsZariskiLocalAtTarget (MorphismProperty.universally fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

Tactic:
RingHom.injective_iff_ker_eq_bot,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ RingHom.ker (ConcreteCategory.hom (app f U)) = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed

Tactic:
rw [universallyClosed_eq]
    exact universally_mono fun X Y f ⟨h₁, h₂⟩ ↦ (isClosedMap_iff_specializingMap _).mpr h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (toSpecMvPolyIntEquiv n) (homOfVector f v ≫ toSpecMvPoly n S) i = v i

Tactic:
homOfVector_toSpecMvPoly,

Goal state after:
n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (toSpecMvPolyIntEquiv n) ((toSpecMvPolyIntEquiv n).symm v) i = v i
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S) ↘ S ≫ S.toSpecΓ ≫ S.isoSpec.inv = 𝔸(n; S) ↘ S

Tactic:
simp [Scheme.isoSpec]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝¹ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this✝ : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
val✝ : Fintype ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  (RingHom.pi fun i ↦
        (CommRingCat.Hom.hom (pushoutSection H hUST ⋯ ⋯)).comp
          ((CommRingCat.Hom.hom ⋯.isoPushout.hom).comp
            (Pi.evalRingHom (fun i ↦ ↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, VX i)) i))).comp
    (Algebra.TensorProduct.piRight ↑Γ(S, US) ↑Γ(S, US) ↑Γ(T, UT) fun i ↦ ↑Γ(X, VX i)).toRingEquiv.toRingHom
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) :=
  ⋯.isoPushout.symm
this :
  (ψY.comp (CommRingCat.Hom.hom (pushoutSection H hUST hUSX hUY))).comp (CommRingCat.Hom.hom e.inv) =
    φ.comp (Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ).toRingHom
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST hUSX hUY))

Tactic:
refine .of_comp (f := ψY) ?_
    convert (hφ.comp hψ').comp e.commRingCatIsoToRingEquiv.injective
    ext1 x; simpa using! congr($this (e.hom x))

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n]))) (𝔸(n; S) ↘ S)
    (terminal.from (Spec ℤ[n])) (terminal.from S)

Tactic:
convert! (IsPullback.of_hasPullback _ _).flip

Goal state after:
case e'_7
n : Type u
S T : Scheme
f : S ⟶ T
e_3✝ : 𝔸(n; S) = pullback (terminal.from S) (terminal.from (Spec ℤ[n]))
⊢ map n f ≫ pullback.snd (terminal.from T) (terminal.from (Spec ℤ[n])) =
    pullback.snd (terminal.from S) (terminal.from (Spec ℤ[n]))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
U V : Set X
hV : V ⊆ U
a✝ : X
⊢ (restrict 0 hV) a✝ = 0 a✝

Tactic:
restrict_apply

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
U V : Set X
hV : V ⊆ U
a✝ : X
⊢ (if a✝ ∈ V then 0 a✝ else 0) = 0 a✝
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z

Tactic:
by_cases hz : z ∉ U

Goal state after:
case pos
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz : z ∉ U
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z

case neg
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz : ¬z ∉ U
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))

Tactic:
RingHom.injective_iff_ker_eq_bot,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : RingHom.ker (ConcreteCategory.hom (X.presheaf.germ U x hx)) = ⊥
⊢ RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) = ⊥
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))

Tactic:
RingHom.injective_iff_ker_eq_bot,

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) = ⊥
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ i ∈ ↑(↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator

Tactic:
rw [SetLike.mem_coe, Submodule.mem_annihilator_span_singleton, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton, Submonoid.coe_finsetProd]

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ ∏ i ∈ s.attach, ↑(f ↑i ⋯) ∈ (↑R ∙ i).annihilator