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
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span (insert x ↑s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
⊢ ↑t = Set.range t✝

Tactic:
simp [t]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : p ∈ (span ↑s).minimalPrimes
⊢ Cardinal.toENat (Submodule.spanRank (span ↑s)) ≤ ↑s.card

Tactic:
· simpa using Submodule.spanRank_span_le_card (s : Set R)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ I.height ≤ Cardinal.toENat (Submodule.spanRank I)

Tactic:
obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
  rw [I.height_eq_inf_minimalPrimes]
  exact (iInf₂_le J hJ).trans (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
⊢ Subring.center D = ⊤

Tactic:
cases nonempty_fintype D

Goal state after:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
⊢ Subring.center D = ⊤
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ Zx ≠ ⊤

Tactic:
by_contra! hZx

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx = ⊤
⊢ False
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx = ⊤
⊢ False

Tactic:
refine (ConjClasses.mk_bijOn (Dˣ)).mapsTo (Set.subset_center_units ?_) hx

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx = ⊤
⊢ x ∈ Units.val ⁻¹' Set.center D
Module: Mathlib.RingTheory.LittleWedderburn

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

Tactic:
cases nonempty_fintype D

Goal state after:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
⊢ Subring.center D = ⊤
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: 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
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ⟨y, hy⟩ ∈ Subring.center ↥R
⊢ x * y = y * x

Tactic:
by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
⊢ IsField D

Tactic:
cases nonempty_fintype D

Goal state after:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
⊢ IsField D
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
this : { asIdeal := q, isPrime := hq } ∈ PrimeSpectrum.basicOpen (f i)
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)

Tactic:
rw [← SetLike.mem_coe, ← PrimeSpectrum.localization_away_comap_range (T i)] at this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
this : { asIdeal := q, isPrime := hq } ∈ Set.range (PrimeSpectrum.comap (algebraMap S (T i)))
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this✝ : (i : ι) → Algebra ((i : ι) → S i) (S i) := fun i ↦ (Pi.evalAlgHom R S i).toAlgebra
this : ∀ (i : ι), IsLocalization.Away (Pi.single i 1) (S i)
⊢ IsLocalIso R ((i : ι) → S i)

Tactic:
apply of_span_range_eq_top (fun i ↦ Pi.single i (1 : S i)) _ fun i ↦ S i

Goal state after:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this✝ : (i : ι) → Algebra ((i : ι) → S i) (S i) := ⋯
this : ∀ (i : ι), IsLocalization.Away (Pi.single i 1) (S i)
⊢ Ideal.span (Set.range fun i ↦ Pi.single i 1) = ⊤
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case 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:
induction N with

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

Goal state before:
pp: 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 : WithBot ℕ∞
⊢ injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N

Tactic:
induction N with

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

Goal state before:
pp: case 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:
induction N with

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

Goal state before:
pp: 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 : WithBot ℕ∞
⊢ injectiveDimension M ≤ N ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ N

Tactic:
induction N with

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

Goal state before:
pp: case 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:
induction N with

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

Goal state before:
pp: 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 : WithBot ℕ∞
⊢ injectiveDimension M ≤ N ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ N

Tactic:
induction N with

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

Goal state before:
pp: case 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:
induction N with

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

Goal state before:
pp: 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 : WithBot ℕ∞
⊢ projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N

Tactic:
induction N with

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

Goal state before:
pp: case 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:
induction N with

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

Goal state before:
pp: 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 : WithBot ℕ∞
⊢ projectiveDimension M ≤ N ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ N

Tactic:
induction N with

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
⊢ (hasseDeriv R k) ((single n) x) = (single (n - ↑k)) (Ring.choose n k • x)

Tactic:
← Int.sub_add_cancel n k,

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
⊢ (hasseDeriv R k) ((single (n - ↑k + ↑k)) x) = (single (n - ↑k + ↑k - ↑k)) (Ring.choose (n - ↑k + ↑k) k • x)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

Tactic:
rw [coeff_nsmul]

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • ((hasseDeriv R (k + l)) f).coeff) n
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ {x | i + 1 ≤ ↑x} ↔ a✝ ≠ ⟨i, hin⟩ ∧ a✝ ∈ {x | i ≤ ↑x}

Tactic:
mem_filter_univ,

Goal state after:
case e'_3.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ i + 1 ≤ ↑a✝ ↔ a✝ ≠ ⟨i, hin⟩ ∧ i ≤ ↑a✝
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (if j ≤ ⟨↑i, him⟩ then 1 else 0) = if i ∈ {i | ↑j ≤ ↑i} then 1 else 0

Tactic:
mem_filter_univ,

Goal state after:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (if j ≤ ⟨↑i, him⟩ then 1 else 0) = if ↑j ≤ ↑i then 1 else 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ((accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝ • 1) =
    (accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝

pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1))

pp: case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

pp: case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0

Tactic:
nsmul_one,

Goal state after:
case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ ((accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => ↑b✝) = (accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝

case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1))

case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
x : K⸨X⸩
hx : Valued.v x = 0
⊢ Valued.v 0 = Valued.v x

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(MonoidWithZeroHom.ofClass Valued.v) x = 0

Tactic:
simp [hx]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ W_ R 1 = C ↑p * X 1 + X 0 ^ p

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, range_one, sum_singleton,
    one_mul, pow_one, C_1, pow_zero, tsub_self, tsub_zero]

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

Goal state before:
pp: p n : ℕ
⊢ ∑ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + C ↑(p ^ (n + 1)) * X (n + 1) ^ p ^ (n + 1 - (n + 1)) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))

Tactic:
CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)),

Goal state after:
p n : ℕ
⊢ ∑ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + C 0 * X (n + 1) ^ p ^ (n + 1 - (n + 1)) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
⊢ h v ≠ 0

Tactic:
simpa [h] using mem_support_iff.mp vin

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
h2 : h v ≠ 0
eq : (MvPolynomial.finSuccEquiv k n) ((T f) (h v)) = 0
⊢ h v = 0

Tactic:
by simpa only [map_eq_zero_iff _ (AlgEquiv.injective _)] using eq

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x : Perfection (R ⧸ I) p
this : (teichmuller p I) x ≡ Quotient.out ((coeff (R ⧸ I) p 0) x) ^ p ^ 0 [SMOD I]
⊢ (Ideal.Quotient.mk I) ((teichmuller p I) x) = (coeff (R ⧸ I) p 0) x

Tactic:
simpa [SModEq.idealQuotientMk] using this

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k) * ↑(p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
Nat.cast_pow,

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ k * ↑(p ^ (n - k + 1)) ∣
    ↑p ^ k * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case h.hn
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ≠ 0

pp: case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))

Tactic:
· exact mod_cast pow_ne_zero n hp.1.ne_zero

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))