internlm/Lean-Github huggingface dataset:
Theorem: IsNilpotent.finset_sum
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
s : Finset β
hf : ∀ b ∈ s, IsNilpotent (f b)
⊢ IsNilpotent (s.sum f)
Tactic:
induction s using Finset.induction_on with
  | empty => simp only [Finset.sum_empty, IsNilpotent.zero]
  | @insert b s hb hs =>
    rw [Finset.sum_insert hb]
    apply IsNilpotent.add
    exact hf b (s.mem_insert_self b)
    exact hs (fun b hb ↦ hf b (by exact Finset.mem_insert_of_mem hb))
Proof state after:
no goals
Theorem: IsNilpotent.finset_sum
Proof state before:
case empty
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ b ∈ ∅, IsNilpotent (f b)
⊢ IsNilpotent (∅.sum f)
Tactic:
simp only [Finset.sum_empty, IsNilpotent.zero]
Proof state after:
no goals
Theorem: IsNilpotent.finset_sum
Proof state before:
case insert
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent ((insert b s).sum f)
Tactic:
rw [Finset.sum_insert hb]
Proof state after:
case insert
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b + ∑ x ∈ s, f x)
Theorem: IsNilpotent.finset_sum
Proof state before:
case insert
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b + ∑ x ∈ s, f x)
Tactic:
apply IsNilpotent.add
Proof state after:
case insert.ha
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b)

case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)
Theorem: IsNilpotent.finset_sum
Proof state before:
case insert.ha
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b)

case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)
Tactic:
exact hf b (s.mem_insert_self b)
Proof state after:
case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)
Theorem: IsNilpotent.finset_sum
Proof state before:
case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)
Tactic:
exact hs (fun b hb ↦ hf b (by exact Finset.mem_insert_of_mem hb))
Proof state after:
no goals
Theorem: IsNilpotent.finset_sum
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b✝ : β
s : Finset β
hb✝ : b✝ ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b ∈ insert b✝ s, IsNilpotent (f b)
b : β
hb : b ∈ s
⊢ b ∈ insert b✝ s
Tactic:
exact Finset.mem_insert_of_mem hb
Proof state after:
no goals
Theorem: IsNilpotent.finsum
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
⊢ IsNilpotent (_root_.finsum f)
Tactic:
by_cases h : Set.Finite f.support
Proof state after:
case pos
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
h : (Function.support f).Finite
⊢ IsNilpotent (_root_.finsum f)

case neg
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
h : ¬(Function.support f).Finite
⊢ IsNilpotent (_root_.finsum f)
Theorem: IsNilpotent.finsum
Proof state before:
case pos
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
h : (Function.support f).Finite
⊢ IsNilpotent (_root_.finsum f)
Tactic:
rw [finsum_def, dif_pos h]
Proof state after:
case pos
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
h : (Function.support f).Finite
⊢ IsNilpotent (∑ i ∈ h.toFinset, f i)
Theorem: IsNilpotent.finsum
Proof state before:
case pos
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
h : (Function.support f).Finite
⊢ IsNilpotent (∑ i ∈ h.toFinset, f i)
Tactic:
exact IsNilpotent.finset_sum _ (fun b _ ↦ hf b)
Proof state after:
no goals
Theorem: IsNilpotent.finsum
Proof state before:
case neg
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ (b : β), IsNilpotent (f b)
h : ¬(Function.support f).Finite
⊢ IsNilpotent (_root_.finsum f)
Tactic:
simp only [finsum_def, dif_neg h, IsNilpotent.zero]
Proof state after:
no goals
Theorem: MvPowerSeries.monomial_one_eq
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ (monomial R e) 1 = e.prod fun s n => X s ^ n
Tactic:
simp only [← MvPolynomial.coe_X, ← MvPolynomial.coe_pow, ← MvPolynomial.coe_monomial, MvPolynomial.monomial_eq, map_one, one_mul]
Proof state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ ↑(e.prod fun n e => MvPolynomial.X n ^ e) = e.prod fun s n => ↑(MvPolynomial.X s ^ n)
Theorem: MvPowerSeries.monomial_one_eq
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ ↑(e.prod fun n e => MvPolynomial.X n ^ e) = e.prod fun s n => ↑(MvPolynomial.X s ^ n)
Tactic:
simp only [← MvPolynomial.coeToMvPowerSeries.ringHom_apply, ← map_finsupp_prod]
Proof state after:
no goals
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n => (a s • X s) ^ n) = (e.prod fun s n => a s ^ n) • (monomial R e) 1
Tactic:
rw [Finsupp.prod_congr (g2 := fun s n ↦ ((C σ R (algebraMap A R (a s)) * (X s : MvPowerSeries σ R)) ^ n))]
Proof state after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n => ((C σ R) ((algebraMap A R) (a s)) * X s) ^ n) = (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n => ((C σ R) ((algebraMap A R) (a s)) * X s) ^ n) = (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
simp only [mul_pow, Finsupp.prod_mul]
Proof state after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((e.prod fun a_1 b => (C σ R) ((algebraMap A R) (a a_1)) ^ b) * e.prod fun a b => X a ^ b) =
    (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((e.prod fun a_1 b => (C σ R) ((algebraMap A R) (a a_1)) ^ b) * e.prod fun a b => X a ^ b) =
    (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
simp only [← map_pow, ← map_finsupp_prod]
Proof state after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * e.prod fun a b => X a ^ b) =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * e.prod fun a b => X a ^ b) =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
rw [← monomial_one_eq]
Proof state after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * (monomial R e) 1 =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * (monomial R e) 1 =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
rw [← smul_eq_C_mul, ← algebra_compatible_smul]
Proof state after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
intro x _
Proof state after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one
Proof state before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
rw [algebra_compatible_smul R, smul_eq_C_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.monomial_eq'
Proof state before:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (monomial R e) (e.prod fun s n => r s ^ n) = e.prod fun s e => (r s • X s) ^ e
Tactic:
rw [prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: MvPowerSeries.monomial_smul_const
Proof state before:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (monomial R e) (r ^ e.sum fun x n => n) = e.prod fun s e => (r • X s) ^ e
Tactic:
rw [prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
Proof state after:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (monomial R e) (r ^ e.sum fun x n => n) = (monomial R e) (e.prod fun s n => r ^ n)
Theorem: MvPowerSeries.monomial_smul_const
Proof state before:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (monomial R e) (r ^ e.sum fun x n => n) = (monomial R e) (e.prod fun s n => r ^ n)
Tactic:
simp only [Finsupp.sum, Finsupp.prod, Finset.prod_pow_eq_pow_sum]
Proof state after:
no goals
Theorem: MvPowerSeries.substDomain_X
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff σ S) (X s))
Tactic:
simp only [constantCoeff_X, IsNilpotent.zero]
Proof state after:
no goals
Theorem: MvPowerSeries.substDomain_zero
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
this : UniformSpace S := ⊥
x✝ : σ
⊢ IsNilpotent ((constantCoeff τ S) 0)
Tactic:
simp only [Pi.zero_apply, map_zero, IsNilpotent.zero]
Proof state after:
no goals
Theorem: MvPowerSeries.substDomain_add
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
s : σ
⊢ IsNilpotent ((constantCoeff τ S) ((a + b) s))
Tactic:
simp only [Pi.add_apply, map_add]
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (a s) + (constantCoeff τ S) (b s))
Theorem: MvPowerSeries.substDomain_add
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (a s) + (constantCoeff τ S) (b s))
Tactic:
exact IsNilpotent.add (ha.const_coeff s) (hb.const_coeff s)
Proof state after:
no goals
Theorem: MvPowerSeries.substDomain_add
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
⊢ Filter.Tendsto (a + b) Filter.cofinite (nhds 0)
Tactic:
letI : UniformSpace S := ⊥
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ Filter.Tendsto (a + b) Filter.cofinite (nhds 0)
Theorem: MvPowerSeries.substDomain_add
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ Filter.Tendsto (a + b) Filter.cofinite (nhds 0)
Tactic:
convert Filter.Tendsto.add (ha.tendsto_zero) (hb.tendsto_zero)
Proof state after:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ 0 = 0 + 0
Theorem: MvPowerSeries.substDomain_add
Proof state before:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a b : σ → MvPowerSeries τ S
ha : SubstDomain a
hb : SubstDomain b
this : UniformSpace S := ⊥
⊢ 0 = 0 + 0
Tactic:
rw [add_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.constantCoeff_smul
Proof state before:
σ : Type u_1
inst✝¹¹ : DecidableEq σ
A : Type u_2
inst✝¹⁰ : CommSemiring A
R✝ : Type u_3
inst✝⁹ : CommRing R✝
inst✝⁸ : Algebra A R✝
τ : Type u_4
inst✝⁷ : DecidableEq τ
S✝ : Type u_5
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra A S✝
inst✝⁴ : Algebra R✝ S✝
inst✝³ : IsScalarTower A R✝ S✝
R : Type u_6
inst✝² : Semiring R
S : Type u_7
inst✝¹ : Semiring S
inst✝ : Module R S
φ : MvPowerSeries σ S
a : R
⊢ (constantCoeff σ S) (a • φ) = a • (constantCoeff σ S) φ
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.substDomain_mul
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
b a : σ → MvPowerSeries τ S
ha : SubstDomain a
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff τ S) ((b * a) s))
Tactic:
simp only [Pi.mul_apply, map_mul]
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
b a : σ → MvPowerSeries τ S
ha : SubstDomain a
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (b s) * (constantCoeff τ S) (a s))
Theorem: MvPowerSeries.substDomain_mul
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
b a : σ → MvPowerSeries τ S
ha : SubstDomain a
this : UniformSpace S := ⊥
s : σ
⊢ IsNilpotent ((constantCoeff τ S) (b s) * (constantCoeff τ S) (a s))
Tactic:
exact Commute.isNilpotent_mul_right (Commute.all _ _) (ha.const_coeff _)
Proof state after:
no goals
Theorem: MvPowerSeries.substDomain_smul
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
r : MvPowerSeries τ S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
⊢ SubstDomain (r • a)
Tactic:
convert substDomain_mul _ ha
Proof state after:
no goals
Theorem: MvPowerSeries.subst_add
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f g : MvPowerSeries σ R
⊢ subst a (f + g) = subst a f + subst a g
Tactic:
rw [← coe_substAlgHom ha, map_add]
Proof state after:
no goals
Theorem: MvPowerSeries.subst_mul
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f g : MvPowerSeries σ R
⊢ subst a (f * g) = subst a f * subst a g
Tactic:
rw [← coe_substAlgHom ha, map_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.subst_pow
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
n : ℕ
⊢ subst a (f ^ n) = subst a f ^ n
Tactic:
rw [← coe_substAlgHom ha, map_pow]
Proof state after:
no goals
Theorem: MvPowerSeries.subst_smul
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
r : A
f : MvPowerSeries σ R
⊢ subst a (r • f) = r • subst a f
Tactic:
rw [← coe_substAlgHom ha, AlgHom.map_smul_of_tower]
Proof state after:
no goals
Theorem: MvPowerSeries.substAlgHom_X
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
s : σ
⊢ (substAlgHom ha) (X s) = a s
Tactic:
rw [← MvPolynomial.coe_X, substAlgHom_coe, MvPolynomial.aeval_X]
Proof state after:
no goals
Theorem: MvPowerSeries.substAlgHom_monomial
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
e : σ →₀ ℕ
r : R
⊢ (substAlgHom ha) ((monomial R e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n => a s ^ n
Tactic:
rw [← MvPolynomial.coe_monomial, substAlgHom_coe, MvPolynomial.aeval_monomial]
Proof state after:
no goals
Theorem: MvPowerSeries.subst_coe
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
p : MvPolynomial σ R
⊢ subst a ↑p = (MvPolynomial.aeval a) p
Tactic:
rw [← coe_substAlgHom ha, substAlgHom_coe]
Proof state after:
no goals