mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
f : ι → R[X]
g : R[X]
n : ℕ
hn : g.natDegree ≤ n
a : ι
s : Finset ι
has : a ∉ s
IH :
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 →
    (∏ i ∈ s, f i).resultant g (∏ i ∈ s, f i).natDegree n = ∏ i ∈ s, (f i).resultant g (f i).natDegree n
hf : ∏ i ∈ insert a s, (f i).leadingCoeff ≠ 0
hf' : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (f a).leadingCoeff * (∏ x ∈ s, f x).leadingCoeff ≠ 0

Tactic:
simpa [*, leadingCoeff_prod'] using hf

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_4
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : R' ⊗[R] ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H' :
  ∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : ↑g ∉ q
hg : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom g)
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Pf : Ideal (Localization.Away f) := Ideal.map (algebraMap R' (Localization.Away f)) P
this✝⁷ : Pf.IsPrime
this✝⁶ : Pf.LiesOver P
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
this✝⁵ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this✝⁴ : IsScalarTower R' (R' ⊗[R] S) (Localization.Away f ⊗[R] S) :=
  IsScalarTower.of_algebraMap_eq' (Eq.symm (AlgHom.comp_algebraMap φ))
this✝³ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
P'f : Ideal (Localization.Away f ⊗[R] S) := Ideal.map (algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)) P'
hP'f : Disjoint ↑(Submonoid.powers (f ⊗ₜ[R] 1)) ↑P'
this✝² : P'f.IsPrime
this✝¹ : P'f.LiesOver P'
this✝ : P'f.LiesOver P
this : P'f.LiesOver Pf
⊢ ∀ (P'' : Ideal (Localization.Away f ⊗[R] S)),
    P''.IsPrime →
      P''.LiesOver Pf → (TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e ∉ P'' → P'' = P'f

Tactic:
intro P'' _ _ hP''
    have : P''.LiesOver P := .trans _ Pf _
    refine congr($(PrimeSpectrum.localization_comap_injective (R := R' ⊗[R] S)
      (Localization.Away f ⊗[R] S) (.powers (f ⊗ₜ 1)) (a₁ := ⟨P'', ‹_›⟩)
      (a₂ := ⟨P'f, ‹_›⟩) (PrimeSpectrum.ext ?_)).1)
    exact (H (P''.under _) inferInstance inferInstance hP'').trans (P'f.over_def P')

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
⊢ False

Tactic:
let y' : 𝟙_ _ ⟶ Over.mk f := Over.homMk _ ((pointEquivClosedPoint f).symm ⟨y, hyc⟩).2

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
⊢ False
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))

Tactic:
by_cases hr : Module.rankAtStalk S ⟨p, inferInstance⟩ = 0

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))

case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), WeaklyEtale f → MorphismProperty.diagonal (@WeaklyEtale) f

Tactic:
Y

Goal state after:
W X✝ Y✝ Z : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
⊢ ∀ (f : X ⟶ Y), WeaklyEtale f → MorphismProperty.diagonal (@WeaklyEtale) f
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ ord R ϖ = 1

Tactic:
by
  rw [Ring.ord, Module.length_eq_one_iff]
  have : (Ideal.span {ϖ}).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible hϖ
  rw [isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective (S := R ⧸ Ideal.span {ϖ})
    Ideal.Quotient.mk_surjective]
  let := Ideal.Quotient.field (Ideal.span {ϖ})
  exact instIsSimpleModule _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom

Tactic:
rw [whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(↑((ord R ↑x).lift ⋯)).toNat) =
    ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) ↑((ord R ↑x).lift ⋯)

Tactic:
ENat.recTopCoe_natCast,

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
x : ↥R⁰
⊢ ↑(Multiplicative.ofAdd ↑(↑((ord R ↑x).lift ⋯)).toNat) = ↑(Multiplicative.ofAdd ↑((ord R ↑x).lift ⋯))
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
a : R
ha : a ∈ R⁰
⊢ (ordMonoidWithZeroHom R) a ≠ 0

Tactic:
by
  lift a to R⁰ using ha
  simp [← ordMonoidWithZeroHom_eq_ordMonoidHom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
rw [whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i) ⁻¹' (zeroLocus t)ᶜ = Set.univ

Tactic:
Set.preimage_eq_univ_iff

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range (comap (Pi.evalRingHom (fun x ↦ ↑(R x)) i)) ⊆ (zeroLocus t)ᶜ
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (conjugateEquiv adj (adj'.comp (Adjunction.id b))) ((ρ_ l').hom ≫ φ) = (conjugateEquiv adj adj') φ ≫ (λ_ r').inv

Tactic:
simp only [conjugateEquiv_apply, Category.assoc, mateEquiv_comp_id_right, id_whiskerLeft,
    Iso.inv_hom_id, Category.comp_id, Iso.hom_inv_id, Iso.cancel_iso_inv_left,
    EmbeddingLike.apply_eq_iff_eq]
  bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
j₀ : 𝒰.I₀
i : { i // j i = j₀ }
⊢ Set.range ⇑(f ↑i) ⊆ Set.range ⇑(𝒰.f j₀)

Tactic:
by rcases i with ⟨i, rfl⟩; exact hj i

Goal state after:
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 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g

Tactic:
exact inf_le_right

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

Goal state before:
pp: case mpr
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u
⊢ f ∉ z.asHomogeneousIdeal

Tactic:
· obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
        exact fun rid => hz (z.1.2 i rid)

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den

Tactic:
by
  rw [ProjectiveSpectrum.mem_basicOpen]
  exact f.den_mem

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
⊢ homogeneousLocalizationToStalk 𝒜 x
      ((CommRingCat.Hom.hom (stalkToFiberRingHom 𝒜 x))
        ((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s)) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s

Tactic:
obtain ⟨V, hxV, i, n, a, b, h, e⟩ := s.2 ⟨x, hxU⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e : ∀ (x : ↥V), (fun x ↦ ↑s (i x)) x = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ homogeneousLocalizationToStalk 𝒜 x
      ((CommRingCat.Hom.hom (stalkToFiberRingHom 𝒜 x))
        ((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s)) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s
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
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 I.radical

Tactic:
rw [h.radical_eq]

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
h : IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime})
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ↑z.num ∈ (↑x).asHomogeneousIdeal.toIdeal ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal

pp: case hI
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑x).asHomogeneousIdeal.toIdeal.IsPrime

pp: case hM
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Disjoint ↑(Submonoid.powers f) ↑(↑x).asHomogeneousIdeal.toIdeal

pp: case hy
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsUnit (IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩)

Tactic:
· rfl

Goal state after:
case hI
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑x).asHomogeneousIdeal.toIdeal.IsPrime

case hM
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Disjoint ↑(Submonoid.powers f) ↑(↑x).asHomogeneousIdeal.toIdeal

case hy
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsUnit (IsLocalization.mk' (Localization (Submonoid.powers f)) 1 ⟨↑z.den, ⋯⟩)
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 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ (Localization.r (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl)
    ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩)
    (↑((fun x_1 ↦
              { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩,
                den_mem := ⋯ })
            { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
      ⟨↑((fun x_1 ↦
                { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩,
                  den_mem := ⋯ })
              { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
        ⋯⟩)

Tactic:
rw [Localization.r_iff_exists]

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ ∃ c,
    ↑c *
        (↑(↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
                ⟨↑((fun x_1 ↦
                          { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                            den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                        { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                  ⋯⟩).2 *
          ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).1) =
      ↑c *
        (↑((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).2 *
          (↑((fun x_1 ↦
                      { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                        den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).1)
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 = ⊤
H : Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ X.zeroLocus ↑(Ideal.span (Set.range fun x ↦ f x.snd.fst)) = ∅

Tactic:
Set.range_comp',

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, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
H : Ideal.span (Set.range fun x ↦ x.snd.fst) = (HomogeneousIdeal.irrelevant 𝒜).toIdeal
⊢ X.zeroLocus ↑(Ideal.span (⇑f '' Set.range fun x ↦ x.snd.fst)) = ∅
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case e_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 = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp (algebraMap (↥(𝒜 0)) (Localization.Away x.snd.fst)) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))

Tactic:
IsScalarTower.algebraMap_eq _ A,

Goal state after:
case e_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 = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp
      ((algebraMap A (Localization.Away x.snd.fst)).comp (algebraMap (↥(𝒜 0)) A)) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
⊢ ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙
            (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj).map
        i ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop g))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) =
    ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop f))
          (ModuleCat.Hom.hom
            (tilde.toOpen ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
          (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)) ⋯) ≫
      ((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).map i

Tactic:
let N := (modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)
        ext1
        apply IsLocalizedModule.ext (.powers (M := R) f.unop)
          (tilde.toOpen _ (PrimeSpectrum.basicOpen (R := R) f.unop)).hom
        · rw [Subtype.forall]
          change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _
          simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]
          obtain ⟨n, a, e⟩ : ∃ n, f.unop ∣ g.unop ^ n := by
            simpa only [Ideal.mem_radical_iff, Ideal.mem_span_singleton] using
              (basicOpen_le_basicOpen_iff _ _).mp (i.1.hom.le)
          refine ((Commute.isUnit_mul_iff (b := algebraMap R _ a) (.map (.all _ _) _)).mp ?_).1
          rw [← map_mul, ← e, map_pow]
          exact (M.isUnit_algebraMap_end_of_le_basicOpen g.unop le_rfl).pow n
        · dsimp [← ModuleCat.hom_comp]
          rw [tilde.toOpen_res_assoc]
          ext x
          dsimp
          simp only [IsLocalizedModule.lift_apply, ← ModuleCat.comp_apply, ← Functor.map_comp]
          rfl

Goal state after: