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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝³ : Algebra.IsIntegral R S
this✝² : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
r : R ⧸ P
⊢ (algebraMap (R ⧸ P) (S ⧸ Q)) (r ^ Fintype.card (R ⧸ P)) = (algebraMap (R ⧸ P) (S ⧸ Q)) r

Tactic:
FiniteField.pow_card

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝³ : Algebra.IsIntegral R S
this✝² : Q.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
r : R ⧸ P
⊢ (algebraMap (R ⧸ P) (S ⧸ Q)) r = (algebraMap (R ⧸ P) (S ⧸ Q)) r
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : 𝒜 →ₐᵍ[R] fun x ↦ Submodule.restrictScalars R (ℬ x)
⊢ ↑((fun f ↦
          let __src := (AlgHom.liftEquiv R S A B).symm ↑f;
          { toAlgHom := __src, map_mem := ⋯ })
        ((fun f ↦
            let __src := (AlgHom.liftEquiv R S A B) ↑f;
            { toAlgHom := __src, map_mem := ⋯ })
          f)) =
    ↑f

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : (fun x ↦ baseChange S (𝒜 x)) →ₐᵍ[S] ℬ
⊢ ↑((fun f ↦
          let __src := (AlgHom.liftEquiv R S A B) ↑f;
          { toAlgHom := __src, map_mem := ⋯ })
        ((fun f ↦
            let __src := (AlgHom.liftEquiv R S A B).symm ↑f;
            { toAlgHom := __src, map_mem := ⋯ })
          f)) =
    ↑f

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ (coeff 0) (invUnitsSub u * X) = (coeff 0) (invUnitsSub u * C ↑u - 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
⊢ (map f) (invUnitsSub u) = invUnitsSub ((Units.map ↑f) u)

Tactic:
ext
  simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]
  rfl

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

Goal state before:
pp: case zero
S : Type u_1
inst✝ : CommRing S
⊢ (coeff 0) ((1 - X) * mk 1) = (coeff 0) 1

Tactic:
simp

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

Goal state before:
pp: case zero
S : Type u_1
inst✝ : CommRing S
d n✝ : ℕ
⊢ (coeff n✝) (mk 1 ^ (0 + 1)) = (coeff n✝) (mk fun n ↦ ↑((0 + n).choose 0))

Tactic:
simp

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : g = 0
⊢ ((powerSeriesFamily 0 f) 0).coeff 0 = (PowerSeries.constantCoeff f • 1).coeff 0

Tactic:
simp

Goal state after:
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
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
aux₁ : 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:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
d n : ℕ
⊢ (1 + X) ^ d = ↑((1 + Polynomial.X) ^ d)

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
x✝³ : ℕ × ℕ
x✝² : x✝³ ∈ ↑⋯.toFinset
x✝¹ : ℕ × ℕ
x✝ : x✝¹ ∈ ↑⋯.toFinset
⊢ (fun x ↦ ⟨x.1 + x.2, x⟩) x✝³ = (fun x ↦ ⟨x.1 + x.2, x⟩) x✝¹ → x✝³ = x✝¹

Tactic:
simp

Goal state after:
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
⊢ (⋃ a, (0 a).support).IsPWO

Tactic:
simp

Goal state after:
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
⊢ ∀ (g : Γ), {a | (0 a).coeff g ≠ 0}.Finite

Tactic:
simp

Goal state after:
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
s : SummableFamily Γ R α
g : Γ
a : α
⊢ a ∈ Set.Finite.toFinset ⋯ ↔ (s a).coeff g ≠ 0

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x✝ : Γ
⊢ (hsum 0).coeff x✝ = HahnSeries.coeff 0 x✝

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ ∀ x ∈ t, x ∉ Set.Finite.toFinset ⋯ → (s x).coeff g = 0

Tactic:
simp

Goal state after:
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
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
⊢ (Pi.single i x i).support.IsPWO

Tactic:
simp

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

Goal state before:
pp: case inl
Γ : 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
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
h✝ : IsEmpty ι
⊢ (⋃ a, x.support).IsPWO

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ Eq.recOn ⋯ ⟨i.snd.1 + i.snd.2, (i.snd.1, i.snd.2)⟩.snd = i.snd

Tactic:
simp

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

Goal state before:
pp: case «0»
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
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨0, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: case «1»
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
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨1, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
g : Γ
⊢ (if 0 = 0 then (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = HahnSeries.coeff 1 g

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
a b : R⟦X⟧
⊢ (powerSeriesFamily x (a * b)).hsum = (powerSeriesFamily x a).hsum * (powerSeriesFamily x b).hsum

Tactic:
by
    simp only [← hsum_mul, hsum_powerSeriesFamily_mul]

Goal state after:
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⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

Tactic:
simp

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
⊢ ({ toFun := fun a ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } 1).coeff g =
    x.coeff g

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = (coeff 0) f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (i : Fin (Nat.succ 0).succ), constantCoeff (![X (), 0] i) = 0

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝¹ : Γ × Γ'
x✝ : x✝¹ ∈ VAddAntidiagonal g ⋯
⊢ s.hsum.coeff x✝¹.1 • t.hsum.coeff x✝¹.2 = s.hsum.coeff x✝¹.1 • t.hsum.coeff x✝¹.2

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (i : Fin (Nat.succ 0).succ), constantCoeff (![0, X ()] i) = 0

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : R⟦ℕ⟧
x✝ : ℕ
⊢ ((fun f ↦ { coeff := fun n ↦ (PowerSeries.coeff n) f, isPWO_support' := ⋯ })
          ((fun f ↦ PowerSeries.mk f.coeff) f)).coeff
      x✝ =
    f.coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : PowerSeries R
n✝ : ℕ
⊢ (PowerSeries.coeff n✝)
      ((fun f ↦ PowerSeries.mk f.coeff)
        ((fun f ↦ { coeff := fun n ↦ (PowerSeries.coeff n) f, isPWO_support' := ⋯ }) f)) =
    (PowerSeries.coeff n✝) f

Tactic:
simp

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

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ (toPowerSeries.symm x).coeff n = (PowerSeries.coeff n) x

Tactic:
simp

Goal state after:
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✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝¹ : R⟦Γ⟧
x✝ : α
⊢ (x✝¹ • 0) x✝ = 0 x✝

Tactic:
simp

Goal state after:
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✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝³ : R⟦Γ⟧
x✝² x✝¹ : SummableFamily Γ' V α
x✝ : α
⊢ (x✝³ • (x✝² + x✝¹)) x✝ = (x✝³ • x✝² + x✝³ • x✝¹) x✝

Tactic:
simp

Goal state after:
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✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝¹ : SummableFamily Γ' V α
x✝ : α
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_6
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ 0 = Nat.castOrderEmbedding 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ r = (toPowerSeries.symm (PowerSeries.C r)).coeff 0

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_6
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ 1 = Nat.castOrderEmbedding 1

Tactic:
simp

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

Goal state before:
pp: case e'_3
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ 1 = (toPowerSeries.symm PowerSeries.X).coeff 1

Tactic:
simp

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

Goal state before:
pp: case top
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))
hf₃ : Function.Injective ⇑f₃
hf₃class :
  ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
    (ofLex a).orderTop =
      (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
        (ofLex (f₃ a)).orderTop
a : M
⊢ (DivisibleHull.archimedeanClassOrderIso M).symm
      ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M))
        ((FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr ⊤)) =
    (FiniteArchimedeanClass.withTopOrderIso M) ⊤

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
R : Type u_3
inst✝ : Semiring R
n : ℕ
⊢ (ofPowerSeries Γ R) (PowerSeries.X ^ n) = (single ↑n) 1

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f : R⟦σ →₀ ℕ⟧
x✝ : σ →₀ ℕ
⊢ ((fun f ↦ { coeff := f, isPWO_support' := ⋯ }) ((fun f ↦ f.coeff) f)).coeff x✝ = f.coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n✝) ((fun f ↦ f.coeff) ((fun f ↦ { coeff := f, isPWO_support' := ⋯ }) f)) =
    (MvPowerSeries.coeff n✝) f

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n✝) (f + g).coeff = (MvPowerSeries.coeff n✝) (f.coeff + g.coeff)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b : A
a : GroupLike R A
⊢ ↑(a⁻¹ * a) = ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
H : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀ :=
  x✝
f : R[X]
⊢ f.Monic →
    ∀ (a₀ : R),
      Polynomial.eval a₀ f ∈ maximalIdeal R →
        IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R

Tactic:
hf

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
H : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀ :=
  x✝
f : R[X]
hf : f.Monic
⊢ ∀ (a₀ : R),
    Polynomial.eval a₀ f ∈ maximalIdeal R →
      IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: case zero
Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
⊢ (x ^ 0).cardSupp ≤ x.cardSupp ^ 0

Tactic:
simp

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

Goal state before:
pp: case neg.zero
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
⊢ (0 ^ 0).cardSupp ≤ x.cardSupp ^ 0

Tactic:
simp

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

Goal state before:
pp: case neg.succ
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
n✝ : ℕ
⊢ (0 ^ (n✝ + 1)).cardSupp ≤ x.cardSupp ^ (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
⊢ 0⁻¹.cardSupp ≤ max ℵ₀ (cardSupp 0)

Tactic:
simp

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

Goal state before:
pp: case h₂
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x).cardSupp ≤ x.cardSupp

Tactic:
refine (cardSupp_single_mul_le _ (-x.order) x.leadingCoeff⁻¹).trans' <| cardSupp_mono fun _ ↦ ?_

Goal state after:
case h₂
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
hx : x ≠ 0
x✝ : Γ
⊢ x✝ ∈ (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x).support → x✝ ∈ ((single (-x.order)) x.leadingCoeff⁻¹ * x).support
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
hκ : Fact (ℵ₀ ≤ κ)
⊢ ∀ {x : R⟦Γ⟧}, x ∈ (cardSuppLTAddSubmonoid Γ R κ).carrier → -x ∈ (cardSuppLTAddSubmonoid Γ R κ).carrier

Tactic:
simp

Goal state after: