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

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Tactic:
let f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
    HahnSeries.embDomainOrderAddMonoidHom
    (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm)

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = 1
⊢ (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) b = 1

Tactic:
← (Ideal.Quotient.mk _).map_one,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
a b : R
hb : (Ideal.Quotient.mk I) a * (Ideal.Quotient.mk I) b = (Ideal.Quotient.mk I) 1
⊢ (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) b = (Ideal.Quotient.mk ⊥.jacobson) 1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : (Ideal.Quotient.mk ⊥.jacobson) (a * y) = 1
h2 : (Ideal.Quotient.mk ⊥.jacobson) (y * a) = 1
⊢ IsUnit a

Tactic:
← (Ideal.Quotient.mk _).map_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : (Ideal.Quotient.mk ⊥.jacobson) (a * y) = (Ideal.Quotient.mk ⊥.jacobson) 1
h2 : (Ideal.Quotient.mk ⊥.jacobson) (y * a) = (Ideal.Quotient.mk ⊥.jacobson) 1
⊢ IsUnit a
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos.refine_2.zero
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
hn : 0 ∈ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}
⊢ 0 ∈ (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

pp: case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
n : ℕ
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}
⊢ n + 1 ∈ (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

Tactic:
· exact Set.mem_union_right _ (Set.mem_singleton 0)

Goal state after:
case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
n : ℕ
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}
⊢ n + 1 ∈ (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: case neg
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
hp : Submodule.IsPrincipal (map (algebraMap R S) p)
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
⊢ Submodule.IsPrincipal p

Tactic:
have hpb : map (algebraMap R S) p ≠ ⊥ := by simp [Ideal.map_eq_bot_iff_of_injective hi, hpbot]

Goal state after:
case neg
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
hp : Submodule.IsPrincipal (map (algebraMap R S) p)
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
⊢ Submodule.IsPrincipal p
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
⊢ supportDim R M ≠ ⊥

Tactic:
have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype
  simp [supportDim]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = Fin.last p.length

Tactic:
rw [Fin.last, hp, h0, zero_add]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = ⟨1, ⋯⟩
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ :
  ({I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf fun i ↦ (id i).colon Set.univ).radical =
    (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical

Tactic:
radical_finset_inf (i := I') (by simp [hI']) (by simp),

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : ((id I').colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⋯
f : M →ₗ[R] LocalizedModule S M := ⋯
hp : p ∈ s₀
x b : M
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
hb : (c * a) • x ∈ q
⊢ ↑(c * a) ∉ (q.colon Set.univ).radical

Tactic:
grind [Submonoid.mem_iInf, mem_primeCompl_iff]

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

Goal state before:
pp: 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 })
⊢ (frac { asIdeal := P, isMaximal := hP } ↑x).1 ∈
    ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))

Tactic:
by simpa using ⟨_, _, x.2, 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 : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

Tactic:
rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, smul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
⊢ (stabilizerHom Q P G) ⟨a, ⋯⟩ = σ

Tactic:
· ext x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    lift x to B' N.1.1 using fun g ↦ hN g.2
    change Ideal.Quotient.mk Q (QuotientGroup.mk (s := N) a • x).1 = _
    rw [this]
    exact DFunLike.congr_fun (s N).2 (Ideal.Quotient.mk _ x)

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

Goal state before:
pp: n m : ℕ
hnm : n ≤ m
⊢ Function.Injective ⇑(accumulate n m)

Tactic:
by
  refine fun t s he ↦ funext fun i ↦ ?_
  obtain h | h := lt_or_ge (i.1 + 1) m
  · have := accumulate_rec i.2 h s
    rwa [← he, accumulate_rec i.2 h t, add_right_cancel_iff] at this
  · have := h.antisymm (i.2.nat_succ_le.trans hnm)
    rw [← accumulate_last i.2 this t, ← accumulate_last i.2 this s, he]
    iterate 2 { intro j hj; exact ((j.2.trans_le hnm).not_ge hj).elim }

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
use RatFunc.X ^ f.order * (P : K⟮X⟯)

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := ⋯
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1))

Tactic:
exact monic_esymm this

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

Goal state before:
pp: case right
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
⊢ ∃ a, (esymmAlgHom (Fin n) R n) a = ⟨p, hp⟩

Tactic:
rw [← AlgHom.mem_range]

Goal state after:
case right
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = (esymmAlgHom (Fin m) R m) q

Tactic:
rw [← AlgHom.mem_range]

Goal state after:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ ⋯.extend ⇑Valued.v = ⇑Valued.v

Tactic:
apply IsDenseInducing.extend_unique

Goal state after:
case hf
K : Type u_2
inst✝ : Field K
⊢ ∀ (x : WithVal (polynomialValuationX K)), Valued.v ((LaurentSeriesPkg K).coe x) = Valued.v x

case hg
K : Type u_2
inst✝ : Field K
⊢ Continuous ⇑Valued.v
Module: Mathlib.RingTheory.MvPowerSeries.Expand

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

Tactic:
obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
          by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
        rw [← hm, coeff_expand_smul, coeff_of_lt_order]
        simp only [← hm, map_nsmul, smul_eq_mul, Nat.cast_mul, nsmul_eq_mul] at hd
        exact lt_of_mul_lt_mul_left' hd

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I := kerLiftAlg (hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)

Goal state after:
case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I := kerLiftAlg (hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0

Tactic:
induction n using Nat.strong_induction_on with | h n IH => ?_

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ n) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
sum_range_succ_comm,

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittNeg p 0) = (map (Int.castRingHom ℚ)) (-X (0, 0))

Tactic:
simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
    map_neg, bind₁_X_right, map_wittStructureInt]

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

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i) -
      ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) =
    X n * C (↑p ^ n)

Tactic:
sum_range_succ_comm,

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ C (↑p ^ n) * X n ^ p ^ (n - n) + ∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) -
      ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) =
    X n * C (↑p ^ n)
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 => ?_

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
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ ∃ a, (coeff R p n) a = x

Tactic:
refine ⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h✝ : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h : n ≤ m
⊢ R

case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ ∀ (n_1 : ℕ),
    (fun m ↦ if h : n ≤ m then ?refine_1 else x ^ p ^ (n - m)) (n_1 + 1) ^ p =
      (fun m ↦ if h : n ≤ m then ?refine_1 else x ^ p ^ (n - m)) n_1

case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ (coeff R p n) ⟨fun m ↦ if h : n ≤ m then ?refine_1 else x ^ p ^ (n - m), ?refine_2⟩ = x
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ (ghostComponent (n + 1)) x.verschiebungFun = ↑p * (ghostComponent n) x

Tactic:
simp only [ghostComponent_apply, aeval_wittPolynomial]
  rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl,
    zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, add_zero, Finset.mul_sum, Finset.sum_congr rfl]
  rintro i -
  simp only [pow_succ', verschiebungFun_coeff_succ, Nat.succ_sub_succ_eq_sub, mul_assoc]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            (C ↑p ^ (j + 1) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1)) *
        C ↑p ^ i *
      C ⅟↑p ^ n =
    C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))))

Tactic:
mul_comm (C (p : ℚ) ^ (j + 1)),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            ((MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) * C ↑p ^ (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1)) *
        C ↑p ^ i *
      C ⅟↑p ^ n =
    C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))))