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

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
inst✝¹ : Algebra R ℚ
inst✝ : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this : CharZero R
⊢ ↑x.den ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_2
inst✝ : Semiring R
⊢ order 0 = emultiplicity X 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
φ ψ : R⟦X⟧
i : ℕ
⊢ ((trunc n) (φ - ψ)).coeff i = ((trunc n) φ - (trunc n) ψ).coeff i

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
φ ψ : R⟦X⟧
⊢ (trunc n) (φ - ψ) = (trunc n) φ - (trunc n) ψ

Tactic:
ext i
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : AddSubgroup R
x✝ : ↑I ∈ 𝓝 0 ∧ (∀ (r x : R), x ∈ I → r • x ∈ I) ∧ ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
hI : ↑I ∈ 𝓝 0
hRI : ∀ (r x : R), x ∈ I → r • x ∈ I
hRI' : ∀ (r' : Rᵐᵒᵖ), ∀ x ∈ I, r' • x ∈ I
⊢ ↑(TwoSidedIdeal.mk' ↑I ⋯ ⋯ ⋯ ⋯ ⋯) ⊆ ↑I

Tactic:
simp

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

Goal state before:
pp: case e_f
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x✝ : ι
⊢ d default = (Finsupp.single () (d ())) default

Tactic:
simp

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

Goal state before:
pp: case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d ())) default

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ φ.order.toNat < φ.order.toNat + 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R⟦X⟧
⊢ IsUnit f → f.order = 0

Tactic:
rintro ⟨⟨u, v, hu, hv⟩, hf⟩
  apply And.left
  rw [← add_eq_zero, ← hf, ← nonpos_iff_eq_zero, ← @order_one R _ _, ← hu]
  exact order_mul_ge _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
k : ℕ
⊢ (coeff k) (divXPowOrder 1) = (coeff k) 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ.order.toNat, ψ.order.toNat) ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
s : Finset ι
hs : ¬↑s ⊆ Set.Iio i
x : ι
hxs : x ∈ ↑s
hxi : i ≤ x
⊢ ∀ i ∈ s, 0 ≤ (f i).order

Tactic:
simp

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

Goal state before:
pp: case e'_5.e_5
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ ()) x✝)) default = x✝ default

Tactic:
simp

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

Goal state before:
pp: case e'_5.e_6
R : Type u_1
inst✝¹ : Semiring R
inst✝ : TopologicalSpace R
f : R⟦X⟧
x✝ : Unit →₀ ℕ
⊢ (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ ()) x✝)) default = x✝ default

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
this : Tendsto (⇑φ ∘ ⇑(coeff d) ∘ toMvPowerSeries) (𝓝 0) (𝓝 0)
f : MvPolynomial σ R
⊢ (⇑φ ∘ ⇑(coeff d) ∘ toMvPowerSeries) f ∈ ↑I → φ (MvPolynomial.coeff d f) ∈ I

Tactic:
hf

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
this : Tendsto (⇑φ ∘ ⇑(coeff d) ∘ toMvPowerSeries) (𝓝 0) (𝓝 0)
f : MvPolynomial σ R
hf : (⇑φ ∘ ⇑(coeff d) ∘ toMvPowerSeries) f ∈ ↑I
⊢ φ (MvPolynomial.coeff d f) ∈ I
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: S : Type u_2
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
a : S
ha : HasEval a
⊢ Filter.Tendsto (fun x ↦ a) Filter.cofinite (nhds 0)

Tactic:
simp

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
p : MvPolynomial σ R
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) ↑p = MvPolynomial.eval₂ φ a ⋯.choose

Tactic:
simpa [MvPolynomial.coe_eval₂Hom] using
      toMvPowerSeries_isDenseInducing.extend_eq
        (toMvPowerSeries_uniformContinuous hφ ha).continuous p

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this :
  HasSum ((fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) ∘ Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
x✝ : ℕ
⊢ φ ((coeff x✝) f) * a ^ x✝ = ((fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) ∘ Finsupp.single ()) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ (Finsupp.single () (d ())) default = d default

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ ε ↑p = (ε.comp (coeToMvPowerSeries.algHom R)) p

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ MvPolynomial.eval₂ (algebraMap R S) (fun i ↦ (ε.comp (coeToMvPowerSeries.algHom R)) (MvPolynomial.X i)) p =
    MvPolynomial.eval₂ (algebraMap R S) (fun s ↦ ε.toRingHom (X s)) p

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ #(Set ℕ) = 𝔠

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 1)) n = 1 n

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a.convert_2
⊢ 0 < 1 / 3

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x ↦ a + a - x) '' Ioi a = Iio a ↔ ∀ (a b : ℝ), (fun x ↦ a - x) '' Ioi b = Iio (a - b)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a b : ℝ
h1 : #↑((fun x ↦ x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Tactic:
have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le

Goal state after:
a b : ℝ
h1 : #↑((fun x ↦ x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: x y : ℝ
h : y ≤ x
⊢ (Icc x y).Countable

Tactic:
rcases le_iff_eq_or_lt.mp h with heq | hlt
    · simp [heq]
    · simp [hlt]

Goal state after:
Module: Mathlib.Analysis.Complex.Cardinality

Goal state before:
pp: ⊢ #ℂ = 𝔠

Tactic:
mk_congr Complex.equivRealProd,

Goal state after:
⊢ #(ℝ × ℝ) = 𝔠
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Module.rank ℚ ℝ = 𝔠

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real
  simpa [mk_real] using aleph0_lt_continuum

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Module.rank ℚ ℂ = Module.rank ℚ ℝ

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
f : ℕ → ℂ
s : ℂ
⊢ ‖term f s 0‖ = if 0 = 0 then 0 else ‖f 0‖ / ↑0 ^ s.re

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
⊢ LSeries f s = ∑' (n : ℕ), f n / ↑n ^ s

Tactic:
simp [LSeries, LSeries.term_def₀ hf, cpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
x : σ →₀ ℕ
hfx : ¬(coeff x) f = 0
i : σ
hi : i ∈ x.support
⊢ x i • weightedOrder w (a i) ≤ x i • weightedOrder w (a i)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Tactic:
rw [← Nat.cofinite_eq_atTop] at h
  refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_
  have : term f s =ᶠ[cofinite] term g s := by
    rw [eventuallyEq_iff_exists_mem] at h ⊢
    obtain ⟨S, hS, hS'⟩ := h
    refine ⟨S \ {0}, sdiff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
    rw [Set.mem_sdiff, Set.mem_singleton_iff] at hn
    simp [hn.2, hS' hn.1]
  exact this.symm.mono fun n hn ↦ by simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
s : ℂ
⊢ term δ s 0 = if 0 = 1 then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f * g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) *
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff ((algebraMap R (PowerSeries R)) x))) n =
    ((algebraMap R (ArithmeticFunction R)) x) n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
⊢ ((ofPowerSeries q) f) 0 = 0

Tactic:
simp

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

Goal state before:
pp: case e_a.e_6
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
x✝ : ℕ
⊢ (((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm x✝).prod fun s e ↦ a ^ e) = a ^ x✝

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
⊢ ∀ (x : ℕ), x ≠ n / k → (coeff x) f • (coeff n) ((X ^ k) ^ x) = 0

Tactic:
intro j

Goal state after:
case pos
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
j : ℕ
⊢ j ≠ n / k → (coeff j) f • (coeff n) ((X ^ k) ^ j) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ ∀ (x : ℕ), (coeff x) f • (coeff n) ((X ^ k) ^ x) = 0

Tactic:
intro j

Goal state after:
case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
j : ℕ
⊢ (coeff j) f • (coeff n) ((X ^ k) ^ j) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝³ : CommRing R
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
inst✝¹ : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (subst a f) = (truncTotal k) (∑ i ∈ range k, subst a ((homogeneousComponent i) f))

Tactic:
truncTotal_subst_eq_truncTotal_subst_sum ha ha₁,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝³ : CommRing R
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
inst✝¹ : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)) =
    (truncTotal k) (∑ i ∈ range k, subst a ((homogeneousComponent i) f))
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝³ : CommRing R
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
inst✝¹ : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (∑ x ∈ range k, (substAlgHom ha) ((homogeneousComponent x) f)) =
    (truncTotal k) (∑ i ∈ range k, subst a ((homogeneousComponent i) f))

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁴ : CommRing R
τ : Type u_4
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝¹ : Finite τ
x : σ → ℕ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ ∑ x_1 ∈ range k, (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent x_1) f)) =
    (truncTotal k) ((substAlgHom ⋯) (∑ i ∈ range k, (homogeneousComponent i) f))

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x ↦ a).comp (Polynomial.aeval (MvPolynomial.X ()))) Polynomial.X =
    (Polynomial.aeval a) Polynomial.X

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : 0 • x ∈ s
⊢ egauge 𝕜 s x ≤ ‖0‖ₑ⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ egauge 𝕜 0 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
f : ArithmeticFunction R
⊢ ⇑f ∈ {f | f 0 = 0}

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ 0 • s
b : ℝ≥0∞
hb : ‖0‖ₑ < b
c : 𝕜
hc₀ : c ∈ {0}ᶜ
hcb : c ∈ eball 0 b
⊢ (fun x ↦ c • x) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ₑ ≠ ∞ ∨ egauge 𝕜 s x ≠ ∞

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = 0 • x
⊢ ‖0‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
simp

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

Goal state before:
pp: case h
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∀ i ∈ x.1.support ∪ x.2.support, a i ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: case e_a.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ 0) = (coeff (n + 1 + 1)) (B ^ 0) - if 0 = 1 then k else 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
w : Finset ι
⊢ (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k

Tactic:
hw

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
w : Finset ι
hw : ∀ i ∈ w, i ∈ s
⊢ ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
f : MvPowerSeries σ R
⊢ (rescale 0) f = C (constantCoeff f)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
hw : ∀ i ∈ ∅, i ∈ s
⊢ ∀ k ≤ n, (∏ x ∈ ∅, f x) k = 1 k

Tactic:
simp

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

Goal state before:
pp: case e_a.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) =
    (coeff (n + 2)) (B ^ (i + 2)) - if i + 2 = 1 then k else 0

Tactic:
simp

Goal state after: