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

Goal state before:
pp: case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R

Tactic:
rw [IH (Fintype.card R) _ R inferInstance rfl]

Goal state after:
case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ ⊤

n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card ↥R < n
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h✝ : f n = N ∨ a ^ n • ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
⊢ b ∈ f n

Tactic:
hn

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
h✝ : f n = N ∨ a ^ n • ⊤ ≤ N
h : f n = N
hn : f n = f (n + 1)
⊢ b ∈ f (n + 1)
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
m₁ m₂ : Ideal R
left✝¹ : m₁.IsMaximal
left✝ : m₂.IsMaximal
hm₁m₂ : m₁ ≠ m₂
e : R ⧸ m₁ ⊓ m₂ ≃+* (R ⧸ m₁) × R ⧸ m₂ := m₁.quotientInfEquivQuotientProd m₂ ⋯
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f

Tactic:
let f := e.toRingHom.comp <| Ideal.Quotient.mk (m₁ ⊓ m₂)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
m₁ m₂ : Ideal R
left✝¹ : m₁.IsMaximal
left✝ : m₂.IsMaximal
hm₁m₂ : m₁ ≠ m₂
e : R ⧸ m₁ ⊓ m₂ ≃+* (R ⧸ m₁) × R ⧸ m₂ := m₁.quotientInfEquivQuotientProd m₂ ⋯
f : R →+* (R ⧸ m₁) × R ⧸ m₂ := e.toRingHom.comp (Ideal.Quotient.mk (m₁ ⊓ m₂))
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⟦X⟧
n : ℕ
⊢ ((ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff n) x

Tactic:
by
  rw [ofPowerSeries_apply_coeff]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
rw [← Polynomial.coe_X, ← intValuation_eq_of_coe]
  exact intValuation_singleton _ Polynomial.X_ne_zero (idealX_span _)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((single (-(↑s + 1))) 1) = exp (- -(↑s + 1))

Tactic:
← inv_inj,

Goal state after:
case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ (Valued.v ((single (-(↑s + 1))) 1))⁻¹ = (exp (- -(↑s + 1)))⁻¹
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
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
⊢ n < d → (PowerSeries.coeff n) F = 0

Tactic:
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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
n : ℕ
⊢ n < d → (PowerSeries.coeff n) F = 0

Tactic:
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
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
⊢ f.coeff (↑s + ↑n) = 0

Tactic:
apply h_val_f (s + n)

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⟧ := ⋯
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
⊢ ↑s + ↑n < D
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ ∃ N, ∀ n < N, coeff hℱ n = 0

Tactic:
by
  let _ : UniformSpace K := ⊥
  obtain ⟨N, hN⟩ := exists_lb_eventual_support hℱ
  refine ⟨N, fun n hn ↦ Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
      ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩
  simp only [pure_zero, nonpos_iff]
  apply Filter.mem_of_superset hN (fun _ ha ↦ ha _ hn)

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

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

Tactic:
rw [and_comm, ne_comm, ← Fin.val_ne_iff]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
· simp only [Set.mem_Iio, inter_mem_iff]
    constructor
    · have := (exists_lb_coeff_ne hℱ).choose_spec
      rw [Filter.eventually_iff] at this
      convert! this
      ext
      simp only [Set.mem_iInter, Set.mem_ofPred_eq]; rfl
    · rw [biInter_mem (Set.finite_Icc ℓ N)]
      intro i _
      apply (coeff_tendsto hℱ _).eventually
      simp

Goal state after:
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 : ℤ := -((embedding ↑γ).log - 1)
hD₀ : D = -((embedding ↑γ).log - 1)
⊢ -D < (embedding ↑γ).log

Tactic:
hD₀

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)
⊢ - -((embedding ↑γ).log - 1) < (embedding ↑γ).log
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 : ℤ := -((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 : ℤ
⊢ n < D → (x✝ - limit hℱ).coeff n = 0

Tactic:
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.LaurentSeries

Goal state before:
pp: case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
x : adicCompletion K⟮X⟯ (idealX K)
hx : Valued.v x = γ
⊢ ∃ γ_1, {x | Valued.v.restrict x < ↑γ_1} ⊆ {t | Valued.v t < γ}

Tactic:
use Units.mk0 (Valued.v.restrict x) (by
        simp only [Valuation.restrict_def, ne_eq, map_eq_zero]
        intro h
        simp only [h, map_zero] at hx
        tauto)

Goal state after:
case h
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
x : adicCompletion K⟮X⟯ (idealX K)
hx : Valued.v x = γ
⊢ {x_1 | Valued.v.restrict x_1 < ↑(Units.mk0 (Valued.v.restrict x) ⋯)} ⊆ {t | Valued.v t < γ}
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
i✝ : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → ↑X
i : ι
⊢ (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f)) v i =
    (r • (LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f)) v) i

Tactic:
simp only [LinearMap.mapMatrixModule_apply, LinearMap.compLeft_apply, Function.comp_apply,
      LinearMap.smul_apply]

Goal state after:
R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
i✝ : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → ↑X
i : ι
⊢ r • (ModuleCat.Hom.hom f) (v i) = (r • (LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f)) v) i
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : 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
i : σ
hi : m i > n i
this : ¬p • m i ≤ p • n i
⊢ ¬p • m ≤ p • n

Tactic:
exact Not.intro fun a ↦ this (a i)

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 : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
hd : d ≤ p • n
⊢ (if d ≤ p • n then (coeff d) ((expand p hp) φ) else 0) = 0

Tactic:
if_pos hd,

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 : σ →₀ ℕ
i : σ
hi : ¬p ∣ d i
hd : d ≤ p • n
⊢ (coeff d) ((expand p hp) φ) = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f

Tactic:
rw [← valuation_LaurentSeries_equal_extension, ← compare_comp_eq_compare ratfuncAdicComplPkg _]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) =
    (⋯.extend ⇑Valued.v ∘ (LaurentSeriesPkg K).compare ratfuncAdicComplPkg) f

case cont_f
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Continuous ⇑Valued.v

case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ ∀ (a : ratfuncAdicComplPkg.space),
    Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 a)) (𝓝 (⋯.extend (⇑Valued.v) a))
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) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
ne : v ≠ w
⊢ ∑ x, r x * v x ≠ ∑ x, r x * w x

Tactic:
by
  intro h
  refine ne <| Finsupp.ext <| congrFun <| ofFn_inj.mp ?_
  apply ofDigits_inj_of_len_eq (Nat.lt_add_right f.totalDegree one_lt_two)
    (by simp) (lt_up vlt) (lt_up wlt)
  simpa only [ofDigits_eq_sum_mapIdx, mapIdx_eq_ofFn, get_ofFn, length_ofFn,
    Fin.val_cast, mul_comm, sum_ofFn] using! h

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

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

Tactic:
sum_congr rfl

Goal state after:
p n : ℕ
⊢ (range (n + 1)).sum ?m.99 = ∑ x ∈ range (n + 1), (expand p) (C (↑p ^ x) * X x ^ p ^ (n - x))

p n : ℕ
⊢ ∀ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = ?m.99 x

p n : ℕ
⊢ ℕ → MvPolynomial ℕ (ZMod (p ^ (n + 1)))
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) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this : g.symm.toRingEquiv.toRingHom.comp ↑g = RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I = Ideal.map ((RingHom.id (MvPolynomial (Fin (n + 1)) k)).comp ↑(T f)) I

Tactic:
rw [id_comp, Ideal.map_coe]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ((bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (X n) -
        ∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      C (⅟↑p ^ n)

Tactic:
rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ,
    sum_range_succ, tsub_self, add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul,
    add_mul, mul_right_comm, mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ',
    mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1, one_mul, add_comm _ (X n ^ p), add_assoc,
    ← add_sub, add_right_inj, frobeniusPolyAux_eq, map_sub, map_X, mul_sub, sub_eq_add_neg,
    add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub,
    add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n) -
      (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) =
    C ↑p *
      (MvPolynomial.map (Int.castRingHom ℚ))
        (∑ i ∈ range n,
          ∑ j ∈ range (p ^ (n - i)),
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))))
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
let P : ℕ → Prop := fun n => y.coeff n = 0
  have : DecidablePred P := Classical.decPred P
  set z := mk p fun n => if P n then x.coeff n else y.coeff n
  have hx : select P z = x := by
    ext1 n; rw [select, coeff_mk, coeff_mk]
    split_ifs with hn
    · rfl
    · rw [(h n).resolve_right hn]
  have hy : select (fun i => ¬P i) z = y := by
    ext1 n; rw [select, coeff_mk, coeff_mk]
    split_ifs with hn
    · exact hn.symm
    · rfl
  calc
    (x + y).coeff n = z.coeff n := by rw [← hx, ← hy, select_add_select_not P z]
    _ = x.coeff n + y.coeff n := by
      simp only [z, mk.eq_1]
      split_ifs with y0
      · rw [y0, add_zero]
      · rw [h n |>.resolve_right y0, zero_add]

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
⊢ (fontaineTheta R p) ((teichmuller p) x) = untilt x

Tactic:
IsHausdorff.eq_iff_smodEq (I := 𝔭)

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
⊢ ∀ (n : ℕ), (fontaineTheta R p) ((teichmuller p) x) ≡ untilt x [SMOD 𝔭 ^ n • ⊤]
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
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ x.coeff i = ∑ s ≤ n, ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ s) (x.coeff s)) * ↑p ^ s).coeff i

pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ ∀ (n_1 : ℕ),
    Subsingleton
      ↑{r |
          r ∈ Finset.Iic n ∧
            ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n_1 ≠ 0}

Tactic:
· rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))]
    let g := fun x : ℕ ↦ (0 : R)
    rw [Finset.sum_congr rfl (g := g)]
    · simp [g]
    · intro b hb
      simp only [Finset.mem_sdiff, Finset.mem_Iic, Finset.mem_singleton] at hb
      exact teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ ∀ (n_1 : ℕ),
    Subsingleton
      ↑{r |
          r ∈ Finset.Iic n ∧
            ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n_1 ≠ 0}
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ dickson 1 1 0 = Chebyshev.C R ↑0

Tactic:
simp only [dickson_zero]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑1 = Chebyshev.C R ↑0
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 1 0 = Chebyshev.S R ↑0

Tactic:
simp only [dickson_zero]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = Chebyshev.S R ↑0
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 1 p = X ^ p

Tactic:
apply map_injective (ZMod.castHom (dvd_refl p) K) (RingHom.injective _)

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ map (ZMod.castHom ⋯ K) (dickson 1 1 p) = map (ZMod.castHom ⋯ K) (X ^ p)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝ : Field F
d : ℕ
⊢ hilbertPoly 0 d = 0

Tactic:
by
  delta hilbertPoly; induction d with
  | zero => simp only
  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
⊢ n > (p * (1 - X)).natDegree →
    (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
hn

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) = ↑n ! * C ((-1) ^ x * ↑(n.choose x) * ↑((n + x).choose n))

Tactic:
rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]

Goal state after:
case a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ C ((-1) ^ x * ↑(n.choose x)) * ↑((n + x)! / x !) = C ((-1) ^ x * ↑(n.choose x)) * (C ↑((n + x).choose n) * ↑n !)
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝ : Field R
a b c x1 x2 : R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2} ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a

Tactic:
rw [roots_quadratic_eq_pair_iff_of_ne_zero ha]

Goal state after:
R : Type u_1
inst✝ : Field R
a b c x1 x2 : R
ha : a ≠ 0
⊢ b = -a * (x1 + x2) ∧ c = a * x1 * x2 ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h.left
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor N (Subalgebra.inclusion hAB).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0

Tactic:
hu'

Goal state after:
case h.left
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst✝ : IsAdicComplete ⊤ A
this : Subsingleton A
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤

Tactic:
Subsingleton.elim f 0,

Goal state after:
case inl
A : Type u_1
inst✝¹ : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst✝ : IsAdicComplete ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g (H.div 0) (H.mod 0) ⊤