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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← map_subst
      (HasSubst.cons_subst_zero_left (0 : Fin 3) 1 2 F.zero_constantCoeff),

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : (s a.1).coeff gh.1 ≠ 0 ∧ (t a.2).coeff gh.2 ≠ 0 ∧ gh.1 +ᵥ gh.2 = g
⊢ (∃ i, (s.toFun i).coeff gh.1 ≠ 0) ∧ (∃ i, (t.toFun i).coeff gh.2 ≠ 0) ∧ True

Tactic:
exact ⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
⊢ (PowerSeries.coeff n) (PowerSeries.mk (f * g).coeff) =
    (PowerSeries.coeff n) (PowerSeries.mk f.coeff * PowerSeries.mk g.coeff)

Tactic:
simp only [PowerSeries.coeff_mul, PowerSeries.coeff_mk, coeff_mul]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
⊢ ∑ ij ∈ Finset.antidiagonal ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 =
    ∑ x ∈ HasAntidiagonal.antidiagonal n, f.coeff x.1 * g.coeff x.2
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : g ∈ (f a).support
⊢ a ∈ f.support

Tactic:
Finsupp.mem_support_iff,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : g ∈ (f a).support
⊢ f a ≠ 0
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ (antipode R) (T n) = T (-n)

Tactic:
unfold T

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
n : ℤ
⊢ (antipode R) (AddMonoidAlgebra.single n 1) = AddMonoidAlgebra.single (-n) 1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m * 1]

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ c m ≡ c n [SMOD I ^ m]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n * 1]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n * 1]

Tactic:
mul_one

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n]
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 a → ∃ I ∈ F, a +ᵥ idealSet I ⊆ s

Tactic:
intro hs
    rcases ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.1 hs with ⟨t, ht, hts⟩
    rcases ht with ⟨I, hI, rfl⟩
    exact ⟨I, hI, hts⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this✝ : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : (IsLocalRing.maximalIdeal (Localization.AtPrime p)).height ≤ 1
⊢ p.height ≤ 1

Tactic:
← IsLocalization.height_under p.primeCompl,

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this✝ : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : (under R (IsLocalRing.maximalIdeal (Localization.AtPrime p))).height ≤ 1
⊢ p.height ≤ 1
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂

Tactic:
let e := IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.1) p₂.1
  have hm : closedPoint (Localization.AtPrime p₂.1) =
    e.symm ⟨p₂, le_refl p₂⟩ := (PrimeSpectrum.ext Localization.AtPrime.map_eq_maximalIdeal).symm
  obtain ⟨q, hxq, h₀, h₁⟩ :=
    @exist_mem_one_of_mem_maximal_ideal (Localization.AtPrime p₂.1) _ _ _
      (e.symm ⟨p₁, h₁.le⟩) (e.symm ⟨p₀, (h₀.trans h₁).le⟩) (e.symm.lt_iff_lt.mpr h₀)
        (by simp [hm, h₁]) (algebraMap R (Localization.AtPrime p₂.1) x) <| by
          rw [← Localization.AtPrime.map_eq_maximalIdeal]
          exact mem_map_of_mem (algebraMap R (Localization.AtPrime p₂.1)) hx
  rw [← e.symm_apply_apply q] at h₀ h₁ hxq
  have hq : (e q).1 < p₂ := by
    have h : e.symm (e q) < e.symm ⟨p₂, le_refl p₂⟩ :=
      h₁.trans_eq Localization.AtPrime.map_eq_maximalIdeal.symm
    rwa [OrderIso.lt_iff_lt, Subtype.mk_lt_mk] at h
  exact Exists.intro (e q).1
    ⟨(p₂.1.under_map_of_isLocalizationAtPrime hq.le).le hxq, e.symm.lt_iff_lt.mp h₀, hq⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = 0
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧ 0 = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
use RelSeries.singleton _ p.last

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = 0
⊢ x ∈ ((RelSeries.singleton {(a, b) | a < b} (RelSeries.last p)).toFun 1).asIdeal ∧
    0 = (RelSeries.singleton {(a, b) | a < b} (RelSeries.last p)).length ∧
      RelSeries.head p = (RelSeries.singleton {(a, b) | a < b} (RelSeries.last p)).head ∧
        RelSeries.last p = (RelSeries.singleton {(a, b) | a < b} (RelSeries.last p)).last
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
⊢ Projective M ↔ ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)

Tactic:
refine ⟨fun h p ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case zero.refine_1
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : Projective M
p : MaximalSpectrum R
⊢ Projective (M.localizedModule p.asIdeal.primeCompl)

case zero.refine_2
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
⊢ Projective M
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:
by
  exact rfl

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
p q : F[X]
⊢ (algebraMap F⟮X⟯ F⸨X⸩) ((algebraMap F[X] F⟮X⟯) p / (algebraMap F[X] F⟮X⟯) q) =
    (algebraMap F[X] F⸨X⸩) p / (algebraMap F[X] F⸨X⸩) q

Tactic:
by
  simp only [map_div₀, IsScalarTower.algebraMap_apply F[X] (RatFunc F) F⸨X⸩]

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

Goal state before:
pp: case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ.IsHomogeneous 0
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)

Tactic:
rw [← totalDegree_zero_iff_isHomogeneous, totalDegree_eq_zero_iff_eq_C] at h
    rw [h, pderiv_C]; apply isHomogeneous_zero

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
this : (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

Tactic:
by
    exact ℱ.sets_of_superset this <| intersec₂.trans intersec₁

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
t s : Fin n →₀ ℕ
⊢ (aeval fun i ↦ esymm σ R (↑i + 1)) ((monomial (t + s)) r) =
    (aeval fun i ↦ esymm σ R (↑i + 1)) ((monomial (t + s)) (r * 1))

Tactic:
mul_one

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ pairs σ k with #t.1 < k, f t = ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
filter_pairs_lt,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ, f t =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

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

Tactic:
rw [disjoint_filter]

Goal state after:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ ∀ x ∈ pairs σ k, #x.1 < k → ¬#x.1 = k
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case mul_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R n) (X ⟨↑i, ⋯⟩) = (esymmAlgHom (Fin m) R m) (X i)

Tactic:
simp_rw [esymmAlgHom, aeval_X]

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
r : R
| C r * 1

Tactic:
mul_one

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| C r
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
⊢ (coeff m) φ * 1 = (coeff m) φ

Tactic:
mul_one

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 m) φ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a ∈ {a ∈ antidiagonal k | a.1 < k ∧ ¬0 < a.1} ↔ a ∈ {(0, k)}

Tactic:
mem_filter,

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a ∈ antidiagonal k ∧ a.1 < k ∧ ¬0 < a.1 ↔ a ∈ {(0, k)}
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) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ degreeOf 0 ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f))) ≠
    degreeOf 0 ((T f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))

Tactic:
by
  rw [degreeOf_zero_t _ _ <| mem_support_iff.mp hv, degreeOf_zero_t _ _ <| mem_support_iff.mp hw]
  refine sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne <;>
  exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

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 : ℕ
⊢ wittStructureRat p Φ n = wittStructureRat p Φ n * 1

pp: case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0

Tactic:
mul_one

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = wittStructureRat p Φ n

case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittOne p 0) = (map (Int.castRingHom ℚ)) 1

Tactic:
simp only [wittOne, wittStructureRat, xInTermsOfW_zero, map_one, bind₁_X_right,
    map_wittStructureInt]

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

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
⊢ i ≠ 0 → C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0

Tactic:
hi0

Goal state after:
case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * 1 =
    X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

Tactic:
mul_one

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * 1

Tactic:
mul_one

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (fun x ↦ ↑x)
      (coeff c
              ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
                ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) *
            1 /
          ↑p ^ n).num =
    coeff c
          ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
            ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) *
        1 /
      ↑p ^ n

Tactic:
mul_one

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (fun x ↦ ↑x)
      (coeff c
            ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n
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 + n)) f ^ p ^ n = (coeffMonoidHom M p m) f

Tactic:
by
  rw [← map_pow, coeffMonoidHom_pow_p_pow]

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
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ : ℕ
i : Fin 2
n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] (i, n).1 (i, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] (i, n).1 (i, n).2)

Tactic:
fin_cases i <;> simp [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp_def]

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

Goal state before:
pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
_hi : i ∈ Finset.range (n + 1)
⊢ i ≠ 0 → (bind₁ onePoly) (C (↑p ^ i) * X i ^ p ^ (n - i)) = 0

Tactic:
hi0

Goal state after:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ (bind₁ onePoly) (C (↑p ^ i) * X i ^ p ^ (n - i)) = 0
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))

Tactic:
← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s

Goal state after:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j : ℕ
hj : j ≠ i
⊢ (↑p ^ i).coeff j = 0

Tactic:
induction i generalizing j with
  | zero =>
    rw [pow_zero, one_coeff_eq_of_pos]
    exact Nat.pos_of_ne_zero hj
  | succ i hi =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP]
    cases j
    · rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]
    · rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_zero]

Goal state after: