mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
hS' : span S ≤ hI.ideal_from_ringHom hJ hf
⊢ hJ.dpow n (f x) = f (hI.dpow n x)

Tactic:
← hS

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
hS' : I ≤ hI.ideal_from_ringHom hJ hf
⊢ hJ.dpow n (f x) = f (hI.dpow n x)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ʳ • x ^ n

Tactic:
inverse_eq_inv',

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • x ^ n
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inr
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this : IsScalarTower S (S × U) U
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
have : Etale S U := by
      have : Etale S (S × U) := Etale.of_equiv e
      exact .comp S (S × U) U

Goal state after:
case succ.inr
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝¹ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝ : IsScalarTower S (S × U) U
this : Etale S U
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
let P := Q.under R

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
⊢ ∃ σ, IsArithFrobAt R σ Q
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
⊢ (binomialFamily x r) n = 0 ^ n

Tactic:
by
  rw [binomialFamily, powerSeriesFamily_of_not_orderTop_pos hx]
  by_cases hn : n = 0 <;> simp [hn]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (powers x) c.1 * (PowerSeries.coeff c.2) b • (powers x) c.2).coeff g ≠ 0

Tactic:
rw [powers_of_orderTop_pos h c.1, powers_of_orderTop_pos h c.2, Algebra.smul_mul_assoc,
      Algebra.mul_smul_comm, ← pow_add, hcn]

Goal state after:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • x ^ n).coeff g ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ (Equiv e s).hsum.coeff g = s.hsum.coeff g

Tactic:
simp only [coeff_hsum, Equiv_toFun]

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : β), (s (e.symm i)).coeff g = ∑ᶠ (i : α), (s i).coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
⊢ ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support

Tactic:
refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd fun a ↦
      Set.VAddAntidiagonal.finite_of_isPWO (s ab.1).isPWO_support (t ab.2).isPWO_support a)

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : x ∈ ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support
⊢ x ∈ {a | (VAddAntidiagonal a ⋯).Nonempty}
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.Xzero)
aux₀ : PowerSeries.HasSubst F.Xzero
⊢ F.Xzero = F.Xzero

Tactic:
Xzero

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.Xzero)
aux₀ : PowerSeries.HasSubst F.Xzero
⊢ subst ![PowerSeries.X, 0] F.toPowerSeries = subst ![PowerSeries.X, 0] F.toPowerSeries
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

Tactic:
by_cases hd₀ : d 1 = 0
      · simp [hd₀, hd₁]
      simp [hd₁, PowerSeries.coeff_X_pow]
      grind

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x : R⟦Γ⟧
s : SummableFamily Γ' V α
⊢ (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum = (of R).symm (x • (of R) s.hsum)

Tactic:
hsum_equiv,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x : R⟦Γ⟧
s : SummableFamily Γ' V α
⊢ ((const Unit x).smul s).hsum = (of R).symm (x • (of R) s.hsum)
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
hκ : Fact (ℵ₀ ≤ κ)
⊢ 0 ∈ {x | x.cardSupp < κ}

Tactic:
simpa using aleph0_pos.trans_le hκ.out

Goal state after:
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp.mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
⊢ I ∈ ↑(F • F) → I ∈ ↑F

Tactic:
intro hI

Goal state after:
case mp.mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ ↑(F • F)
⊢ I ∈ ↑F
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp.mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
⊢ I ∈ ↑F → I ∈ ↑(F • F)

Tactic:
intro hI

Goal state after:
case mp.mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
hI : I ∈ ↑F
⊢ I ∈ ↑(F • F)
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsUniform ∧ F • F = F → F.IsGabriel

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
⊢ F.IsGabriel
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIN.refine_2.hy
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : comap f (map f q ^ n) ⊔ I = comap f (map f q ^ n.succ) ⊔ I
y : R
hy : y ∈ comap f (map f q ^ n.succ)
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx : f (Submodule.IsPrincipal.generator I) * f z ∈ map f q ^ n
⊢ ¬I ≤ q

Tactic:
exact fun e ↦ h₂.not_ge (hp.2 ⟨h₁, e⟩ h₂.le)

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
y : S
hx : (Quotient.mk (map (algebraMap R S) p)) y ∈ ↑P'
⊢ (Quotient.mk (map (algebraMap R S) p)) y ∈ ⇑(Quotient.mk (map (algebraMap R S) p)) '' ↑P

Tactic:
rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
y : S
hx : y ∈ P
⊢ (Quotient.mk (map (algebraMap R S) p)) y ∈ ⇑(Quotient.mk (map (algebraMap R S) p)) '' ↑P

case hIJ
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
y : S
hx : (Quotient.mk (map (algebraMap R S) p)) y ∈ P'
⊢ map (algebraMap R S) p ≤ P
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
hb : b ∈ q
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
⊢ x ∈ q

Tactic:
replace hb := q.smul_mem c hb

Goal state after:
case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
hb : ↑c • b ∈ q
⊢ x ∈ q
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

Tactic:
Ideal.count_associates_factors_eq

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P}))

case neg.hI
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Ideal.span {↑P} ≠ 0

case neg.hJ
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (idealX K).asIdeal.IsPrime

case neg.hJ₀
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (idealX K).asIdeal ≠ ⊥
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: case pos
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
i : ι
h₀ : 0 ∈ Submonoid.map (Pi.evalRingHom R i) M
this : Unique (S i)
⊢ Surjective (↑↑(algebraMap (R i) (S i))).1

Tactic:
exact surjective_to_subsingleton (algebraMap (R i) (S i))

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
p : Ideal R
inst✝¹⁵ : p.IsPrime
Rₚ : Type u_3
inst✝¹⁴ : CommRing Rₚ
inst✝¹³ : Algebra R Rₚ
inst✝¹² : IsLocalization.AtPrime Rₚ p
inst✝¹¹ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra S Sₚ
inst✝⁸ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁷ : Algebra Rₚ Sₚ
inst✝⁶ : IsDomain R
inst✝⁵ : IsDedekindDomain S
inst✝⁴ : IsTorsionFree R S
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : p.IsMaximal
hp : p ≠ ⊥
P : ↑(p.primesOver S)
this : NeZero p
⊢ (maximalIdeal Rₚ).inertiaDeg' ↑((primesOverEquivPrimesOver p Rₚ Sₚ hp) P) = p.inertiaDeg' ↑P

Tactic:
have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
    (ne_bot_of_mem_primesOver (NeZero.ne _) P.prop) inferInstance

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
p : Ideal R
inst✝¹⁵ : p.IsPrime
Rₚ : Type u_3
inst✝¹⁴ : CommRing Rₚ
inst✝¹³ : Algebra R Rₚ
inst✝¹² : IsLocalization.AtPrime Rₚ p
inst✝¹¹ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra S Sₚ
inst✝⁸ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁷ : Algebra Rₚ Sₚ
inst✝⁶ : IsDomain R
inst✝⁵ : IsDedekindDomain S
inst✝⁴ : IsTorsionFree R S
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : p.IsMaximal
hp : p ≠ ⊥
P : ↑(p.primesOver S)
this✝ : NeZero p
this : (↑P).IsMaximal
⊢ (maximalIdeal Rₚ).inertiaDeg' ↑((primesOverEquivPrimesOver p Rₚ Sₚ hp) P) = p.inertiaDeg' ↑P
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
⊢ ↑f.vars ⊆ Set.range Subtype.val

Tactic:
simpa [Set.subset_def]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : MvPolynomial n R
i : n
hig : i ∉ g.vars
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
f : S
hf0 : ((↑e.symm).comp Polynomial.CAlgHom).toRingHom f ≠ 0
hif : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f).vars
h : IsRelPrime (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f) g
⊢ ↑g.vars ⊆ Set.range Subtype.val

Tactic:
simpa [Set.subset_def]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hf0
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ φ ≠ 0

Tactic:
grind only [monomial_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ f ∈ closure (Set.range ⇑(algebraMap K⟮X⟯ K⸨X⸩)) ↔ f ∈ Set.univ

Tactic:
simp only [UniformSpace.mem_closure_iff_symm_ball, Set.mem_univ, iff_true, Set.Nonempty,
    Set.mem_inter_iff, Set.mem_range, exists_exists_eq_and]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ ∀ {V : Set (K⸨X⸩ × K⸨X⸩)},
    V ∈ uniformity K⸨X⸩ → SetRel.IsSymm V → ∃ a, (algebraMap K⟮X⟯ K⸨X⸩) a ∈ UniformSpace.ball f V
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective ⇑(esymmAlgHom σ R n)

Tactic:
rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]
  exact (AlgEquiv.injective _).comp (esymmAlgHom_fin_injective R hn)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case mul_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (p * X i) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
rw [map_mul]

Goal state after:
case mul_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p * (esymmAlgHom (Fin m) R m) (X i) ∈ (esymmAlgHom (Fin m) R n).range
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : (coeff (p • n)) ((expand p hp) φ) ≠ 0
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False

Tactic:
coeff_apply,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : (expand p hp) φ (p • n) ≠ 0
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
y : ↑M
hy : single j j 1 • y = ↑(v i)
⊢ single j i 1 • single i j 1 • ↑(v i) = ↑(v i)

Tactic:
simp [← mul_smul, ← hy]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f : MvPowerSeries σ R
⊢ IsRestricted |c| f ↔ IsRestricted c f

Tactic:
by
  simp [IsRestricted, NormedAddGroup.tendsto_nhds_zero, Finsupp.prod]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
⊢ ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop, (trunc' R m) ((map (frobenius R p)) ((expand p hp) f)) = (trunc' R m) (f ^ p)

Tactic:
Filter.frequently_atTop

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
⊢ ∀ (a : σ →₀ ℕ), ∃ b, a ≤ b ∧ (trunc' R b) ((map (frobenius R p)) ((expand p hp) f)) = (trunc' R b) (f ^ p)
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: case refine_2
k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
e : (p : Ideal k) → [inst : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun p [p.IsPrime] ↦
    have this := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
h : IsReduced (AlgebraicClosure k ⊗[k] A)
p : Ideal k
hp : p.IsPrime
⊢ IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)

Tactic:
· exact isReduced_of_injective _ (Algebra.TensorProduct.congr (e p).symm AlgEquiv.refl).injective

Goal state after: