mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
⊢ quasiFiniteLocus f = ⊤ ↔ LocallyQuasiFinite f

Tactic:
refine ⟨fun H ↦ locallyQuasiFinite_iff_isDiscrete_preimage_singleton.mpr fun x ↦ ?_,
    fun _ ↦ f.quasiFiniteLocus_eq_top⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
x : ↥Y
⊢ _root_.IsDiscrete (⇑f ⁻¹' {x})
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hf₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(↑R h1Cotangentι) ⇑(↑R P.cotangentComplex)

Tactic:
exact P.exact_hCotangentι_cotangentComplex

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
⊢ IsIso f

Tactic:
← MorphismProperty.isomorphisms.iff,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
⊢ MorphismProperty.isomorphisms Scheme f
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
⊢ (CommRingCat.Hom.hom φ).Smooth

Tactic:
refine Algebra.Smooth.of_formallySmooth_fiber fun p hp ↦ ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ Algebra.FormallySmooth p.ResidueField (p.Fiber ↑S)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ I = (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ I ≤ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker

case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K
h : (valuation K (IsDiscreteValuationRing.maximalIdeal R)) x = (valuation K (IsDiscreteValuationRing.maximalIdeal R)) y
⊢ ∃ u, u • x = y

Tactic:
exact IsDiscreteValuationRing.associated_of_valuation_eq _ _ h

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx : coheight x = 1
hx' : x ∈ U
this : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x)
⊢ (ordHom x hx)
      ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ((ConcreteCategory.hom (X.presheaf.germ U x hx')) f)) =
    1

Tactic:
exact Ring.ordFrac_of_isUnit (hf.map (X.presheaf.germ U x hx').hom)

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))

Tactic:
convert_to! IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
inst✝¹ : CompactSpace ↥V
e : V ≅ Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → ↑(R i))) ⧸ ⊥))
inst✝ : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this✝ : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot ↑(CommRingCat.of ((i : ι) → ↑(R i)))).toCommRingCatIso.inv)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(vanishingIdeal t) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal

Tactic:
coe_vanishingIdeal,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
rid₁ : x✝ ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
x : A
hx : ∀ a ∈ DFinsupp.support ((decompose 𝒜) x), (proj 𝒜 a) x ∈ I
⊢ x ∈ I

Tactic:
simp_rw [proj_apply] at hx

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
rid₁ : x✝ ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
x : A
hx : ∀ a ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) a) ∈ I
⊢ x ∈ I
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

Tactic:
apply le_antisymm

Goal state after:
case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

case a
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
⊢ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso (𝟙 X) (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
        X.ringCatSheaf =
    𝟙 X.ringCatSheaf

Tactic:
by ext : 3; simp [← Functor.map_comp, SheafedSpace.sheaf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso (f ≫ g) (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun x ↦ eqToIso ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Z)).app
        Z.ringCatSheaf =
    {
        hom :=
          Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
            (Opens.grothendieckTopology ↥Y)).map
        {
          hom :=
            Functor.whiskerRight { app := fun U ↦ (Hom.appIso g (Opposite.unop U)).inv, naturality := ⋯ }
              (forget₂ CommRingCat RingCat) }

Tactic:
by ext : 3; simp [← Functor.map_comp, SheafedSpace.sheaf]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
f : A
d : ι
n : ℕ
hf : f ∈ 𝒜 d
x : A
hx : x ∈ 𝒜 (n • d)
⊢ f ^ n ∈ Submonoid.powers f

Tactic:
by use n

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ g ^ d ∈ 𝒜 (e • d)

Tactic:
convert! SetLike.pow_mem_graded d hg using 2

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ e • d = d • e
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j) ∈ 𝒜 (m * i)

Tactic:
rw [(_ : m * i = _)]
    apply GradedMonoid.toGradedMul.mul_mem (i := (j - m) • i) (j := (m + m - j) • i) <;> mem_tac
    rw [← add_smul]; congr; lia

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal

Tactic:
apply le_antisymm

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ Ideal.span (Set.range fun x ↦ x.snd.fst) ≤ (HomogeneousIdeal.irrelevant 𝒜).toIdeal

case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range fun x ↦ x.snd.fst)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r = X.basicOpen (f r)

Tactic:
apply le_antisymm

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r ≤ X.basicOpen (f r)

case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ X.basicOpen (f r) ≤ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t✝ : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
x : ↥(Spec R)
hxU : x ∈ unop U
r : ↑R
hxr : x ∈ ↑(basicOpen r)
hrU : basicOpen r ≤ unop U
this✝² :
  ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (unop U)))),
    (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) x) =
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) x)
t : ↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r)))
this✝¹ : Module ↑R ↑Γ(M, basicOpen r) := Module.compHom (↑Γ(M, basicOpen r)) (algebraMap ↑R ↑Γ(Spec R, basicOpen r))
this✝ : IsScalarTower ↑R ↑Γ(Spec R, basicOpen r) ↑Γ(M, basicOpen r)
this : Module ↑R ↑Γ(N, basicOpen r) := Module.compHom (↑Γ(N, basicOpen r)) (algebraMap ↑R ↑Γ(Spec R, basicOpen r))
⊢ (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) (t • (ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m) =
    t • (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m)

Tactic:
have : IsScalarTower R Γ(Spec R, basicOpen r) Γ(N, basicOpen r) :=
      .of_algebraMap_smul fun _ _ ↦ rfl

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t✝ : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
x : ↥(Spec R)
hxU : x ∈ unop U
r : ↑R
hxr : x ∈ ↑(basicOpen r)
hrU : basicOpen r ≤ unop U
this✝³ :
  ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (unop U)))),
    (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) x) =
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) x)
t : ↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r)))
this✝² : Module ↑R ↑Γ(M, basicOpen r) := Module.compHom (↑Γ(M, basicOpen r)) (algebraMap ↑R ↑Γ(Spec R, basicOpen r))
this✝¹ : IsScalarTower ↑R ↑Γ(Spec R, basicOpen r) ↑Γ(M, basicOpen r)
this✝ : Module ↑R ↑Γ(N, basicOpen r) := Module.compHom (↑Γ(N, basicOpen r)) (algebraMap ↑R ↑Γ(Spec R, basicOpen r))
this : IsScalarTower ↑R ↑Γ(Spec R, basicOpen r) ↑Γ(N, basicOpen r)
⊢ (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) (t • (ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m) =
    t • (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫ fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜 =
    (openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫
      X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A)))

Tactic:
simp only [fromOfGlobalSections, toBasicOpenOfGlobalSections, CommRingCat.ofHom_comp,
    Category.assoc, Scheme.Cover.ι_glueMorphisms_assoc, basicOpenIsoSpec_inv_ι_assoc,
    awayι_toSpecZero, Iso.inv_comp_eq]

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ X.toSpecΓ ∣_ PrimeSpectrum.basicOpen (f x.snd.fst) ≫
      (basicOpenIsoSpecAway (f x.snd.fst)).hom ≫
        Spec.map
            (CommRingCat.ofHom (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst)) ≫
              CommRingCat.ofHom (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers x.snd.fst))) =
    (X.isoOfEq ⋯).hom ≫
      (openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫
        X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) A) ≫ CommRingCat.ofHom f)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ X.toSpecΓ ∣_ PrimeSpectrum.basicOpen (f x.snd.fst) ≫
      (basicOpenIsoSpecAway (f x.snd.fst)).hom ≫
        Spec.map
            (CommRingCat.ofHom (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst)) ≫
              CommRingCat.ofHom (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers x.snd.fst))) =
    (X.isoOfEq ⋯).hom ≫
      (openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫
        X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) A) ≫ CommRingCat.ofHom f)

Tactic:
simp only [openCoverOfMapIrrelevantEqTop,
    Scheme.openCoverOfIsOpenCover_f, Scheme.isoOfEq_hom_ι_assoc, ← morphismRestrict_ι_assoc]

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ X.toSpecΓ ∣_ PrimeSpectrum.basicOpen (f x.snd.fst) ≫
      (basicOpenIsoSpecAway (f x.snd.fst)).hom ≫
        Spec.map
            (CommRingCat.ofHom (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst)) ≫
              CommRingCat.ofHom (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers x.snd.fst))) =
    X.toSpecΓ ∣_ PrimeSpectrum.basicOpen (f x.snd.fst) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen (f x.snd.fst)) ≫
        Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) A) ≫ CommRingCat.ofHom f)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case e_x.e_f
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
⊢ (fun i ↦ v i ^ ai i) = fun x ↦ v x ^ (ai x % d + d * (ai x / d))

Tactic:
ext i
      congr
      exact Eq.symm (Nat.mod_add_div (ai i) d)

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom ((toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯))
          (sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c))))

Tactic:
stalkIso'_germ

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ = val (↑(sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c)) ⟨p, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
M : (Spec S).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsLocalizing (modulesSpecToSheaf.obj ((Scheme.Modules.pushforward (Spec.map φ)).obj M))

Tactic:
← Functor.comp_obj,

Goal state after:
R S : CommRingCat
φ : R ⟶ S
M : (Spec S).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsLocalizing ((Scheme.Modules.pushforward (Spec.map φ) ⋙ modulesSpecToSheaf).obj M)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
⊢ IsMax R.toLocalSubring

Tactic:
intro S hS
  refine (LocalSubring.toSubring_injective (hS.1.antisymm fun x hx ↦ (R.2 x).elim id fun h ↦ ?_)).ge
  by_contra h'
  have hx0 : x ≠ 0 := by rintro rfl; exact h' R.zero_mem
  have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
    isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩
  obtain ⟨x', hx'⟩ := isUnit_iff_exists_inv.mp (hS.2.1 _ this)
  have : x' = x := by simpa [Subtype.ext_iff, inv_mul_eq_iff_eq_mul₀ hx0] using hx'
  exact h' (this ▸ x'.2)

Goal state after: