mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁶ : 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
⊢ UniformContinuous (eval₂ φ a)

Tactic:
by

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✝⁶ : 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
f : MvPowerSeries σ R
⊢ HasSum (fun d ↦ φ ((coeff d) f) * d.prod fun s e ↦ a s ^ e) (eval₂ φ a f)

Tactic:
by

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 ()) = d

Tactic:
by

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⟧
⊢ HasSum (fun d ↦ φ ((coeff d) f) * a ^ d) (eval₂ φ a f)

Tactic:
by

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✝⁶ : 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
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p
⊢ ε = eval₂ φ a

Tactic:
by

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
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε ↑p = Polynomial.eval₂ φ a p
⊢ ε = eval₂ φ a

Tactic:
by

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
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 ⇑ε
⊢ Continuous ⇑(ε.comp φ)

Tactic:
by

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
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 ⇑ε
⊢ ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (ε a)

Tactic:
by

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
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
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
p : Polynomial R
⊢ (aeval ha) ↑p = (Polynomial.aeval a) p

Tactic:
by

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
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
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
⊢ HasSum (fun d ↦ (coeff d) f • a ^ d) ((aeval ha) f)

Tactic:
by

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✝¹³ : 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
T : Type u_4
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[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ Continuous[inst✝¹⁶.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑(ε.comp φ)

Tactic:
simp only [coe_comp, Continuous.comp hε hφ]

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✝¹³ : 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
T : Type u_4
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[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)

Tactic:
by

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✝⁸ : 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
ha : HasEval a
r : R
⊢ (↑↑(eval₂Hom ⋯ ha)).toFun ((algebraMap R (MvPowerSeries σ R)) r) = (algebraMap R S) r

Tactic:
by

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
a : σ → 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
ha : HasEval a
⊢ ⇑(aeval ha) = eval₂ (algebraMap R S) a

Tactic:
by

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
a : σ → 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
ha : HasEval a
⊢ Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑(aeval ha)

Tactic:
by

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
a : σ → 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
ha : HasEval a
p : MvPolynomial σ R
⊢ (aeval ha) ↑p = (MvPolynomial.aeval a) p

Tactic:
by

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] ⇑ε
⊢ aeval ⋯ = ε

Tactic:
by

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
a : σ → 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
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum (fun d ↦ (coeff d) f • d.prod fun s e ↦ a s ^ e) ((aeval ha) f)

Tactic:
by

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
a : σ → 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
ha : HasEval a
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : IsUniformAddGroup T
inst✝⁵ : IsTopologicalRing T
inst✝⁴ : IsLinearTopology T T
inst✝³ : T2Space T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst✝¹⁸.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑ε
⊢ ε.comp (aeval ha) = aeval ⋯

Tactic:
by

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

Goal state before:
pp: ⊢ lift.{v, u_1} 𝔠 = 𝔠

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c

Tactic:
by
  rw [← lift_continuum.{v, u}, lift_le]

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠

Tactic:
by
  rw [← lift_continuum.{v, u}, lift_le]

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

Goal state before:
pp: c : Cardinal.{u}
⊢ 𝔠 < lift.{v, u} c ↔ 𝔠 < c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < 𝔠 ↔ c < 𝔠

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ℵ_ 1 ≤ 𝔠

Tactic:
by

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

Goal state before:
pp: ⊢ 𝔠 ^ ℵ₀ = 𝔠

Tactic:
by

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

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

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
inst✝¹ : TopologicalSpace S
inst✝ : DiscreteTopology S
⊢ Filter.Tendsto a Filter.cofinite (nhds 0) ↔ ∀ (d : τ →₀ ℕ), {s | (coeff d) (a s) ≠ 0}.Finite

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
inst✝¹ : TopologicalSpace S
inst✝ : DiscreteTopology S
⊢ HasSubst a ↔ HasEval a

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
⊢ HasSubst fun x ↦ 0

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 b : σ → MvPowerSeries τ S
ha : HasSubst a
hb : HasSubst b
⊢ HasSubst (a + b)

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
b a : σ → MvPowerSeries τ S
ha : HasSubst a
⊢ HasSubst (b * a)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
S : Type u_5
inst✝ : CommRing S
⊢ HasSubst fun s ↦ X 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
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
d : τ →₀ ℕ
⊢ {s | (coeff d) ((map h) (a s)) ≠ 0} ⊆ {s | (coeff d) (a 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
a : σ → R
⊢ HasSubst (a • X)

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
inst✝ : Finite σ
a : σ → MvPowerSeries τ S
ha : ∀ (s : σ), constantCoeff (a s) = 0
s : σ
⊢ IsNilpotent (constantCoeff (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
i j : σ
⊢ ∀ (s : Fin (Nat.succ 0).succ), constantCoeff (![X i, X j] 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
i : σ
⊢ ∀ (s : Fin (Nat.succ 0).succ), constantCoeff (![X i, 0] 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
i : σ
⊢ ∀ (s : Fin (Nat.succ 0).succ), constantCoeff (![0, X i] s) = 0

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
n : ℕ
hn : n ≠ 0
a : σ → MvPowerSeries τ S
h : HasSubst a
⊢ 0 < n

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
S : Type u_5
inst✝ : CommRing S
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

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
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
⊢ IsNilpotent (constantCoeff ↑((MvPowerSeries.truncTotal (x i)) (a i)))

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
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
d : τ →₀ ℕ
i : σ
⊢ i ∈ {s | (coeff d) ↑((MvPowerSeries.truncTotal (x s)) (a s)) ≠ 0} → i ∈ {s | (coeff d) (a 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
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ subst = eval₂ (algebraMap R (MvPowerSeries τ 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
p : MvPolynomial σ R
⊢ subst a ↑p = (MvPolynomial.aeval a) p

Tactic:
by

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = c ^ n

Tactic:
by

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = g n
⊢ cantorFunctionAux c f n = cantorFunctionAux c g n

Tactic:
by

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⇑(substAlgHom ha) = ⇑(aeval ⋯)

Tactic:
by

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
⊢ (fun n ↦ cantorFunctionAux c f (n + 1)) = fun n ↦ c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
by

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ Summable (cantorFunctionAux c 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
⊢ ⇑(substAlgHom ha) = subst a

Tactic:
by

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

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ cantorFunction c f ≤ cantorFunction c g

Tactic:
by

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)

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
⊢ 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
⊢ subst X = id

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
⊢ (substAlgHom ha) f = 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 g : MvPowerSeries σ R
⊢ subst a (f + g) = subst a f + subst a g

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 g : MvPowerSeries σ R
⊢ subst a (f - g) = subst a f - subst a g

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
⊢ ∀ (n : ℕ), f n = true → f_max 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
f g : MvPowerSeries σ R
⊢ subst a (f * g) = subst a f * subst a g

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
n : ℕ
⊢ subst a (f ^ n) = subst a f ^ n

Tactic:
by

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

Goal state before:
pp: σ : 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 : σ → MvPowerSeries τ S
ha : HasSubst a
r : A
f : MvPowerSeries σ R
⊢ subst a (r • f) = r • 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
p : MvPolynomial σ R
⊢ (substAlgHom ha) ↑p = (MvPolynomial.aeval a) p

Tactic:
by

Goal state after: