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:
F.assoc,

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.HEval

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ n • x.orderTop ≤ ((powers x) n).orderTop

Tactic:
simp [h, orderTop_nsmul_le_orderTop_pow]

Goal state after:
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
G : Type u_3
inst✝ : Group G
a : G
b : A
⊢ ((LinearMap.mul' R A[G] ∘ₗ LinearMap.rTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a) b =
    ((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a) b

Tactic:
simpa [← (ℛ R b).eq] using congr(lsingle (R := R) (1 : G)
      $(sum_antipode_mul_eq_algebraMap_counit (ℛ R b)))

Goal state after:
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] := ⋯
c : ℕ → R := ⋯
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')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ n + 2 ≤ 2 * (n + 1)

Tactic:
nlinarith only [h2i]

Goal state after:
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] := ⋯
c : ℕ → R := ⋯
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')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ 2 * (n + 1) ≤ i * (n + 1)

Tactic:
nlinarith only [h2i]

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

Goal state before:
pp: case hIN
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
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := ⋯
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := ⋯
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ map (algebraMap R (Localization.AtPrime q)) q ^ n ≤ map f q • map (algebraMap R (Localization.AtPrime q)) q ^ n

Tactic:
rw [smul_eq_mul, ← pow_succ',
    ← (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)).map_rel_iff]

Goal state after:
case hIN
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
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n) ≤
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1))
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ IsLocalRing.maximalIdeal R ≤ sInf {J | Ideal.span {x} ≤ J ∧ J.IsPrime}

Tactic:
refine le_sInf (fun J ⟨hJ1, hJ2⟩ ↦ ?_)

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
J : Ideal R
x✝ : J ∈ {J | Ideal.span {x} ≤ J ∧ J.IsPrime}
hJ1 : Ideal.span {x} ≤ J
hJ2 : J.IsPrime
⊢ IsLocalRing.maximalIdeal R ≤ J
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
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑x = i ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
nth_rw 1 [← QuotientGroup.out_eq' i, eq_comm, QuotientGroup.eq]

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ (Quotient.out i)⁻¹ * x ∈ ↑H.toOpenSubgroup ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier
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'
x : S ⧸ map (algebraMap R S) p
hx : x ∈ ↑P'
⊢ x ∈ ⇑(Quotient.mk (map (algebraMap R S) p)) '' ↑P

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x

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'
y : S
hx : (Quotient.mk (map (algebraMap R S) p)) y ∈ ↑P'
⊢ (Quotient.mk (map (algebraMap R S) p)) y ∈ ⇑(Quotient.mk (map (algebraMap R S) p)) '' ↑P
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((localized₀FrameHom S (mkLinearMap S M)) (id i))) = ⨅ q ∈ s, q

Tactic:
id_eq,

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((localized₀FrameHom S (mkLinearMap S M)) i)) = ⨅ q ∈ s, q
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
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
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
b : D
hb : b ∉ Zx
⊢ card ↥Zx < card D

Tactic:
refine card_lt_of_injective_of_notMem _ Subtype.val_injective (?_ : b ∉ _)

Goal state after:
case intro.mk
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
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
b : D
hb : b ∉ Zx
⊢ b ∉ Set.range Subtype.val
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
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
⊢ x + a ^ n • y ∈ N

Tactic:
rwa [N.add_mem_iff_right hx, h, ← N.add_mem_iff_right (N.smul_mem (a ^ n) hx), ← smul_add]

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

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
⊢ Injective Rₛ Mₛ

Tactic:
have MB : Baer R M := Baer.of_injective ‹_›

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : Baer R M
⊢ Injective Rₛ Mₛ
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: 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
⊢ (ResidueField R)[(residue S) β] = ⊤ ↔ R[β] = ⊤

Tactic:
by
  constructor
  · intro hβ
    refine eq_top_iff.mpr <| Submodule.le_of_le_smul_of_le_jacobson_bot
      (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
      (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ maximalIdeal R • ⊤)
    intro s _
    rw [adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hβ
    obtain ⟨p, hp⟩ := hβ (residue S s)
    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ residue_surjective p
    rw [Ideal.smul_top_eq_map]
    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
    · rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
    · rw [Algebra.FormallyUnramified.map_maximalIdeal, Submodule.restrictScalars_mem,
        ← Ideal.Quotient.eq]
      -- def eq abuse since IsLocalRing.residue needs to be an abbrev
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl] at hp
      exact hp.symm
  · intro hβ_gen
    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
    intro x
    obtain ⟨s, rfl⟩ := residue_surjective (R := S) x
    obtain ⟨p, rfl⟩ := hβ_gen s
    exact ⟨p.map (residue R), by
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]⟩

Goal state after:
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) ∈ f.pullback g

Tactic:
simpa using hs.symm

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ exp (-d)
triv : g = f
x✝ : n < d
⊢ g.coeff n = f.coeff n

Tactic:
by rw [triv]

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

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

Tactic:
refine fun t s he ↦ funext fun i ↦ ?_

Goal state after:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
⊢ t i = s i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ ↑((renameSymmetricSubalgebra e) ⟨esymm σ R (↑i + 1), ⋯⟩) = esymm τ R (↑i + 1)

Tactic:
renameSymmetricSubalgebra_apply_coe,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ (rename ⇑e) (esymm σ R (↑i + 1)) = esymm τ R (↑i + 1)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
t : Fin n →₀ ℕ
hnm : n ≤ m
inst✝ : Nontrivial R
⊢ ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) t r))) = (accumulate n m) ⇑t

Tactic:
induction t using Finsupp.induction₂ with
  | zero => simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
  | add_single i _ _ _ _ ih =>
    have := i.2.trans_le hnm
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
    · exact monic_esymm this
    · exact (monic_esymm this).pow toLex_add toLex.injective
    · rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]

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

Goal state before:
pp: case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k =
    (ofLex (toLex (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))))) k

Tactic:
dsimp only [Pi.toLex_apply, ofLex_toLex]

Goal state after:
case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k = (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) k
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (p.support.sup ⇑toLex)) i)
    ((ofLex (toLex (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))))) i)

Tactic:
dsimp only [Pi.toLex_apply, ofLex_toLex]

Goal state after:
case inr.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (p.support.sup ⇑toLex)) i < (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ {y | Valued.v.restrict y < ↑(Units.mk0 (Valued.v.restrict x) ⋯)} ⊆ {P | Valued.v P < embedding ↑d}

Tactic:
simp [v_def, Valuation.restrict_lt_iff, ← hx]

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 : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
n : ℕ
⊢ -(-1) ^ n = (-1) ^ (n + 1)

Tactic:
rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_comm]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * esymm σ R k = (-1) ^ k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t

Tactic:
by
  rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]

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

Goal state before:
pp: case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ((expand p hp) φ).order ≤ p • φ.order

Tactic:
obtain ⟨d, hd₁, hd₂⟩ := exists_coeff_ne_zero_and_order (ne_zero_iff_order_finite.mp hφ)

Goal state after:
case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : (coeff d) φ ≠ 0
hd₂ : ↑(Finsupp.degree d) = φ.order
⊢ ((expand p hp) φ).order ≤ p • φ.order
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ((expand p hp) φ).order = p • φ.order

Tactic:
· apply eq_of_le_of_ge
    · obtain ⟨d, hd₁, hd₂⟩ := exists_coeff_ne_zero_and_order (ne_zero_iff_order_finite.mp hφ)
      have : p • φ.order = (p • d).degree := by simp [← hd₂]
      rw [this]
      exact order_le <| (coeff_expand_smul p hp φ _) ▸ hd₁
    · refine MvPowerSeries.le_order fun d hd => ?_
      by_cases! h : ∀ i, p ∣ d i
      · 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
      · obtain ⟨i, hi⟩ := h
        exact coeff_expand_of_not_dvd p hp φ hi

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) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
by
  rw [monomial_eq, Finsupp.prod_fintype]
  · simp only [map_mul, map_prod, leadingCoeff_mul, leadingCoeff_prod]
    rw [AlgEquiv.ofAlgHom_apply, algHom_C, algebraMap_eq, finSuccEquiv_apply,
      eval₂Hom_C, coe_comp]
    simp only [AlgEquiv.ofAlgHom_apply, Function.comp_apply, leadingCoeff_C, map_pow,
      leadingCoeff_pow, algebraMap_eq]
    have : ∀ j, ((finSuccEquiv k n) ((T1 f) 1 (X j))).leadingCoeff = 1 := fun j ↦ by
      by_cases h : j = 0
      · simp [h, finSuccEquiv_apply]
      · simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
        obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
        simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]
    simp only [this, one_pow, Finset.prod_const_one, mul_one]
  exact fun i ↦ pow_zero _

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

Goal state before:
pp: 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) ((X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0

Tactic:
simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right,
    bind₁_C_right]

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
⊢ (1 - ∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
      rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) *
      (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) =
    X n * C (↑p ^ n) * C (⅟↑p ^ n)