mathlib-initiative/mathlib-tactics huggingface dataset:
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
ha : HasSubst a
s : σ
⊢ (substAlgHom ha) (X s) = a s

Tactic:
by

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
⊢ ∀ (n : ℕ), g_min n = true → g n = true

Tactic:
by

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
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ (substAlgHom ha) ((monomial e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a : σ → MvPowerSeries τ S
r : S
⊢ subst a (C r) = C r

Tactic:
by

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
ha : HasSubst a
s : σ
⊢ subst a (X s) = a s

Tactic:
by

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
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ subst a ((monomial e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n

Tactic:
by

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
ha : HasSubst a
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (subst a)

Tactic:
by

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c / (1 - c) < 1

Tactic:
by

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
ha : HasSubst a
f : MvPowerSeries σ R
e : τ →₀ ℕ
⊢ (coeff e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff e) (d.prod fun s e ↦ a s ^ e)

Tactic:
by

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
ha : HasSubst a
f : MvPowerSeries σ R
⊢ constantCoeff (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 0 = 0

Tactic:
by

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

Goal state before:
pp: case e'_4.refine_1.succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ cantorFunctionAux c g_min (n✝ + 1) = 0

Tactic:
simp [g_min]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
⊢ (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 1)) =
    1

Tactic:
by

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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ i, d i ≠ 0

Tactic:
by

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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
i : σ
hi : d i ≠ 0
⊢ i ∈ d.support

Tactic:
by

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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
i : σ
hi : d i ≠ 0
⊢ (fun a b ↦ 0 ^ b) i (d i) = 0

Tactic:
by

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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ constantCoeff (d.prod fun s e ↦ a s ^ e) = 0

Tactic:
by

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ cantorFunction c f < cantorFunction c g

Tactic:
by

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ ∀ k < n, f k = g k

Tactic:
by

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
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ constantCoeff (subst a f) = 0

Tactic:
by

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)

Tactic:
by

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

Goal state before:
pp: ⊢ #ℝ = 𝔠

Tactic:
by

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

Goal state before:
pp: ⊢ #↑Set.univ = 𝔠

Tactic:
by

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

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ Uncountable ℝ

Tactic:
by

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

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
⊢ (map (algebraMap R S)) f = subst X f

Tactic:
by

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
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
⊢ (map h) (subst a f) = subst (fun i ↦ (map h) (a i)) ((map h) f)

Tactic:
by

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
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ HasSubst 0

Tactic:
by

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

Goal state before:
pp: a : ℝ
⊢ #↑(Ioi a) = 𝔠

Tactic:
by

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

Goal state before:
pp: a : ℝ
⊢ (fun x ↦ a + a - x) '' Iio a = Ioi a

Tactic:
by

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

Goal state before:
pp: a : ℝ
⊢ #↑(Iio a) = 𝔠

Tactic:
by

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
f : MvPowerSeries σ R
⊢ subst 0 f = (map (algebraMap R S)) (C (constantCoeff f))

Tactic:
by

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
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ subst 0 f = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h : a < b
⊢ #↑(Ioo a b) = 𝔠

Tactic:
by

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
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✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ε.comp (substAlgHom ha) = aeval ⋯

Tactic:
by

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

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

Tactic:
by

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
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✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑(aeval ⋯)

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ (Ioo x y).Countable ↔ y ≤ x

Tactic:
by

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

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

Tactic:
by

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
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
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) f

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ (Ico x y).Countable ↔ y ≤ x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ (Ioc x y).Countable ↔ y ≤ x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ #ℂ = 𝔠

Tactic:
by

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

Goal state before:
pp: ⊢ #↑Set.univ = 𝔠

Tactic:
by

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

Goal state before:
pp: ⊢ ¬Set.univ.Countable

Tactic:
by

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

Goal state before:
pp: ⊢ finrank ℝ ℂ = 2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift.{0, u_1} (Module.rank ℝ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ finrank ℝ E = 2 * finrank ℂ E

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff (subst a f))

Tactic:
by

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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff ((substAlgHom ha) f))

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
⊢ ∀ (d : υ →₀ ℕ), {s | (coeff d) ((substAlgHom hb) (a s)) ≠ 0}.Finite

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
⊢ term f s n = f n * ↑n ^ (-s)

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
⊢ term f s n = f n / ↑n ^ s

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
⊢ term f s n = term g s n

Tactic:
by

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
υ : 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
ha : HasSubst a
hb : HasSubst b
⊢ (AlgHom.restrictScalars R (substAlgHom hb)).comp (substAlgHom ha) = substAlgHom ⋯

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ (↑n + 1) ^ s * term f s (n + 1) = f (n + 1)

Tactic:
by

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
υ : 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
ha : HasSubst a
hb : HasSubst b
⊢ subst b ∘ subst a = subst fun s ↦ subst b (a s)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ ‖term f s n‖ ≤ ‖term g s n‖

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ ‖term f s' n‖ ≤ ‖term f s n‖

Tactic:
by

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

Goal state before:
pp: a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
⊢ 0 ≤ term a (↑x) n

Tactic:
by

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

Goal state before:
pp: a : ℕ → ℂ
n : ℕ
hn : n ≠ 0
h : 0 < a n
x : ℝ
⊢ 0 < term a (↑x) n

Tactic:
by

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:
by

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:
by

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, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d ≤ weightedOrder w (subst a f)

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S \ {0}
⊢ term f s n = term g s n

Tactic:
Set.mem_sdiff,

Goal state after:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S ∧ n ∉ {0}
⊢ term f s n = term g s n
Module: Mathlib.NumberTheory.LSeries.Basic

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

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
n : ℕ
hn : term g s n = term f s n
⊢ ‖term g s n‖ ≤ ‖term f s n‖

Tactic:
by

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
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤ weightedOrder w (subst a f)

Tactic:
by

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:
by

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

Goal state before:
pp: s : ℂ
⊢ LSeriesSummable 0 s

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s a : ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
⊢ LSeriesHasSum f s a ↔ LSeriesHasSum g s a

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : LSeriesSummable f s
⊢ LSeriesSummable f s'

Tactic:
by

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

Goal state before:
pp: ⊢ LSeries 0 = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
⊢ f * δ = f 1 • δ

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
h : f 1 = 1
⊢ f * δ = δ

Tactic:
by

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

Goal state before:
pp: ⊢ L δ = 1

Tactic:
by

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
ha : HasSubst a
f : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬(coeff i) f = 0
j : σ
hj : j ∈ i.support
⊢ (⨅ i, weightedOrder (fun x ↦ 1) (a i)) * ↑(i j) ≤ (fun i c ↦ ↑c * weightedOrder (fun x ↦ 1) (a i)) j (i j)

Tactic:
by

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
ha : HasSubst a
f : MvPowerSeries σ R
⊢ (⨅ i, (a i).order) * f.order ≤ (subst a f).order

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ f =O[atTop] fun n ↦ ↑n ^ s.re

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ ‖f 1‖ ≤ C

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ -s.re + x - 1 < -1

Tactic:
by

Goal state after: