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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ 0 = x.coeff n

pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding

Tactic:
· contrapose! h
      exact order_le_of_coeff_ne_zero h.symm

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ exp ↑s * Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D)

Tactic:
mul_comm,

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) * exp ↑s ≤ exp (-D)
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
⊢ (algebraMap S Sₚ) (x * s') - mk' Sₚ x s ∈ Ideal.map (algebraMap S Sₚ) P

Tactic:
have h₁ : s.1 ∉ P := (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop

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
⊢ (algebraMap S Sₚ) (x * s') - mk' Sₚ x s ∈ Ideal.map (algebraMap S Sₚ) P
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
⊢ exp (-↑s) * Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-D)

Tactic:
mul_comm,

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) * exp (-↑s) ≤ exp (-D)
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
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ (Ideal.Quotient.mk P) ↑s * ((Ideal.Quotient.mk P) x * ((Ideal.Quotient.mk P) ↑s)⁻¹) = (Ideal.Quotient.mk P) x

Tactic:
mul_comm,

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
⊢ (Ideal.Quotient.mk P) x * ((Ideal.Quotient.mk P) ↑s)⁻¹ * (Ideal.Quotient.mk P) ↑s = (Ideal.Quotient.mk P) x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ exp (-d)
triv : ¬g = f
hn : n < d
⊢ g.coeff n - f.coeff n = 0

Tactic:
← HahnSeries.coeff_sub

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ exp (-d)
triv : ¬g = f
hn : n < d
⊢ (g - f).coeff n = 0
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ₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
h : Function.Bijective ⇑(algebraMap R₂ R₁)
⊢ Ideal.map (algebraMap R R₂) p = comap (algebraMap R₂ R₁) (Ideal.map (algebraMap R R₁) p)

Tactic:
IsScalarTower.algebraMap_eq R R₂ R₁,

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ₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
h : Function.Bijective ⇑(algebraMap R₂ R₁)
⊢ Ideal.map (algebraMap R R₂) p = comap (algebraMap R₂ R₁) (Ideal.map ((algebraMap R₂ R₁).comp (algebraMap R R₂)) p)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: 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
⊢ Irreducible f

Tactic:
have hfd : f.coeff d ≠ 0 := by simpa using hd
  let d₀ := d.erase i
  let φ : MvPolynomial n R := monomial d₀ (f.coeff d)
  let ψ : MvPolynomial n R := f - φ * X i
  have hf : f = φ * X i + ψ := by grind only
  have hφ : φ * X i = monomial d (f.coeff d) := by
    nth_rw 1 [← Finsupp.erase_add_single i d]; simp [φ, monomial_add_single, hdi, d₀]
  have hdψ (k) : ψ.coeff k = if d = k then 0 else f.coeff k := by
    simp +contextual [ψ, hφ, sub_eq_iff_eq_add, ite_add_ite]
  rw [hf]
  apply irreducible_mul_X_add
  · grind only [monomial_eq_zero]
  · simp [φ, hfd, d₀, hdi]
  · suffices ∀ x, d ≠ x → x ∈ f.support → i ∉ x.support by
      simpa [mem_vars_iff_mem_support, hdψ] using this
    exact fun x hxd hx hix ↦
      Finset.disjoint_iff_ne.mp (disjoint hd hx hxd) i (by simp [hdi]) _ hix rfl
  · rintro p hpφ ⟨q, hq⟩
    obtain ⟨m, b, hm, hb, rfl⟩ := (dvd_monomial_iff_exists hfd).mp hpφ
    obtain ⟨d₂, hd₂, H⟩ := nontrivial.exists_ne d
    obtain rfl : m = 0 := by
      have aux : coeff d₂ ψ ≠ 0 := by simpa [hdψ, H.symm] using hd₂
      simp only [hq, coeff_monomial_mul', ne_eq, ite_eq_right_iff, Classical.not_imp] at aux
      simpa using disjoint hd₂ hd H (Finsupp.support_mono aux.1)
        ((Finsupp.support_mono hm).trans (d.support.erase_subset i))
    have hb' : IsUnit b := isPrimitive _ fun k ↦
      if hk : k = d then hk ▸ hb else hf ▸ by simp [hq, hφ, Ne.symm hk]
    simpa

Goal state after:
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
⊢ (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

Tactic:
rw [dif_neg hkm.2, dif_pos hkm.1]; exact Nat.zero_lt_one

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

Goal state before:
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
⊢ ¬leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r) = 0

Tactic:
leadingCoeff_esymmAlgHomMonomial _ hnm

Goal state after:
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
⊢ ¬r = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ (ratfuncAdicComplRingEquiv K) { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) } =
    (ofPowerSeries ℤ K) PowerSeries.X

Tactic:
ratfuncAdicComplRingEquiv_apply,

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ ratfuncAdicComplPkg.compare (LaurentSeriesPkg K)
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm RatFunc.X) }.toCompletion =
    (ofPowerSeries ℤ K) PowerSeries.X
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ antidiagonal k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
rw [this, sum_singleton] at sub_both_sides

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
this : {a ∈ antidiagonal k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ ∑ i, r i * v i ≠ ∑ i, r i * w i

Tactic:
refine sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne <;>
  exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

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

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

Tactic:
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0,
    zero_mul, add_zero, map_sum, sum_congr rfl]

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

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0

Tactic:
mul_comm,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (C (⅟↑p ^ n) * (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * (0 - ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) = 0

Tactic:
zero_sub,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * -∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: case succ
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ (Quotient.out ((coeff (R ⧸ I) p (m + 1)) x) ^ p) ^ p ^ m ≡ x.teichmullerAux (m + 1) [SMOD I ^ (m + 1)]

Tactic:
exact .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := m) <| by
    simp [SModEq.idealQuotientMk, coeff_pow_p']

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
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) f)).leadingCoeff

Tactic:
← f.support_sum_monomial_coeff

Goal state after:
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
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
⊢ IsUnit
    ((MvPolynomial.finSuccEquiv k n)
        ((T f) (∑ v ∈ f.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff
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)
⊢ n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)

Tactic:
| ind n ih =>

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)
⊢ n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)
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)
⊢ n ∈ ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)).vars ∧
    ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)).vars ⊆ range (n + 1)

Tactic:
mul_comm,

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)
⊢ n ∈ (C (⅟↑p ^ n) * (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))).vars ∧
    (C (⅟↑p ^ n) * (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))).vars ⊆ range (n + 1)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))

Tactic:
by
      rw [bind₁_bind₁]; exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl

Goal state after:
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 : ℕ
H : ∃ a ∈ range n, i ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ i ∈ range n

Tactic:
rcases H with ⟨j, hj, H⟩

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 ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: 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 ≠ 0

Tactic:
exact mod_cast hp.1.ne_zero

Goal state after:
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)
H : ∃ a ∈ range n, n ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ False

Tactic:
rcases H with ⟨j, hj, H⟩

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 ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: 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 ≠ 0

Tactic:
exact mod_cast hp.1.ne_zero

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ C ↑p ^ k * xInTermsOfW p R k + ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k

Tactic:
mul_comm,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ xInTermsOfW p R k * C ↑p ^ k + ∑ x ∈ range k, C ↑p ^ x * (bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
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 × ℕ →₀ ℕ
⊢ (fun x ↦ ↑x)
      (1 / ↑p ^ n *
          coeff c
            ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n,
                C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i))).num =
    1 / ↑p ^ n *
      coeff c
        ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i))

Tactic:
mul_comm,

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 × ℕ →₀ ℕ
⊢ (fun x ↦ ↑x)
      (coeff c
            ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) *
          (1 / ↑p ^ n)).num =
    coeff c
        ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) *
      (1 / ↑p ^ n)