Theorem: MvPowerSeries.StronglySummable.support_mul (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

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
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))

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]
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

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
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))

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
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))

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]
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

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]
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

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
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

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]
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

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]
State after:
no goals

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
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

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₁
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

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'
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

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]
State after:
no goals

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
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

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₂
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

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'
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

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]
State after:
no goals

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'
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

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 _)
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

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'
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

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' ⊢
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

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'
State after:
no goals