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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), ↑i < ⊤ → (coeff i) φ = 0
⊢ ∀ (n : ℕ), (coeff n) φ = (coeff n) 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), ↑i < ⊤ → (coeff i) φ = 0
⊢ φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff i) φ = 0
⊢ ∀ i < n, (coeff i) φ = 0

Tactic:
simpa using

Goal state after:
case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff i) φ = 0
⊢ ∀ i < n, (coeff i) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff i) φ = 0
⊢ ↑n ≤ φ.order

Tactic:
| coe n =>

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

Goal state before:
pp: case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ φ.order = ↑n ↔ (∀ (i : ℕ), ↑i = ↑n → (coeff i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n → (coeff i) φ = 0

Tactic:
| coe n =>

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
ψ_lt_φ : ψ.order < φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
simpa using

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
ψ_lt_φ : ψ.order < φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r ≤ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ v.intValuation r ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r < 1 ↔ r ∈ v.asIdeal

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ v.intValuation r < 1 ↔ r ∈ v.asIdeal
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ ↑0 < φ.order

Tactic:
simpa using

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ 0 < φ.order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hf : constantCoeff φ = 0
⊢ ↑n ≤ n • φ.order

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hf : constantCoeff φ = 0
⊢ ↑n ≤ ↑n * φ.order
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 : ℚ
⊢ Function.Injective (⇑(algebraMap R ℚ) ∘ Nat.cast)

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
inst✝¹ : Algebra R ℚ
inst✝ : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
⊢ Function.Injective Nat.cast
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ φ = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝ : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ φ = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ X ^ φ.order.toNat ∣ φ

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ ∀ m < φ.order.toNat, (coeff m) φ = 0
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 ⋯ ⋯ ⋯ ⋯ ⋯) ∈ 𝓝 0

Tactic:
simpa using

Goal state after:
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
⊢ ↑I ∈ 𝓝 0
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : ℕ → R
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) (mk a))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : ℕ → R
h : ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
⊢ ∀ (d : ℕ), HasSum (fun i ↦ (coeff d) (f i)) (a d)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
⊢ ↑n = emultiplicity X φ

Tactic:
| coe n =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ order 1 = 0
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
k : ι
hk : i < k
⊢ ↑n < (f k).order

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
k : ι
hk : i < k
⊢ ↑n < (f k).order
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case h
σ : 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✝ : σ → ℕ := ⋯
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ ↑I
⊢ n ∈ {n | a s ^ n.succ ∈ I}

Tactic:
simpa using

Goal state after:
case h
σ : 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}
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ ↑I
⊢ a s ^ (n + 1) ∈ I
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
s : σ
has : a s ∈ ↑I
⊢ n s = 0 s

Tactic:
simpa using

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
s : σ
has : a s ∈ ↑I
⊢ a s ∈ I
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
hf : (⇑φ ∘ ⇑(coeff d) ∘ toMvPowerSeries) f ∈ ↑I
⊢ φ (MvPolynomial.coeff d f) ∈ I

Tactic:
simpa using

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.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
⊢ (if d' = 0 then x else 0) ∈ J

Tactic:
split_ifs <;> [exact hx; exact J.zero_mem]

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

Goal state before:
pp: case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
this : ∀ (d' : σ →₀ ℕ), (coeff d') (C x) ∈ J
⊢ x ∈ ↑K

Tactic:
simpa using

Goal state after:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
this : ∀ (d' : σ →₀ ℕ), (coeff d') (C x) ∈ J
⊢ x ∈ K
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
this : ∀ d' ≤ d, (coeff d') ((monomial e) x) ∈ J
⊢ x ∈ K

Tactic:
simpa using

Goal state after:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
this : ∀ d' ≤ d, (coeff d') ((monomial e) x) ∈ J
⊢ x ∈ K
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 using

Goal state after:
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 p
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → constantCoeff ((map (Ideal.Quotient.mk I)) f) ^ b = 0
n : ℕ
hn : N + Finsupp.degree d ≤ n
⊢ (coeff d) ((map (Ideal.Quotient.mk I)) (f ^ n)) = 0

Tactic:
simpa using

Goal state after:
case h
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : ↑I ∈ 𝓝 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → constantCoeff ((map (Ideal.Quotient.mk I)) f) ^ b = 0
n : ℕ
hn : N + Finsupp.degree d ≤ n
⊢ (coeff d) ((map (Ideal.Quotient.mk I)) f ^ n) = 0
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
T : Type u_3
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous ⇑ε
p : Polynomial R
⊢ (⇑ε ∘ eval₂ φ a) ↑p = Polynomial.eval₂ (ε.comp φ) (ε a) p

Tactic:
simpa using

Goal state after:
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
T : Type u_3
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous ⇑ε
p : Polynomial R
⊢ ε (Polynomial.eval₂ φ a p) = Polynomial.eval₂ (ε.comp φ) (ε a) p
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ ℶ_ 1 = 𝔠

Tactic:
simpa using

Goal state after:
⊢ ℶ_ 1 = 𝔠
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠

Tactic:
← continuum_power_aleph0

Goal state after:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
S : Type u_5
inst✝ : CommRing S
this : UniformSpace S := ⊥
⊢ HasSubst fun s ↦ X s

Tactic:
simpa using

Goal state after:
σ : Type u_1
S : Type u_5
inst✝ : CommRing S
this : UniformSpace S := ⊥
⊢ HasEval fun s ↦ X s
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
simpa using

Goal state after:
case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ c ^ n
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 : τ →₀ ℕ
⊢ (coeff n) (subst 0 f) = (coeff n) ((map (algebraMap R S)) (C (constantCoeff f)))

Tactic:
rw [coeff_subst (by simp [hasSubst_def]), coeff_map, finsum_eq_single _ 0]

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
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ (coeff 0) f • (coeff n) (Finsupp.prod 0 fun s e ↦ 0 s ^ e) = (algebraMap R S) ((coeff n) (C (constantCoeff f)))

σ : 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 : τ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ 0 → (coeff x) f • (coeff n) (x.prod fun s e ↦ 0 s ^ e) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    x.1 + x.2 = k →
      ¬({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) x = (q ^ i, q ^ j)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    x.1 + x.2 = k →
      ¬({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) x = (q ^ i, q ^ j)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i) *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ j) =
    0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : i + j = k ∧ q ^ k ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    x.1 + x.2 = k →
      ¬({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) x = (q ^ i, q ^ j)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0

Tactic:
simpa using h (i, j) hab.1

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
ε : MvPowerSeries τ S →ₐ[R] T := AlgHom.restrictScalars R (aeval hb)
hε : Continuous ⇑ε
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) f

Tactic:
simpa using

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
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
ε : MvPowerSeries τ S →ₐ[R] T := AlgHom.restrictScalars R (aeval hb)
hε : Continuous ⇑ε
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun s ↦ eval₂ (algebraMap S T) b (a s)) f
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos
σ : 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)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent ((algebraMap R S) ((coeff 0) f))

Tactic:
simpa using

Goal state after:
case pos
σ : 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)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent ((algebraMap R S) (constantCoeff f))
Module: Mathlib.Analysis.Complex.Cardinality

Goal state before:
pp: ⊢ ℵ₀ < 𝔠

Tactic:
apply cantor

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

Goal state before:
pp: ⊢ lift.{0, 0} #ℚ < lift.{0, 0} #ℝ

Tactic:
simpa using

Goal state after:
⊢ ℵ₀ < 𝔠
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ

Tactic:
simpa using

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:
simpa using

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
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff (subst a 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
υ : 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
this✝¹ : UniformSpace R := ⋯
this✝ : UniformSpace S := ⋯
this : UniformSpace T := ⋯
⊢ Continuous ⇑(AlgHom.restrictScalars R (substAlgHom hb))

Tactic:
simpa using

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
υ : 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
this✝¹ : UniformSpace R := ⊥
this✝ : UniformSpace S := ⊥
this : UniformSpace T := ⊥
⊢ Continuous (subst b)