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

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

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

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

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

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

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

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

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