internlm/Lean-Github huggingface dataset:
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 : σ →₀ ℕ
i : ι
j : κ
h : (i, j) ∈ support fun i => (coeff α d) (f i.1 * g i.2)
this : ∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Tactic:
obtain ⟨⟨b, c⟩, hbc, h'⟩ := this
Proof state after:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
hbc : (b, c) ∈ antidiagonal d
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
hbc : (b, c) ∈ antidiagonal d
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Tactic:
simp only [mem_antidiagonal] at hbc
Proof state after:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ (i, j) ∈ ↑(((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset))
Tactic:
erw [Finset.mem_product]
Proof state after:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ((i, j).1 ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset) ∧ (i, j).2 ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ((i, j).1 ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset) ∧ (i, j).2 ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset
Tactic:
simp only [Finset.mem_biUnion, mem_antidiagonal, Finite.mem_toFinset, mem_support,
  ne_eq, Prod.exists]
Proof state after:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ (∃ a b, a + b = d ∧ ¬(coeff α a) (f i) = 0) ∧ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ (∃ a b, a + b = d ∧ ¬(coeff α a) (f i) = 0) ∧ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Tactic:
constructor
Proof state after:
case intro.mk.intro.left
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α a) (f i) = 0

case intro.mk.intro.right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro.left
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α a) (f i) = 0

case intro.mk.intro.right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Tactic:
. use b, c, hbc
  intro h₁
  apply h'
  rw [h₁, MulZeroClass.zero_mul]
Proof state after:
case intro.mk.intro.right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro.right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Tactic:
. use b, c, hbc
  intro h₂
  apply h'
  rw [h₂, MulZeroClass.mul_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro.left
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α a) (f i) = 0
Tactic:
use b, c, hbc
Proof state after:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ¬(coeff α b) (f i) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ¬(coeff α b) (f i) = 0
Tactic:
intro h₁
Proof state after:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₁ : (coeff α b) (f i) = 0
⊢ False
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₁ : (coeff α b) (f i) = 0
⊢ False
Tactic:
apply h'
Proof state after:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₁ : (coeff α b) (f i) = 0
⊢ (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₁ : (coeff α b) (f i) = 0
⊢ (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) = 0
Tactic:
rw [h₁, MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case intro.mk.intro.right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ∃ a b, a + b = d ∧ ¬(coeff α b) (g j) = 0
Tactic:
use b, c, hbc
Proof state after:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ¬(coeff α c) (g j) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
⊢ ¬(coeff α c) (g j) = 0
Tactic:
intro h₂
Proof state after:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₂ : (coeff α c) (g j) = 0
⊢ False
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₂ : (coeff α c) (g j) = 0
⊢ False
Tactic:
apply h'
Proof state after:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₂ : (coeff α c) (g j) = 0
⊢ (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) = 0
Theorem: MvPowerSeries.StronglySummable.support_mul
Proof state before:
case right
σ : 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)
b c : σ →₀ ℕ
h' : (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) ≠ 0
hbc : b + c = d
h₂ : (coeff α c) (g j) = 0
⊢ (coeff α (b, c).1) (f i) * (coeff α (b, c).2) (g j) = 0
Tactic:
rw [h₂, MulZeroClass.mul_zero]
Proof state after:
no goals
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)
⊢ ∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0
Tactic:
by_contra 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)
h' : ¬∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0
⊢ False
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)
h' : ¬∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0
⊢ False
Tactic:
refine' h (sum_eq_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)
h' : ¬∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f (i, j).1) * (coeff α x.2) (g (i, j).2) = 0
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)
h' : ¬∃ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) ≠ 0
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f (i, j).1) * (coeff α x.2) (g (i, j).2) = 0
Tactic:
push_neg at 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)
h' : ∀ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) = 0
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f (i, j).1) * (coeff α x.2) (g (i, j).2) = 0
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)
h' : ∀ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (g j) = 0
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f (i, j).1) * (coeff α x.2) (g (i, j).2) = 0
Tactic:
simp only [mem_antidiagonal] at 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)
h' : ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ)), p.1 + p.2 = d → (coeff α p.1) (f i) * (coeff α p.2) (g j) = 0
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), x.1 + x.2 = d → (coeff α x.1) (f i) * (coeff α x.2) (g j) = 0
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)
h' : ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ)), p.1 + p.2 = d → (coeff α p.1) (f i) * (coeff α p.2) (g j) = 0
⊢ ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), x.1 + x.2 = d → (coeff α x.1) (f i) * (coeff α x.2) (g j) = 0
Tactic:
exact h'
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.mul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ StronglySummable fun i => f i.1 * g i.2
Tactic:
classical exact fun d => Finite.subset (finite_toSet _) (support_mul hf hg d)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.mul
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ StronglySummable fun i => f i.1 * g i.2
Tactic:
exact fun d => Finite.subset (finite_toSet _) (support_mul hf hg d)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.coeff_sum
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
⊢ (coeff α d) hf.sum = ∑ i ∈ s, (coeff α d) (f i)
Tactic:
rw [coeff_sum_def, sum_subset (Finite.toFinset_subset.mpr hs)]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
⊢ ∀ x ∈ s, x ∉ ⋯.toFinset → (coeff α d) (f x) = 0
Theorem: MvPowerSeries.StronglySummable.coeff_sum
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
⊢ ∀ x ∈ s, x ∉ ⋯.toFinset → (coeff α d) (f x) = 0
Tactic:
intro i _ hi'
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
i : ι
a✝ : i ∈ s
hi' : i ∉ ⋯.toFinset
⊢ (coeff α d) (f i) = 0