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

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

Tactic:
exact ⟨I, hI, isTorsionQuot_self F I⟩

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

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

Tactic:
rw [← Set.singleton_subset_iff, ← Ideal.span_le, Ideal.span_singleton_generator]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
r : Ideal (R ⧸ span t)
x✝ : (fun q ↦ q.IsPrime ∧ map f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map f (span {x}) ≤ r
⊢ span (insert x s) ≤ comap f r

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
r : Ideal (R ⧸ span t)
x✝ : (fun q ↦ q.IsPrime ∧ map f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map f (span {x}) ≤ r
⊢ comap f r ≤ p

Tactic:
· rw [span_le, Set.insert_subset_iff]
    have := map_le_iff_le_comap.mp hxr (subset_span rfl)
    refine ⟨this, hsp.trans ((hr.comap f).isRadical.radical_le_iff.mpr ?_)⟩
    rw [span_le, Set.insert_subset_iff]
    exact ⟨this, span_le.mp (mk_ker.symm.trans_le (ker_le_comap _))⟩

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
r : Ideal (R ⧸ span t)
x✝ : (fun q ↦ q.IsPrime ∧ map f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map f (span {x}) ≤ r
⊢ comap f r ≤ p
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ supportDim R M = ⊥

Tactic:
simpa [supportDim, support_eq_empty_iff]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p I : Ideal R
inst✝ : p.IsPrime
h : I ≤ p
⊢ ↑(Ideal.map (Ideal.Quotient.mk I) p).height + ↑(Submodule.spanFinrank I) ≤
    ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
· gcongr
    have : (Ideal.map (Ideal.Quotient.mk I) p).IsPrime :=
      Ideal.isPrime_map_quotientMk_of_isPrime h
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
this : (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
⊢ I = J

Tactic:
rw [← hI, ← hJ, this]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : ((id I').colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical

Tactic:
id_eq

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ ((id J').colon Set.univ).radical = (J'.colon Set.univ).radical

Tactic:
id_eq

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (J'.colon Set.univ).radical = (J'.colon Set.univ).radical
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
⊢ (t.inf fun x_1 ↦ ((id x_1).colon {x}).radical) = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical

Tactic:
id_eq

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
⊢ (t.inf fun x_1 ↦ (x_1.colon {x}).radical) = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
g' : ↥I →ₗ[R] M
a : ↥S
e : ↑a • g = (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ) (g', a).1
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype) a = g

Tactic:
obtain ⟨g', rfl⟩ := MB I g'

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype) a = g
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
f : V⸨X⸩
⊢ (derivative R) f = (hasseDeriv R 1) f

Tactic:
exact rfl

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Ideal.span {PowerSeries.X ^ d} ∣ Ideal.span {f}
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f

Tactic:
Ideal.span_singleton_dvd_span_singleton_iff_dvd

Goal state after:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : PowerSeries.X ^ d ∣ f
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ (∏ i, m i True.intro) i

Tactic:
rw [Fintype.prod_apply]

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ ∏ c, m c True.intro i
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 : φ ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = n}
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) φ) n'

Tactic:
AddMonoidAlgebra.supported_eq_span_single

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 : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {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 : φ ∈ AddMonoidAlgebra.supported R R {d | (weight w) d = n}
⊢ ∑ i, w i • (X i * (pderiv i) φ) = n • φ

Tactic:
AddMonoidAlgebra.supported_eq_span_single

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

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
this : ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
by
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
    apply this.mono fun _ hf ↦ hU₁ hf

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.IrreducibleQuadratic

Goal state before:
pp: case hd
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ ι a ∈ (sumSMulXSMulY c).support

Tactic:
MvPolynomial.mem_support_iff,

Goal state after:
case hd
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ coeff (ι a) (sumSMulXSMulY c) ≠ 0
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
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
⊢ p ∣ m i

Tactic:
have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
this : (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ p ∣ m i
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
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : (if m = p • d then 1 else 0) ≠ 0
this : (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ p ∣ m i

Tactic:
have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
d : σ →₀ ℕ
hd : (if m = p • d then 1 else 0) ≠ 0
this : (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
meq : m = p • d
⊢ p ∣ m i
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ ∀ {X Y : ModuleCat R} (f : X ⟶ Y),
    (ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).map f ≫
        (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑Y) i ≪≫ₗ
              fromModuleCatToModuleCatLinearEquiv R (↑Y) i).toModuleIso.hom =
      (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X) i ≪≫ₗ
              fromModuleCatToModuleCatLinearEquiv R (↑X) i).toModuleIso.hom ≫
        (𝟭 (ModuleCat R)).map f

Tactic:
intros
    ext
    simp [fromModuleCatToModuleCatLinearEquivtoModuleCatObj]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
by_cases h_le : m ≤ n

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
· rw [← hm, coeff_trunc', if_pos (nsmul_le_nsmul_right h_le p), coeff_expand_smul,
        MvPolynomial.coeff_expand_smul _ hp, coeff_trunc', if_pos h_le]

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a)).natDegree +
      ((Polynomial.X ^ v 0).natDegree +
        ∑ i, ((Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ).natDegree) =
    up ^ ↑0 * v 0 + ∑ i, up ^ ↑i.succ * v i.succ

Tactic:
natDegree_finSuccEquiv,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ degreeOf 0 (MvPolynomial.C a) +
      ((Polynomial.X ^ v 0).natDegree +
        ∑ i, ((Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ).natDegree) =
    up ^ ↑0 * v 0 + ∑ i, up ^ ↑i.succ * v i.succ
Module: Mathlib.RingTheory.Perfectoid.Untilt

Goal state before:
pp: O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
n : ℕ
⊢ untilt ((⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x) ^ p ^ n = untilt x

Tactic:
simp only [← map_pow]
  congr
  simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittSub p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n
  simp only [sub_zero, map_sub, constantCoeff_X]

Goal state after:
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 ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)

Tactic:
apply dvd_sub_pow_of_dvd_sub

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 ∣ (expand p) (wittStructureInt p Φ k) - wittStructureInt p Φ k ^ p
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)

Tactic:
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]

Goal state after:
case e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((eval₂Hom (RingHom.id ℤ) x).comp C)) fun i ↦
        (eval₂Hom ((↑ULift.ringEquiv.symm).comp (RingHom.id ℤ)) fun i ↦ ↑ULift.ringEquiv.symm (x i)) (φ i))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun n ↦ (aeval (mk p fun i ↦ { down := x i }).coeff) (φ n))
      (wittPolynomial p ℤ k)