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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑(Submodule.generators I).ncard = p.height

Tactic:
(IsNoetherian.noetherian I).generators_ncard

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑(Submodule.spanFinrank I) = p.height
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ I ≤ maximalIdeal R

Tactic:
exact le_maximalIdeal h

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ maximalIdeal R
⊢ x ∈ Ring.jacobson R

Tactic:
simpa [ringJacobson_eq_maximalIdeal R]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N

Tactic:
obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr ‹_› ⟨f, hf⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
⊢ Subring.center D = ⊤

Tactic:
induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
   =>  _ 

Goal state after:
case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
⊢ Subring.center D = ⊤
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n → injectiveDimension (M.localizedModule S) ≤ ↑↑n

Tactic:
simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n → projectiveDimension (M.localizedModule S) ≤ ↑↑n

Tactic:
simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
n : ℕ
⊢ projectiveDimension M ≤ ↑↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑↑n

Tactic:
simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
k : ℕ
ih : ∀ (f : V⸨X⸩), ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
f : V⸨X⸩
⊢ (k.factorial • (hasseDeriv R k) ((derivative R) f)).coeff n = ((k + 1).factorial • (hasseDeriv R (k + 1)) f).coeff n

Tactic:
derivative_apply,

Goal state after:
case succ
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
k : ℕ
ih : ∀ (f : V⸨X⸩), ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
f : V⸨X⸩
⊢ (k.factorial • (hasseDeriv R k) ((hasseDeriv R 1) f)).coeff n = ((k + 1).factorial • (hasseDeriv R (k + 1)) f).coeff n
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
⊢ (algebraMap S Sₚ) (x * s') - mk' Sₚ x s ∈ Ideal.map (algebraMap S Sₚ) P

Tactic:
have h₂ : algebraMap S Sₚ s ∉ Ideal.map (algebraMap S Sₚ) P := by
    rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ (algebraMap S Sₚ) (x * s') - mk' Sₚ x s ∈ Ideal.map (algebraMap S Sₚ) P
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n ↦ f.coeff ↑n)).coeff (Int.negSucc n) = 0

Tactic:
apply HahnSeries.embDomain_of_notMem_range

Goal state after:
case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ Int.negSucc n ∉ Set.range ⇑{ toFun := ⇑(Nat.castAddMonoidHom ℤ), inj' := ⋯, map_rel_iff' := ⋯ }
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0

Tactic:
apply HahnSeries.embDomain_of_notMem_range

Goal state after:
case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ n✝ ∉ Set.range ⇑{ toFun := ⇑(Nat.castAddMonoidHom ℤ), inj' := ⋯, map_rel_iff' := ⋯ }
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ∃ a, Valued.v a = n

Tactic:
use 0; simp [hn0]

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

Goal state before:
pp: case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
this : (accumulate n m) t ⟨↑i, ⋯⟩ = s ⟨↑i, ⋯⟩ + (accumulate n m) t ⟨↑i + 1, h⟩
⊢ t i = s i

Tactic:
accumulate_rec i.2 h t,

Goal state after:
case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
this : t ⟨↑i, ⋯⟩ + (accumulate n m) t ⟨↑i + 1, h⟩ = s ⟨↑i, ⋯⟩ + (accumulate n m) t ⟨↑i + 1, h⟩
⊢ t i = s i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
⊢ (ofLex (toLex (Finsupp.indicator t fun x x_1 ↦ 1))) k =
    (ofLex (toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1))) k

Tactic:
simp only [ofLex_toLex, Finsupp.indicator_apply]

Goal state after:
case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (toLex (Finsupp.indicator t fun x x_1 ↦ 1))) ((Iic ⟨i, him⟩ \ t).min' hne))
    ((ofLex (toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1))) ((Iic ⟨i, him⟩ \ t).min' hne))

Tactic:
simp only [ofLex_toLex, Finsupp.indicator_apply]

Goal state after:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ (if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ t then 1 else 0) <
    if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ then 1 else 0
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
⊢ (expand p hp) ((substAlgHom hf) φ) = subst (fun i ↦ (expand p hp) (f i)) φ

Tactic:
expand_substAlgHom,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
⊢ (substAlgHom ⋯) φ = subst (fun i ↦ (expand p hp) (f i)) φ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ (LaurentSeriesRingEquiv K).toRingHom ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers K⟮X⟯ (idealX K)

Tactic:
apply mem_integers_of_powerSeries

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ ↑((powerSeriesRingEquiv K) (PowerSeries.C a)) =
    ↑((((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C).codRestrict (adicCompletionIntegers K⟮X⟯ (idealX K)) ⋯)
        a)

Tactic:
powerSeriesRingEquiv_coe_apply,

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) (PowerSeries.C a)) =
    ↑((((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C).codRestrict (adicCompletionIntegers K⟮X⟯ (idealX K)) ⋯)
        a)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n

Tactic:
vars_C_mul

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n

case ind.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

Tactic:
vars_C_mul

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

case ind.hpq.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n

Tactic:
rw [mem_range]
    lia

Goal state after:
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.verschiebungFun.coeff i ^ p ^ (n + 1 - i) =
    ↑p * ∑ i ∈ Finset.range (n + 1), ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl,
    zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, add_zero, Finset.mul_sum, Finset.sum_congr rfl]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∀ x_1 ∈ Finset.range (n + 1),
    ↑p ^ (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
      ↑p * (↑p ^ x_1 * x.coeff x_1 ^ p ^ (n - x_1))
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ x.out.coeff ↑i = coeff i x

Tactic:
by
  rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]

Goal state after:
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (select P z).coeff n = x.coeff n

Tactic:
select,

Goal state after:
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (mk p fun n ↦ if P n then z.coeff n else 0).coeff n = x.coeff n
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (select (fun i ↦ ¬P i) z).coeff n = y.coeff n

Tactic:
select,

Goal state after:
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (mk p fun n ↦ if ¬P n then z.coeff n else 0).coeff n = y.coeff n
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ Function.LeftInverse (fun g ↦ ⟨fun k ↦ (truncate k).comp g, ⋯⟩) fun f ↦ lift ↑f ⋯

Tactic:
by rintro ⟨f, hf⟩; simp only [truncate_comp_lift]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ SMul.smul 0 f = 0

Tactic:
SMul.smul

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ ↑0 • f = 0
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ SMul.smul (n + 1) f = SMul.smul n f + f

Tactic:
SMul.smul

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑(n + 1) • f = ↑n • f + f
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
⊢ SMul.smul 0 f = 0

Tactic:
SMul.smul

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
⊢ ↑0 • f = 0
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ SMul.smul (↑n.succ) f = SMul.smul (↑n) f + f

Tactic:
SMul.smul

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑↑n.succ • f = ↑↑n • f + f
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ SMul.smul (Int.negSucc n) f = -SMul.smul (↑n.succ) f

Tactic:
SMul.smul

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑(Int.negSucc n) • f = -(↑↑n.succ • f)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
ht1 : (maximalIdeal R).height ≤ p.height
this :
  span (⇑(algebraMap R (Localization.AtPrime p)) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
simp only [← maximalIdeal_height_eq_ringKrullDim, ← IsLocalization.height_under p.primeCompl,
      IsLocalization.AtPrime.under_maximalIdeal _ p, ge_iff_le]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
ht1 : (maximalIdeal R).height ≤ p.height
this :
  span (⇑(algebraMap R (Localization.AtPrime p)) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ↑p.height
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
have lt : q < p := lt_of_le_of_ne qle (Ne.symm eq)

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
⊢ π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t

Tactic:
simp only [toFun_eq_rTensor_φ_toFun' _ ha, π]

Goal state after: