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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this : IsUnit (c * (b - a) + Polynomial.eval a (derivative f))
⊢ a = b

Tactic:
isUnit_iff_exists

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this :
  ∃ b_1,
    (c * (b - a) + Polynomial.eval a (derivative f)) * b_1 = 1 ∧
      b_1 * (c * (b - a) + Polynomial.eval a (derivative f)) = 1
⊢ a = b
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
⊢ ringKrullDim R = 1

Tactic:
· have : ¬ ringKrullDim R ≤ 0 := fun h ↦ by
      have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h
      exact hn Ring.KrullDimLE.isField_of_isDomain
    suffices h : Ring.KrullDimLE 1 R by
      rw [Ring.krullDimLE_iff] at h
      exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))
    refine Ring.krullDimLE_one_iff_of_noZeroDivisors.mpr fun I hI hI_prime ↦ ?_
    obtain ⟨x, hI, hx⟩ : ∃ (x : R), x ∈ I ∧ x ≠ 0 := by
      apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))
      simp only [ne_eq, not_exists, not_and, not_not] at h
      exact fun hx ↦ h x hx
    have : IsLocalRing.maximalIdeal R ≤ I := le_trans (h x hx)
      ((Ideal.IsRadical.radical_le_iff hI_prime.isRadical).mpr
        ((Ideal.span_singleton_le_iff_mem I).mpr hI))
    have := Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal R) hI_prime.ne_top this
    exact this ▸ (IsLocalRing.maximalIdeal.isMaximal R)

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

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊤

Tactic:
← WithBot.coe_top,

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ↑⊤
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o ↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm : closedPoint (Localization.AtPrime p₂.asIdeal) = e.symm ⟨p₂, ⋯⟩
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂

Tactic:
obtain ⟨q, hxq, h₀, h₁⟩ :=
    @exist_mem_one_of_mem_maximal_ideal (Localization.AtPrime p₂.1) _ _ _
      (e.symm ⟨p₁, h₁.le⟩) (e.symm ⟨p₀, (h₀.trans h₁).le⟩) (e.symm.lt_iff_lt.mpr h₀)
        (by simp [hm, h₁]) (algebraMap R (Localization.AtPrime p₂.1) x) <| by
          rw [← Localization.AtPrime.map_eq_maximalIdeal]
          exact mem_map_of_mem (algebraMap R (Localization.AtPrime p₂.1)) hx

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀✝ : p₀ < p₁
h₁✝ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o ↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm : closedPoint (Localization.AtPrime p₂.asIdeal) = e.symm ⟨p₂, ⋯⟩
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq : (algebraMap R (Localization.AtPrime p₂.asIdeal)) x ∈ q.asIdeal
h₀ : e.symm ⟨p₀, ⋯⟩ < q
h₁ : q.asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ x ∈ ((RelSeries.snoc Q (RelSeries.last p) ⋯).toFun 1).asIdeal

Tactic:
by simpa [h]

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
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    intro _
    apply LocalizedModule.instSubsingleton _
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ (Polynomial.idealX K).intValuation Polynomial.X = exp (-1)

Tactic:
exact intValuation_singleton _ Polynomial.X_ne_zero (idealX_span _)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ f.coeff (HahnSeries.order f + ↑m) = 0

Tactic:
← powerSeriesPart_coeff

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ (PowerSeries.coeff m) f.powerSeriesPart = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ f.coeff (HahnSeries.order f + ↑m) = 0

Tactic:
← powerSeriesPart_coeff

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ (PowerSeries.coeff m) f.powerSeriesPart = 0
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ weightedHomogeneousSubmodule R w n
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) φ) n'

Tactic:
weightedHomogeneousSubmodule_eq_finsupp_supported,

Goal state after:
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = n}
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) φ) n'
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ weightedHomogeneousSubmodule R w n
⊢ ∑ i, w i • (X i * (pderiv i) φ) = n • φ

Tactic:
weightedHomogeneousSubmodule_eq_finsupp_supported,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = n}
⊢ ∑ i, w i • (X i * (pderiv i) φ) = n • φ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P | Valued.v (P.2 - P.1) < ↑γ} ∈ uniformity K⸨X⸩

Tactic:
← hx

Goal state after:
case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P | Valued.v (P.2 - P.1) < Valued.v x} ∈ uniformity K⸨X⸩
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
⊢ UniformContinuous fun f ↦ f.coeff d

Tactic:
refine uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_
  let γ : (ℤᵐ⁰)ˣ := Units.mk0 (exp (-(d + 1))) coe_ne_zero
  use {P | Valued.v (P.snd - P.fst) < ↑γ}
  refine ⟨?_, fun _ hP ↦ ?_⟩
  · obtain ⟨x, hx⟩ := LaurentSeries.valuation_surjective K γ
    have : Valued.v.restrict x ≠ 0 := fun h ↦ NeZero.ne γ.1 <|
      hx ▸ MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff.1 h
    rw [← hx]
    nth_rw 2 [← Valuation.coe_ofClass]
    rw [← MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀]
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding]
    exact (Valued.hasBasis_uniformity K⸨X⸩ ℤᵐ⁰).mem_of_mem
      (i := Units.mk0 (Valued.v.restrict x) this) (by tauto)
  · simpa [eq_coeff_of_valuation_sub_lt K hP.le (lt_add_one _)] using mem_uniformity_of_eq hS rfl

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
⊢ (↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n) = esymmAlgHom τ R n

Tactic:
by
  ext i : 2
  simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_toAlgHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]

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

Goal state before:
pp: case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x

Tactic:
· intro r hr
    apply hc_gcd
    intro i
    simpa [coeff_sumSMulX] using hr (Finsupp.single i 1)

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

Goal state before:
pp: case inr.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (supDegree (⇑toLex) p)) j = (ofLex (supDegree (⇑toLex) p)) ((Equiv.swap i j) i)

Tactic:
Equiv.swap_apply_left

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_2
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⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ Valued.v.restrict ((algebraMap K⟮X⟯ K⸨X⸩) x✝¹.2 - (algebraMap K⟮X⟯ K⸨X⸩) x✝¹.1) < ↑d

Tactic:
rw [← map_sub, Valuation.restrict_lt_iff_lt_embedding]

Goal state after:
case h.refine_2
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⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ Valued.v ((algebraMap K⟮X⟯ K⸨X⸩) (x✝¹.2 - x✝¹.1)) < embedding ↑d
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case right.inr.ind
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
have hd :
      (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex).supDegree toLex = p.supDegree toLex := by
    rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]
    · exact accumulate_invAccumulate le_rfl hp.antitone_supDegree
    · rwa [Ne, leadingCoeff_eq_zero toLex.injective]

Goal state after:
case right.inr.ind
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ {t ∈ pairs σ k | #t.1 < k}.disjUnion ({t ∈ pairs σ k | #t.1 = k}) ⋯ = pairs σ k

Tactic:
grind [MvPolynomial.NewtonIdentities.pairs]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ Function.Bijective ⇑(esymmAlgHom (Fin n) R n)

Tactic:
use esymmAlgHom_fin_injective R le_rfl
  rintro ⟨p, hp⟩
  rw [← AlgHom.mem_range]
  obtain rfl | h0 := eq_or_ne p 0
  · exact Subalgebra.zero_mem _
  induction he : p.supDegree toLex using WellFoundedLT.induction generalizing p with | _ t ih
  subst he
  let t := Finsupp.equivFunOnFinite.symm (invAccumulate n n <| ↑(ofLex <| p.supDegree toLex))
  have hd :
      (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex).supDegree toLex = p.supDegree toLex := by
    rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]
    · exact accumulate_invAccumulate le_rfl hp.antitone_supDegree
    · rwa [Ne, leadingCoeff_eq_zero toLex.injective]
  obtain he | hne := eq_or_ne p (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex)
  · convert! AlgHom.mem_range_self _ (monomial t <| p.leadingCoeff toLex)
  have := (supDegree_sub_lt_of_leadingCoeff_eq toLex.injective hd.symm ?_).resolve_right hne
  · specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl
    · rwa [sub_ne_zero]
    convert! ← Subalgebra.add_mem _ ih ⟨monomial t (p.leadingCoeff toLex), rfl⟩
    apply sub_add_cancel p
  · rw [leadingCoeff_esymmAlgHomMonomial t le_rfl]

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
φ : 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

Tactic:
hc

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : 0 ≠ 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 : ι
⊢ ↑⟨single j i 1 • ∑ i, single i j 1 • ↑(v i), ⋯⟩ = ↑(v i)

Tactic:
simp only [Finset.smul_sum]

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
⊢ ∑ x, single j i 1 • single x j 1 • ↑(v x) = ↑(v i)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : K
⊢ HahnSeries.C x = (ofPowerSeries ℤ K) (PowerSeries.C x)

Tactic:
simp [C_apply, ofPowerSeries_C]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
k : ℕ
⊢ (bind₁ (xInTermsOfW p R)) (W_ R k) = X k

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum]

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ φ = wittStructureInt p Φ

Tactic:
by
  funext k
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  rw [map_wittStructureInt]
  -- Porting note: was `refine' congr_fun _ k`
  revert k
  refine congr_fun ?_
  apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))
  · intro n
    specialize h n
    apply_fun map (Int.castRingHom ℚ) at h
    simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial,
      AlgHom.coe_toRingHom] using h
  · intro n; apply wittStructureRat_prop

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

Goal state before:
pp: case zero
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ (bind₁ (wittMulN p 0)) (wittPolynomial p ℤ k) = ↑0 * wittPolynomial p ℤ k

Tactic:
simp [wittMulN, zero_mul, bind₁_zero_wittPolynomial]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ (fun n ↦ peval (φ n) ![x✝.coeff, y✝.coeff]) n = (fun n ↦ peval (ψ n) ![x✝.coeff, y✝.coeff]) n

Tactic:
poly_eq_of_wittPolynomial_bind_eq' p φ ψ

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ (fun n ↦ peval (ψ n) ![x✝.coeff, y✝.coeff]) n = (fun n ↦ peval (ψ n) ![x✝.coeff, y✝.coeff]) n

p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ ∀ (n : ℕ), (bind₁ φ) (wittPolynomial p ℤ n) = (bind₁ ψ) (wittPolynomial p ℤ n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.frobeniusFun.coeff n = (aeval x.coeff) (frobeniusPoly p n)

Tactic:
by
  rw [frobeniusFun, coeff_mk]

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

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

Tactic:
Finset.sum_eq_single 0,

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = r ^ p ^ n

case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ f (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) +
      f (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) =
    ∑ i ≤ n, f ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i

Tactic:
hc

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ f (↑p ^ (n + 1) * c) + f (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i) =
    ∑ i ≤ n, f ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i