internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : i ∈ {i | weightedOrder w (f i) ≤ some n}
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Tactic:
simp only [mem_setOf_eq] at hi
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Tactic:
simp only [mem_setOf_eq, Nat.cast_id, ne_eq, mem_iUnion, mem_setOf_eq, exists_prop]
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Tactic:
have heq: (ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i) := by
  rw [ENat.coe_toNat_eq_self]
  exact ne_of_lt (lt_of_le_of_lt hi hn)
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Tactic:
obtain ⟨d, hd⟩ := exists_coeff_ne_zero_of_weightedOrder w (f i) heq
Proof state after:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ ∃ i_1 ∈ s, ¬(coeff α i_1) (f i) = 0
Tactic:
refine' ⟨d, _, hd.2⟩
Proof state after:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ d ∈ s
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe.intro
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
heq : ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w (f i) ∧ (coeff α d) (f i) ≠ 0
⊢ d ∈ s
Tactic:
simpa [← hd.1, WithTop.some_eq_coe, Nat.cast_le] using hi
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ ↑(ENat.toNat (weightedOrder w (f i))) = weightedOrder w (f i)
Tactic:
rw [ENat.coe_toNat_eq_self]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ weightedOrder w (f i) ≠ ⊤
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : weightedOrder w (f i) ≤ some n
⊢ weightedOrder w (f i) ≠ ⊤
Tactic:
exact ne_of_lt (lt_of_le_of_lt hi hn)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.order_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : Finite σ
f : ι → MvPowerSeries σ α
⊢ σ → 1 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.not_mem_unionOfSupportOfCoeffLe_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ i ∉ hf.unionOfSupportOfCoeffLe d ↔ ∀ e ≤ d, (coeff α e) (f i) = 0
Tactic:
simp only [unionOfSupportOfCoeffLe, Finset.mem_biUnion, Finset.mem_Iic, Finite.mem_toFinset,
  mem_support, not_exists, ne_eq, not_and, not_not]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.of_subset_unionOfSupportOfCoeffLe_finite
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d}.Finite
Tactic:
suffices {I : Finset ι | I ⊆ hf.unionOfSupportOfCoeffLe  d} =
  (hf.unionOfSupportOfCoeffLe  d).powerset by
  rw [this]; apply finite_toSet
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
Theorem: MvPowerSeries.StronglySummable.of_subset_unionOfSupportOfCoeffLe_finite
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
ext I
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
I : Finset ι
⊢ I ∈ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} ↔ I ∈ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Theorem: MvPowerSeries.StronglySummable.of_subset_unionOfSupportOfCoeffLe_finite
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
I : Finset ι
⊢ I ∈ {I | I ⊆ hf.unionOfSupportOfCoeffLe d} ↔ I ∈ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
simp only [mem_setOf_eq, coe_powerset, Set.mem_preimage, mem_powerset_iff, Finset.coe_subset]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.of_subset_unionOfSupportOfCoeffLe_finite
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
this : {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
⊢ {I | I ⊆ hf.unionOfSupportOfCoeffLe d}.Finite
Tactic:
rw [this]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
this : {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
⊢ (↑(hf.unionOfSupportOfCoeffLe d).powerset).Finite
Theorem: MvPowerSeries.StronglySummable.of_subset_unionOfSupportOfCoeffLe_finite
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
this : {I | I ⊆ hf.unionOfSupportOfCoeffLe d} = ↑(hf.unionOfSupportOfCoeffLe d).powerset
⊢ (↑(hf.unionOfSupportOfCoeffLe d).powerset).Finite
Tactic:
apply finite_toSet
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ ∀ (d : σ →₀ ℕ), (support fun i => (coeff α d) ((f + g) i)) ⊆ ↑(⋯.toFinset ∪ ⋯.toFinset)
Tactic:
intro d i
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((f + g) i)) → i ∈ ↑(⋯.toFinset ∪ ⋯.toFinset)
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((f + g) i)) → i ∈ ↑(⋯.toFinset ∪ ⋯.toFinset)
Tactic:
simp only [Pi.add_apply, map_add, Function.mem_support, ne_eq, coe_union, Finite.coe_toFinset,
  Set.mem_union]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
⊢ ¬(coeff α d) (f i) + (coeff α d) (g i) = 0 → ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
⊢ ¬(coeff α d) (f i) + (coeff α d) (g i) = 0 → ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Tactic:
intro h
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
⊢ ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
⊢ ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Tactic:
by_cases h₁ : coeff α d (f i) = 0
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : (coeff α d) (f i) = 0
⊢ ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0

case neg
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : ¬(coeff α d) (f i) = 0
⊢ ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : (coeff α d) (f i) = 0
⊢ ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Tactic:
right
Proof state after:
case pos.h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : (coeff α d) (f i) = 0
⊢ ¬(coeff α d) (g i) = 0
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
case pos.h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : (coeff α d) (f i) = 0
⊢ ¬(coeff α d) (g i) = 0
Tactic:
simpa [h₁] using h
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : ¬(coeff α d) (f i) = 0
⊢ ¬(coeff α d) (f i) = 0 ∨ ¬(coeff α d) (g i) = 0
Tactic:
left
Proof state after:
case neg.h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : ¬(coeff α d) (f i) = 0
⊢ ¬(coeff α d) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.support_add
Proof state before:
case neg.h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : DecidableEq ι
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (f i) + (coeff α d) (g i) = 0
h₁ : ¬(coeff α d) (f i) = 0
⊢ ¬(coeff α d) (f i) = 0
Tactic:
exact h₁
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ StronglySummable (f + g)
Tactic:
classical exact fun d => Finite.subset (finite_toSet _) (support_add hf hg d)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ StronglySummable (f + g)
Tactic:
exact fun d => Finite.subset (finite_toSet _) (support_add hf hg d)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
⊢ StronglySummable (a • f)
Tactic:
intro d
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)).Finite
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)).Finite
Tactic:
apply Finite.subset (hf d)
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)) ⊆ support fun i => (coeff α d) (f i)
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((a • f) i)) ⊆ support fun i => (coeff α d) (f i)
Tactic:
intro i
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((a • f) i)) → i ∈ support fun i => (coeff α d) (f i)
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((a • f) i)) → i ∈ support fun i => (coeff α d) (f i)
Tactic:
simp only [Pi.smul_apply', Pi.smul_apply, Function.mem_support, ne_eq]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ ¬(coeff α d) (a i • f i) = 0 → ¬(coeff α d) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
⊢ ¬(coeff α d) (a i • f i) = 0 → ¬(coeff α d) (f i) = 0
Tactic:
intro h h'
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ False
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ False
Tactic:
apply h
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ (coeff α d) (a i • f i) = 0
Theorem: MvPowerSeries.StronglySummable.smul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
a : ι → α
hf : StronglySummable f
d : σ →₀ ℕ
i : ι
h : ¬(coeff α d) (a i • f i) = 0
h' : (coeff α d) (f i) = 0
⊢ (coeff α d) (a i • f i) = 0
Tactic:
rw [coeff_smul, h', MulZeroClass.mul_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι : Type u_3
inst✝³ : Semiring α
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq σ
f : ι → MvPowerSeries σ α
κ : Type u_4
inst✝ : DecidableEq κ
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ ∀ (d : σ →₀ ℕ),
    (support fun i => (coeff α d) (f i.1 * g i.2)) ⊆
      ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Tactic:
rintro d ⟨i, j⟩ h
Proof state after:
case mk
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι : Type u_3
inst✝³ : Semiring α
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq σ
f : ι → MvPowerSeries σ α
κ : Type u_4
inst✝ : DecidableEq κ
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
j : κ
h : (i, j) ∈ support fun i => (coeff α d) (f i.1 * g i.2)
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case mk
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι : Type u_3
inst✝³ : Semiring α
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq σ
f : ι → MvPowerSeries σ α
κ : Type u_4
inst✝ : DecidableEq κ
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
j : κ
h : (i, j) ∈ support fun i => (coeff α d) (f i.1 * g i.2)
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Tactic:
suffices ∃ p ∈ antidiagonal d, coeff α (p.fst : σ →₀ ℕ) (f i) * (coeff α p.snd) (g j) ≠ 0 by
  obtain ⟨⟨b, c⟩, hbc, h'⟩ := this
  simp only [mem_antidiagonal] at hbc
  erw [Finset.mem_product]
  simp only [Finset.mem_biUnion, mem_antidiagonal, Finite.mem_toFinset, mem_support,
    ne_eq, Prod.exists]
  constructor
  . use b, c, hbc
    intro h₁
    apply h'
    rw [h₁, MulZeroClass.zero_mul]
  . use b, c, hbc
    intro h₂
    apply h'
    rw [h₂, MulZeroClass.mul_zero]
Proof state after:
case mk
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι : Type u_3
inst✝³ : Semiring α
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq σ
f : ι → MvPowerSeries σ α
κ : Type u_4
inst✝ : DecidableEq κ
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
i : ι
j : κ
h : (i, j) ∈ support fun i => (coeff α d) (f i.1 * g i.2)
⊢ ∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0