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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
            ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                Algebra.TensorProduct.includeRight)).coeff
        n =
      1 ∧
    ∀ i > n,
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
              ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight)).coeff
          i =
        0

Tactic:
nontriviality R

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
a✝ : Nontrivial R
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
            ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                Algebra.TensorProduct.includeRight)).coeff
        n =
      1 ∧
    ∀ i > n,
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
              ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight)).coeff
          i =
        0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : ∏ i ∈ s, (g i).leadingCoeff ≠ 0
⊢ f.resultant (∏ i ∈ s, g i) m = ∏ i ∈ s, f.resultant (g i) m

Tactic:
resultant_comm f

Goal state after:
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
m : ℕ
hm : f.natDegree ≤ m
hg : ∏ i ∈ s, (g i).leadingCoeff ≠ 0
⊢ (-1) ^ (m * (∏ i ∈ s, g i).natDegree) * (∏ i ∈ s, g i).resultant f (∏ i ∈ s, g i).natDegree m =
    ∏ x ∈ s, (-1) ^ (m * (g x).natDegree) * (g x).resultant f (g x).natDegree m
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ ((X - C r) ^ m).resultant g m n = eval r g ^ m

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ ((X - C r) ^ m).resultant g m n = eval r g ^ m
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
natDegree_scaleRoots,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
natDegree_scaleRoots,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝¹ : Nontrivial 𝓡
h✝ : Subsingleton (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
dsimp [UniversalFactorizationRing]; exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Subsingleton R
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
dsimp [UniversalFactorizationRing]; exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
natDegree_scaleRoots,

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) f.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) f.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
natDegree_scaleRoots,

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mem.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r s : R
⊢ ((taylor r) (X + C s)).resultant ((taylor r) g) = (X + C s).resultant g

Tactic:
nontriviality R

Goal state after:
case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ ((taylor r) (X + C s)).resultant ((taylor r) g) = (X + C s).resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)

Tactic:
nontriviality R

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
i : ℕ
hi : i < 1
j : ℕ
hj : j < 1
⊢ (Matrix.reindex e e) f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ = !![1] ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
obtain ⟨rfl⟩ : i = 0 := by lia

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
j : ℕ
hj : j < 1
hi : 0 < 1
⊢ (Matrix.reindex e e) f.sylvesterDeriv ⟨0, hi⟩ ⟨j, hj⟩ = !![1] ⟨0, hi⟩ ⟨j, hj⟩
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
hgq : ¬IsUnit (1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g))
m : Ideal (P.Fiber (Localization.Away e₀))
left✝ : m.IsMaximal
hm : Ideal.span {1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g)} ≤ m
⊢ (algebraMap R'' S) g ∈ q

Tactic:
have := H (m.comap (Algebra.TensorProduct.includeRight.toRingHom.comp (algebraMap _ _)))
      inferInstance (m.comap_liesOver P (Algebra.TensorProduct.includeRight.comp
        (IsScalarTower.toAlgHom _ _ _)))
        (Ideal.notMem_of_isUnit (m.comap Algebra.TensorProduct.includeRight)
        (IsLocalization.Away.algebraMap_isUnit _))

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝ : Algebra.IsIntegral R' (Localization.Away e₀)
hgq : ¬IsUnit (1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g))
m : Ideal (P.Fiber (Localization.Away e₀))
left✝ : m.IsMaximal
hm : Ideal.span {1 ⊗ₜ[R'] (algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g)} ≤ m
this :
  Ideal.comap (TensorProduct.includeRight.comp (algebraMap (R' ⊗[R] R'') (Localization.Away e₀))) m =
    Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
⊢ (algebraMap R'' S) g ∈ q
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FormallyUnramified T (T ⊗[R] S)
⊢ Subsingleton Ω[S⁄R]

Tactic:
let _ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FormallyUnramified T (T ⊗[R] S)
x✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
⊢ Subsingleton Ω[S⁄R]
Module: Mathlib.Topology.Sheaves.Module

Goal state before:
pp: X : TopCat
U : Opens ↑X
R : TopCat.Sheaf RingCat X
x✝ : (Opens ↥U)ᵒᵖ
⊢ ((U.overPullbackSheafEquivOver.app R).inv.hom ≫
          U.overEquivalence.symm.functor.op.whiskerLeft (U.sheafRestrictSheafEquivOver.app R).inv.hom ≫
            Functor.whiskerRight (NatTrans.op U.overEquivalence.symm.unit) (U.sheafRestrict.obj R).obj).app
      x✝ =
    (𝟙 (U.sheafRestrict.obj R).obj).app x✝

Tactic:
simp [overPullbackSheafEquivOver, sheafRestrictSheafEquivOver, eqToHom_map, overEquivalence,
    IsOpenMap.functor]

Goal state after:
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
⊢ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔ Function.Injective ⇑(algebraMap R S)

Tactic:
← PrimeSpectrum.comap_surjective_iff_injective_of_finite,

Goal state after:
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
⊢ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔ Function.Surjective (PrimeSpectrum.comap (algebraMap R S))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

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

Tactic:
rw [← isIso_comp_left_iff X.isoSpec.inv]

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ IsIso (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
⊢ IsIso f ↔ finrank f = 1

Tactic:
refine ⟨fun h ↦ finrank_eq_one_of_isIso f, fun h ↦ ?_⟩
  wlog hY : ∃ R, Y = Spec R
  · rw [← MorphismProperty.isomorphisms.iff,
      IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms Scheme) Y.affineCover]
    intro i
    dsimp [Scheme.Cover.pullbackHom]
    refine this _ ?_ ⟨_, rfl⟩
    ext y
    rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have _ : IsAffine X := isAffine_of_isAffineHom f
    rw [← isIso_comp_left_iff X.isoSpec.inv]
    refine this _ _ ?_ ⟨_, rfl⟩
    rw [finrank_comp_left_of_isIso, h]
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *
  algebraize [φ.hom]
  have : IsIso φ := by
    rw [ConcreteCategory.isIso_iff_bijective]
    apply Module.algebraMap_bijective_of_rankAtStalk
    rwa [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
⊢ ringKrullDim R + ↑(ENat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
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
⊢ Function.Injective ⇑(mulQuot a I)

Tactic:
simp only [mulQuot, Submodule.mapQ, ← ker_eq_bot]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.liftQ I (Submodule.mkQ (a • I) ∘ₗ (mul R R) a) ⋯).ker = ⊥
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Module.length R (R ⧸ span {0}) = Module.length R R

Tactic:
let m := (Submodule.quotEquivOfEqBot (Ideal.span {0} : Submodule R R) (span_singleton_zero))

Goal state after:
R : Type u_1
inst✝ : CommRing R
m : (R ⧸ span {0}) ≃ₗ[R] R := Submodule.quotEquivOfEqBot (span {0}) ⋯
⊢ Module.length R (R ⧸ span {0}) = Module.length R R
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x y : ↥X
hx : coheight x = 1
hy : coheight y = 1
f g : ↑X.functionField
hf : f ≠ 0
hg : g ≠ 0
⊢ ord f x ≤ ord g y ↔ (ordHom x hx) f ≤ (ordHom y hy) g

Tactic:
simp [ord_eq_unzero_ordHom hx hf, ord_eq_unzero_ordHom hy hg, Multiplicative.toAdd_le]

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 : ι
⊢ (Scheme.Hom.opensRange (Sigma.ι (fun i ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
Scheme.Hom.opensRange_comp

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 : ι
⊢ (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (fun i ↦ Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ
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
x : ProjectiveSpectrum 𝒜
⊢ f ∈ (⨅ (_ : x ∈ t), x.asHomogeneousIdeal).toIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal

Tactic:
rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]

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

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ∀ i ∈ Finset.image x Finset.univ, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩

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))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ (ConcreteCategory.hom
        ((Proj.structureSheaf 𝒜).presheaf.germ
          (ProjectiveSpectrum.basicOpen 𝒜 ↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den) x ⋯))
      (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s

Tactic:
refine Presheaf.germ_ext (C := CommRingCat) _ V hxV (homOfLE <| fun _ h' ↦ h ⟨_, h'⟩) i ?_

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 :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.map (homOfLE ⋯).op))
      (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.map i.op)) s
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 𝒜)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ (ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x)) (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) =
    Quotient.mk'' z

Tactic:
rw [homogeneousLocalizationToStalk, Quotient.liftOn'_mk'',
    stalkToFiberRingHom_germ, sectionInBasicOpen]

Goal state after:
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.622

Tactic:
apply GradedMonoid.toGradedMul.mul_mem (i := (j - m) • i) (j := (m + m - j) • i)

Goal state after:
case refine_2.a
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) ∈ 𝒜 ((j - m) • i)

case refine_2.a
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) b ^ (m + m - j) ∈ 𝒜 ((m + m - j) • i)