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

Goal state before:
pp: case intro
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
key : q - 1 + ∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card = q ^ n - 1
Φₙ : ℤ[X] := cyclotomic n ℤ
⊢ False

Tactic:
apply_fun (Nat.cast : ℕ → ℤ) at key

Goal state after:
case intro
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)
⊢ False
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
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
⊢ 0 ∈ {x | a ^ n • x ∈ N}

Tactic:
by simp

Goal state after:
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 : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ N ≤ N + a ^ n • ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
⊢ Subring.center D = ⊤

Tactic:
cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (f { asIdeal := P, isMaximal := hP }.asIdeal) (frac { asIdeal := P, isMaximal := hP } ↑x).1 ∈
    Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P)))

Tactic:
exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩

Goal state after:
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
k : ℕ
n : ℤ
x : V
m : ℤ
⊢ ((hasseDeriv R k) ((single (n + ↑k)) x)).coeff m = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m

Tactic:
dsimp only [hasseDeriv_coeff]

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
n : ℤ
x : V
m : ℤ
⊢ Ring.choose (m + ↑k) k • ((single (n + ↑k)) x).coeff (m + ↑k) = ((single n) (Ring.choose (n + ↑k) k • x)).coeff m
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
ha : ¬IsUnit (1, 0)
hb : ¬IsUnit (0, 1)
⊢ (1, 0) + (0, 1) = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
k : ℕ
ih : ∀ (f : V⸨X⸩), ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
f : V⸨X⸩
⊢ ((⇑(derivative R))^[k + 1] f).coeff n = ((k + 1).factorial • (hasseDeriv R (k + 1)) f).coeff n

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x ≠ 0 → x.powerSeriesPart ≠ 0

Tactic:
simp only [ne_eq]

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ ¬x = 0 → ¬x.powerSeriesPart = 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
n✝ : ℤ
n : ℕ
⊢ (single ↑(n + ↑1)) 1 = (single 1) 1⁻¹ ^ (n + ↑1)

Tactic:
single_one_eq_pow,

Goal state after:
F : Type u
inst✝ : Field F
n✝ : ℤ
n : ℕ
⊢ (single 1) 1 ^ (n + ↑1) = (single 1) 1⁻¹ ^ (n + ↑1)
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
s : S
hs : s ∈ ker g
⊢ ⟨(0, s), ⋯⟩ ∈ ker (f.pullbackFst g)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ ↑q.den ∈ nonZeroDivisors ℤ

Tactic:
by simp

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

Goal state before:
pp: case refine_3
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})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, (w x • (X x * (pderiv x) p) + w x • (X x * (pderiv x) q)) = n • p + n • q

Tactic:
sum_add_distrib,

Goal state after:
case refine_3
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})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, w x • (X x * (pderiv x) p) + ∑ x, w x • (X x * (pderiv x) q) = n • p + n • q
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)
⊢ embedding ↑γ ≠ 0

Tactic:
by simp

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ i ∉ c.support → coeff (Finsupp.single i 1) (c i • X i) = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ IsUniformInducing ⇑(algebraMap K⟮X⟯ K⸨X⸩)

Tactic:
isUniformInducing_iff,

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ Filter.comap (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) (uniformity K⸨X⸩) = uniformity K⟮X⟯
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries σ R
⊢ (expand 1 ⋯) f = f

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
S : Type u_4
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
i : MvPowerSeries σ S
⊢ ((expand p hp).comp (substAlgHom hf)) i = (substAlgHom ⋯) i

Tactic:
simp [expand, subst_comp_subst_apply hf (HasSubst.X_pow hp)]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
⊢ (substAlgHom ⋯) φ = subst (fun i ↦ (expand p hp) (f i)) φ

Tactic:
substAlgHom_apply

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
⊢ subst (fun i ↦ (expand p hp) (f i)) φ = subst (fun i ↦ (expand p hp) (f i)) φ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
⊢ ∑ a ∈ antidiagonal (Fintype.card σ), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 = 0

Tactic:
by
  let k := Fintype.card σ
  suffices (-1 : MvPolynomial σ R) ^ (k + 1) *
      ∑ a ∈ antidiagonal k, (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd = 0 by
    simpa using this
  simp [k, ← sum_filter_add_sum_filter_not (antidiagonal k) (fun a ↦ a.fst < k),
    ← mul_esymm_eq_sum, mul_add, ← mul_assoc, ← pow_add, mul_comm ↑k (esymm σ R k)]

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 : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ * (coeff (p • m)) (d.prod fun s e ↦ (X s ^ p) ^ e) = (coeff m) φ

Tactic:
rw [finsum_eq_single _ m]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ (coeff m) φ * (coeff (p • m)) (m.prod fun s e ↦ (X s ^ p) ^ e) = (coeff m) φ

σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ ∀ (x : σ →₀ ℕ), x ≠ m → (coeff x) φ * (coeff (p • m)) (x.prod fun s e ↦ (X s ^ p) ^ e) = 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
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
⊢ 0 / p = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
x : M
⊢ (let __spread.0 := DistribSMul.toAddMonoidHom (ι → M) (single i i 1);
      { toFun := (↑__spread.0).toFun, map_add' := ⋯, map_smul' := ⋯ })
      (Function.const ι x) =
    Pi.single i x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
x✝ : ↥(toModuleCatObj R (ι → M) i)
x : ι → M
hx : x ∈ toModuleCatObj R (ι → M) i
y : ι → M
hy : single i i 1 • y = x
⊢ (fun x ↦ ⟨Pi.single i x, ⋯⟩) ((fun x ↦ ∑ i_1, ↑x i_1) ⟨x, hx⟩) = ⟨x, hx⟩

Tactic:
rw [single_smul] at hy

Goal state after:
R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
x✝ : ↥(toModuleCatObj R (ι → M) i)
x : ι → M
hx : x ∈ toModuleCatObj R (ι → M) i
y : ι → M
hy : Pi.single i (1 • y i) = x
⊢ (fun x ↦ ⟨Pi.single i x, ⋯⟩) ((fun x ↦ ∑ i_1, ↑x i_1) ⟨x, hx⟩) = ⟨x, hx⟩
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
x : M
⊢ (fun x ↦ ∑ i_1, ↑x i_1) ((fun x ↦ ⟨Pi.single i x, ⋯⟩) x) = x

Tactic:
by simp

Goal state after:
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 : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
⊢ i ∈ Finset.univ

Tactic:
by simp

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
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
⊢ 0 / p = 0

Tactic:
by simp

Goal state after:
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 : ι
⊢ i ∉ Finset.univ → single j i 1 • single i j 1 • ↑(v i) = 0

Tactic:
by simp

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
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
⊢ 0 / p = 0

Tactic:
by simp

Goal state after:
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₀
⊢ (ModuleCat.matrixEquivalence R i).functor.map (r • f) = r • (ModuleCat.matrixEquivalence R i).functor.map f

Tactic:
ext (v : ι → X)

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
⊢ (ModuleCat.Hom.hom ((ModuleCat.matrixEquivalence R i).functor.map (r • f))) v =
    (ModuleCat.Hom.hom (r • (ModuleCat.matrixEquivalence R i).functor.map f)) v
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
let e (p : Ideal k) [p.IsPrime] : AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
    have := p.algEquivResidueFieldOfField.isAlgebraic
    IsAlgClosure.equiv k _ _

Goal state after:
k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
e : (p : Ideal k) → [inst : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun p [p.IsPrime] ↦
    have this := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
this :
  ∀ {C : M → ℝ},
    (∀ (a b : M), C (a + b) = C a * C b) →
      Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0) →
        Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0) →
          0 ≤ C → Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
hC' : ¬0 ≤ C
x✝ : M
⊢ 0 x✝ ≤ |C| x✝

Tactic:
by simp

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
x : M
⊢ 0 ≤ ‖∑ p ∈ antidiagonal x, f p.1 * g p.2‖

Tactic:
by simp

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 w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
wlt : ∀ (i : Fin (n + 1)), w i < up
ne : v ≠ w
h : ∑ x, r x * v x = ∑ x, r x * w x
⊢ (ofFn ⇑v).length = (ofFn ⇑w).length

Tactic:
by simp

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) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ Polynomial.X ^ v 0 ≠ 0

Tactic:
by simp

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

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

Tactic:
constantCoeff_X,

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

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

Tactic:
zero_pow,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 = 0

case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ p ^ (n - m) ≠ 0
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✝ : ℕ
⊢ (Ideal.Quotient.mk I) 1 = (coeff (R ⧸ I) p x✝) 1 ∧ 1 ^ p ^ x✝ ≡ 1 [SMOD I ^ (x✝ + 1)]

Tactic:
by simp

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
n : ℕ
⊢ (Ideal.Quotient.mk I) (Quotient.out ((coeff (R ⧸ I) p n) x) * Quotient.out ((coeff (R ⧸ I) p n) y)) =
    (coeff (R ⧸ I) p n) (x * y)

Tactic:
by simp

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 : Perfection R p
n : ℕ
⊢ (Ideal.Quotient.mk I) ((coeffMonoidHom R p n) x) = (coeff (R ⧸ I) p n) ((mapMonoidHom p ↑(Ideal.Quotient.mk I)) x) ∧
    (coeffMonoidHom R p n) x ^ p ^ n ≡ (coeffMonoidHom R p 0) x [SMOD I ^ (n + 1)]

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittMul p 0 = X (0, 0) * X (1, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittMul, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
    map_mul, bind₁_X_right, map_wittStructureInt]

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

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

Tactic:
xInTermsOfW_aux

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Fact (Nat.Prime p)
⊢ coeff 1 0 = 1

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Fact (Nat.Prime p)
⊢ coeff 0 0 = 0

Tactic:
by simp

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

Goal state before:
pp: 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 + 1 - k) = p * p ^ (n - k)

Tactic:
← pow_succ',

Goal state after:
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 + 1 - k) = p ^ (n - k + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p (m + Nat.zero)) (f ^ p ^ Nat.zero) = (coeffMonoidHom M p m) f

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n

Tactic:
induction n using Nat.strong_induction_on with | h n IH => ?_
  rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]
  intro c
  rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one]
  have sum_induction_steps :
      map (Int.castRingHom ℚ)
        (∑ i ∈ range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
      ∑ i ∈ range n,
        C ((p : ℚ) ^ i) * wittStructureRat p (map (Int.castRingHom ℚ) Φ) i ^ p ^ (n - i) := by
    rw [map_sum]
    apply Finset.sum_congr rfl
    intro i hi
    rw [Finset.mem_range] at hi
    simp only [IH i hi, map_mul, map_pow, map_C]
    rfl
  simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ←
    map_bind₁, ← map_sub, coeff_map]
  rw [show (p : ℚ) ^ n = ((↑(p ^ n) : ℤ) : ℚ) by norm_cast]
  rw [← Rat.den_eq_one_iff, eq_intCast, Rat.den_div_intCast_eq_one_iff]
  swap; · exact mod_cast pow_ne_zero n hp.1.ne_zero
  revert c; rw [← C_dvd_iff_dvd_coeff]
  exact C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum Φ n IH

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly p f
⊢ IsPoly p fun R _Rcr ↦ g ∘ f

Tactic:
by
  obtain ⟨φ, hf⟩ := hf
  obtain ⟨ψ, hg⟩ := hg
  use fun n => bind₁ φ (ψ n)
  intros
  simp only [aeval_bind₁, Function.comp, hg, hf]

Goal state after: