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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
h : p.height ≤ n
⊢ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

Tactic:
obtain ⟨I, hI, e₁, e₂⟩ := exists_spanRank_eq_and_height_eq p (IsPrime.ne_top ‹_›)

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = ↑p.height
e₂ : I.height = p.height
⊢ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n
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
⊢ x ∈ ((RelSeries.eraseLast p).eraseLast.snoc q h2).last.asIdeal

Tactic:
simpa using! hxq

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
le : support R (QuotSMulTop x M) ⊆ support R M
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
let q : LTSeries (support R M) :=
    p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) (fun _ _ h ↦ h)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
le : support R (QuotSMulTop x M) ⊆ support R M
q : LTSeries ↑(support R M) := p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) ⋯
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
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 ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ d ∈ n.properDivisors

Tactic:
refine Nat.mem_properDivisors.mpr ⟨⟨_, (finrank_mul_finrank Z Zx D).symm⟩, ?_⟩

Goal state after:
case intro.mk
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 ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ d < n
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
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 ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ q ^ d < q ^ n

Tactic:
← card_D,

Goal state after:
case intro.mk
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 ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ q ^ d < card D
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⟧ := ⋯
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : 0 < D + ↑s
d : ℕ
hd : D + ↑s = ↑d
⊢ ∀ n < d, (PowerSeries.coeff n) F = 0

Tactic:
intro n hn

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 : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : 0 < D + ↑s
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
hn : n < d
⊢ (PowerSeries.coeff n) F = 0
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 : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : 0 < D + ↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D + ↑s))

Tactic:
· obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
        rw [hd]
        apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
        intro n hn
        rw [powerSeriesPart_coeff f n, hs]
        apply h_val_f
        lia

Goal state after:
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⟧ := ⋯
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
⊢ ∀ n < d, (PowerSeries.coeff n) F = 0

Tactic:
intro n hn

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
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
n : ℕ
hn : n < d
⊢ (PowerSeries.coeff n) F = 0
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
use ((HahnSeries.single (-WithZero.log n)) 1)

Goal state after:
case h
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ Valued.v ((single (-n.log)) 1) = 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 → ℕ
⊢ {x | i + 1 ≤ ↑x} = {x | i ≤ ↑x}.erase ⟨i, hin⟩

pp: case convert_3
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ DecidableEq (Fin n)

pp: case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ {x | i ≤ ↑x}

Tactic:
· ext
    rw [mem_erase]
    simp_rw [mem_filter_univ, i.succ_le_iff, lt_iff_le_and_ne]
    rw [and_comm, ne_comm, ← Fin.val_ne_iff]

Goal state after:
case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ {x | i ≤ ↑x}
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
D : ℤ := ⋯
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
⊢ ∀ n < D, (x✝ - limit hℱ).coeff n = 0

Tactic:
intro n hn

Goal state after:
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
D : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
hD : exp (-D) < embedding ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
n : ℤ
hn : n < D
⊢ (x✝ - limit hℱ).coeff n = 0
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
h : ∀ m ∈ (sumSMulX c).support, ∀ (x : n), m x = 0
i : n
hi : c i ≠ 0
⊢ False

Tactic:
specialize h (Finsupp.single i 1) (by
        rwa [mem_support_iff, coeff_sumSMulX]) i

Goal state after:
case a
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
i : n
h : (Finsupp.single i 1) i = 0
hi : c i ≠ 0
⊢ False
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
by_cases! ord_nonpos : f.order < 0

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: 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)))
⊢ leadingCoeff (⇑toLex) p ≠ 0

Tactic:
rwa [Ne, leadingCoeff_eq_zero toLex.injective]

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
m : σ →₀ ℕ
⊢ (coeff (p • m)) ((expand p hp) φ) = (coeff m) φ

Tactic:
simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp), smul_eq_mul]
  have {d : σ →₀ ℕ} : (d.prod fun s e ↦ (X s (R := R) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [finsum_eq_single _ m]
  · rw [this, coeff_monomial, if_pos rfl, mul_one]
  · intro d hd
    rw [this, coeff_monomial, if_neg _, mul_zero]
    simp [nsmul_right_inj hp, hd.symm]

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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
⊢ (coeff d) ((expand p hp) φ) = 0

Tactic:
obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
          by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ (coeff d) ((expand p hp) φ) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ (fun x ↦ 0) n ≤ ‖(coeff n) (f + g)‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2

Tactic:
dsimp [Finsupp.prod]; positivity

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ n.prod fun x1 x2 ↦ |c| x1 ^ x2

Tactic:
dsimp [Finsupp.prod]; positivity

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers K⟮X⟯ (idealX K)

Tactic:
rw [mem_adicCompletionIntegers, valuation_compare, val_le_one_iff_eq_coe]
  exact ⟨F, rfl⟩

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
v : Fin (n + 1) →₀ ℕ
this : ∀ (j : Fin (n + 1)), ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1
⊢ MvPolynomial.C (MvPolynomial.coeff v f) *
      ∏ x, ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X x))).leadingCoeff ^ v x =
    MvPolynomial.C (MvPolynomial.coeff v f)

Tactic:
simp only [this, one_pow, Finset.prod_const_one, mul_one]

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 y : Perfection (R ⧸ I) p
⊢ (x * y).teichmullerFun = x.teichmullerFun * y.teichmullerFun

Tactic:
refine teichmullerFun_spec fun n ↦ ?_
    refine ⟨(coeff _ p n x).out * (coeff _ p n y).out, by simp, ?_⟩
    rw [mul_pow]
    refine (teichmullerFun_sModEq ?_).symm.mul (teichmullerFun_sModEq ?_).symm <;> simp

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

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

Tactic:
simp only [map_pow, map_mul, algHom_C, algebraMap_eq]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → 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 : ℕ → ℤ
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)

Tactic:
specialize h (ULift ℤ) (mk p fun i => ⟨x i⟩) k

Goal state after:
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 : (ghostComponent k) (f (mk p fun i ↦ { down := x i })) = (ghostComponent k) (g (mk p fun i ↦ { down := x i }))
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (map (Int.castRingHom R)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n))

Tactic:
hom_bind₁

Goal state after:
case e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ =
    (map (Int.castRingHom R)) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ)

Tactic:
hom_bind₁

Goal state after:
case e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))) Φ
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
hom_bind₁

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
x : R
⊢ (Perfection.lift p R S) (π.comp f) = (↑m.equiv).comp f

Tactic:
rw [← Equiv.eq_symm_apply]

Goal state after:
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
x : R
⊢ π.comp f = (Perfection.lift p R S).symm ((↑m.equiv).comp f)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    C ↑p ^ x * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) =
      C ↑p ^ x * X x ^ p ^ (n - x)

Tactic:
refine fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)

Goal state after:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
⊢ (if P m then X m else 0) ^ p ^ (n - m) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ (teichmullerFun p 1).coeff (n✝ + 1) = coeff 1 (n✝ + 1)

Tactic:
· rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]; rfl

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

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

Tactic:
by
  ext1; rw [RingHom.comp_apply, truncate_lift]

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h : ∀ (n : ℕ), (Ideal.Quotient.mk 𝔭) (x.coeff n) = 0
⊢ (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (𝔭 ^ (n + 1))) (((Pi.evalRingHom (fun a ↦ R) n).comp ghostMap) x)) =
    (quotEquivOfEq ⋯) 0

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, Pi.evalRingHom_apply, ghostMap_apply,
    quotEquivOfEq_mk, map_zero]

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h : ∀ (n : ℕ), (Ideal.Quotient.mk 𝔭) (x.coeff n) = 0
⊢ (Ideal.Quotient.mk (span {↑p ^ (n + 1)})) ((ghostComponent n) x) = 0
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.ker (map (Ideal.Quotient.mk 𝔭)) ≤ RingHom.ker ((Ideal.Quotient.mk (𝔭 ^ (n + 1))).comp (ghostComponent n))

Tactic:
by
  intro x
  simp only [RingHom.mem_ker, map_eq_zero_iff, RingHom.comp_apply]
  intro h
  simp only [ghostComponent]
  apply_fun Ideal.quotEquivOfEq (Ideal.span_singleton_pow _ (n + 1))
  simp only [RingHom.coe_comp, Function.comp_apply, Pi.evalRingHom_apply, ghostMap_apply,
    quotEquivOfEq_mk, map_zero]
  simp only [eq_zero_iff_dvd] at h ⊢
  exact pow_dvd_ghostComponent_of_dvd_coeff (fun _ _ ↦ h _)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ dickson 2 1 (n + 2) = Chebyshev.S R ↑(n + 2)

Tactic:
by
    rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.S_add_two,
      dickson_two_one_eq_chebyshev_S (n + 1), dickson_two_one_eq_chebyshev_S n]
    push_cast
    ring

Goal state after: