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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ lift.{0, u_1} (SummableFamily.powers x).hsum.cardSupp ≤ sum fun n ↦ x.cardSupp ^ n

Tactic:
cardSupp_hsum_le,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (sum fun a ↦ ((SummableFamily.powers x) a).cardSupp) ≤ sum fun n ↦ x.cardSupp ^ n
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]
⊢ f.Monic →
    ∀ (a₀ : R),
      Polynomial.eval a₀ f ∈ I →
        IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
_

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),
    Polynomial.eval a₀ f ∈ I →
      IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ IsArtinianRing (Localization.AtPrime q)

Tactic:
isArtinianRing_iff_isNilpotent_maximalIdeal,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
⊢ IsNilpotent (IsLocalRing.maximalIdeal (Localization.AtPrime q))
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
I : Ideal R
hIn : I ≠ ⊥
⊢ I.IsPrime → ∃ x ∈ I, Prime x

Tactic:
_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
I : Ideal R
hIn : I ≠ ⊥
a✝ : I.IsPrime
⊢ ∃ x ∈ I, Prime x
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 : (under R (IsLocalRing.maximalIdeal (Localization.AtPrime p))).height ≤ 1
⊢ p.height ≤ 1

Tactic:
Localization.AtPrime.under_maximalIdeal

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 : p.height ≤ 1
⊢ p.height ≤ 1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_1
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)
⊢ under R (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ∈ I.minimalPrimes

Tactic:
Localization.AtPrime.under_maximalIdeal

Goal state after:
case refine_1
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)
⊢ p ∈ I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ ∃ y ∈ I, x = x * y

Tactic:
suffices h : x ∈ I * Ideal.span {x} by
    rw [Ideal.mem_mul_span_singleton] at h
    grind

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ I * span {x}
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
⊢ IsOpen s → IsOpen ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
_

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen ((fun a ↦ ↑a) ⁻¹' s)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
h : P.height ≤ ↑t.card
⊢ t.card ≤ s.card + s'.card

Tactic:
refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
h : P.height ≤ ↑t.card
⊢ o.card ≤ s'.card
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
n : ℕ
S : Submonoid R
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M n
⊢ HasProjectiveDimensionLE (M.localizedModule S) n

Tactic:
by
  have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
  induction n generalizing M with
  | zero =>
    have projle : HasProjectiveDimensionLE M 0 := ‹_›
    simp only [HasProjectiveDimensionLE, zero_add] at projle ⊢
    rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at projle ⊢
    exact Module.projective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)
  | succ n ih =>
    rcases ModuleCat.enoughProjectives.1 M with ⟨⟨P, f⟩⟩
    let T := ShortComplex.mk (kernel.ι f) f (kernel.condition f)
    have T_exact : T.ShortExact := { exact := ShortComplex.exact_kernel f }
    let TS := T.map (ModuleCat.localizedModuleFunctor S)
    have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
    have : Projective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).projective_obj _
    have := (T_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mp ‹_›
    exact (TS_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mpr (ih (kernel f))

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : (ResidueField R)[(residue S) β] = ⊤
s : S
⊢ s ∈ ⊤ → s ∈ Subalgebra.toSubmodule R[β] ⊔ maximalIdeal R • ⊤

Tactic:
_

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : (ResidueField R)[(residue S) β] = ⊤
s : S
a✝ : s ∈ ⊤
⊢ s ∈ Subalgebra.toSubmodule R[β] ⊔ maximalIdeal R • ⊤
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h : x < order f - ↑k
⊢ Ring.choose (x + ↑k) k • f.coeff (x + ↑k) = 0

Tactic:
coeff_eq_zero_of_lt_order <| lt_sub_iff_add_lt.mp h,

Goal state after:
R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h : x < order f - ↑k
⊢ Ring.choose (x + ↑k) k • 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
⊢ ∑ i, X i * (pderiv i) φ = ∑ i, 1 i • (X i * (pderiv i) φ)

Tactic:
Pi.one_apply,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
⊢ ∑ i, X i * (pderiv i) φ = ∑ x, 1 • (X x * (pderiv x) φ)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case right
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
i : ℤ
⊢ i ∈ Set.Icc ℓ N → φ i ∈ ℱ

Tactic:
_

Goal state after:
case right
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
i : ℤ
a✝ : i ∈ Set.Icc ℓ N
⊢ φ i ∈ ℱ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
t : Fin n →₀ ℕ
hnm : n ≤ m
⊢ leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) t r) = r

Tactic:
by
  induction t using Finsupp.induction₂ with
  | zero => rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
  | add_single i _ _ _ _ ih =>
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]
    exacts [toLex.injective, toLex_add]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
by
  rw [denseRange_iff_closure_range]
  ext f
  simp only [UniformSpace.mem_closure_iff_symm_ball, Set.mem_univ, iff_true, Set.Nonempty,
    Set.mem_inter_iff, Set.mem_range, exists_exists_eq_and]
  intro V hV h_symm
  rw [uniformity_eq_comap_neg_add_nhds_zero_swapped] at hV
  obtain ⟨T, hT₀, hT₁⟩ := hV
  obtain ⟨γ, hγ⟩ := Valued.mem_nhds_zero.mp hT₀
  have := (embedding γ.1)
  obtain ⟨P, hP⟩ := exists_ratFunc_val_lt f
    <| γ.map (embedding (f := .ofClass (valued K).v))
  use P
  apply hT₁
  apply hγ
  simpa only [Units.coe_map, MonoidHom.coe_mk, ZeroHom.toFun_eq_coe, OneHom.coe_mk, add_comm,
    MonoidWithZeroHom.toZeroHom_coe, ← sub_eq_add_neg, Set.mem_ofPred_eq,
    Valuation.restrict_lt_iff_lt_embedding]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
Filter.comap

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    uniformity K⟮X⟯
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
⊢ ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t

Tactic:
simp at h2

Goal state after:
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) *
        (∑ 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) -
      (-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
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
simp only [left_distrib, add_sub_cancel_left] at sub_both_sides

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
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ antidiagonal k with x.1 < k ∧ 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
n m : σ →₀ ℕ
h : n ≤ m
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
⊢ (MvPolynomial.expand p) ((trunc' R n) f) = (MvPolynomial.expand p) ((trunc' R n) ↑((trunc' R m) f))

Tactic:
← trunc'_trunc' h

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
n m : σ →₀ ℕ
h : n ≤ m
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
⊢ (MvPolynomial.expand p) ((trunc' R n) ↑((trunc' R m) f)) = (MvPolynomial.expand p) ((trunc' R n) ↑((trunc' R m) f))
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  ↑((MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (map (frobenius R p)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))
⊢ (MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R n) f)) =
    (trunc' R (p • n)) ↑((trunc' R (p • n)) f ^ p)

Tactic:
← MvPolynomial.map_frobenius_expand,

Goal state after:
case h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  ↑((MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (map (frobenius R p)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))
⊢ (MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R n) f)) =
    (trunc' R (p • n)) ↑((MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R (p • n)) f)))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
xInTermsOfW,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i, C (↑p ^ ↑i) * xInTermsOfW p R ↑i ^ p ^ (n - ↑i)) * C (⅟↑p ^ n) =
    (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n)
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 ((↑g.symm).comp ↑g) (Ideal.map (T f) I) = Ideal.map (↑g.symm) (Ideal.map g (Ideal.map (T f) I))

Tactic:
simp [← Ideal.map_map, Ideal.map_coe]

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

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

Tactic:
simp only [smul_zero, map_nsmul, constantCoeff_X]

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✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : (bind₁ (W_ R)) (xInTermsOfW p R n) = X n
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x.ghostFun).coeff n = x.coeff n

Tactic:
apply_fun aeval x.coeff at this

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : (aeval x.coeff) ((bind₁ (W_ R)) (xInTermsOfW p R n)) = (aeval x.coeff) (X n)
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x.ghostFun).coeff n = x.coeff n
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case refine_3
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
_

Goal state after:
case refine_3
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case refine_3
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
_

Goal state after:
case refine_3
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (n : ℕ), (ghostComponent n) (x✝ + y✝).verschiebungFun = (ghostComponent n) (x✝.verschiebungFun + y✝.verschiebungFun)
Module: Mathlib.RingTheory.WittVector.Identities

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

Tactic:
one_coeff_eq_of_pos

Goal state after:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
j : ℕ
hj : j ≠ 0
⊢ 0 = 0

case zero.hn
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
j : ℕ
hj : j ≠ 0
⊢ 0 < j
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
_

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
_

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (n : ℕ), (ghostComponent n) (x✝ * y✝).frobeniusFun = (ghostComponent n) (x✝.frobeniusFun * y✝.frobeniusFun)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
_

Goal state after:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (n : ℕ), (ghostComponent n) (x✝ + y✝).frobeniusFun = (ghostComponent n) (x✝.frobeniusFun + y✝.frobeniusFun)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: 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 : ℕ
this :
  (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i ↦ ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i ↦ ¬P i) x) = (ghostComponent n) x

Tactic:
apply_fun aeval x.coeff at this

Goal state after:
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 : ℕ
this :
  (aeval x.coeff)
      ((bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i ↦ ¬P i)) (wittPolynomial p ℤ n)) =
    (aeval x.coeff) (wittPolynomial p ℤ n)
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i ↦ ¬P i) x) = (ghostComponent n) x
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n i : ℕ
⊢ i ∈ Finset.range (n + 1) → i ≠ 0 → ↑p ^ i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0

Tactic:
_

Goal state after:
case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n i : ℕ
a✝ : i ∈ Finset.range (n + 1)
⊢ i ≠ 0 → ↑p ^ i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0