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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ StronglySummable fun p => (homogeneousComponent w p) f
Tactic:
intro d
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)).Finite
Tactic:
apply (finite_toSet {weight w d}).subset
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) ⊆ ↑{(weight w) d}

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) ⊆ ↑{(weight w) d}
Tactic:
intro p
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (p ∈ support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) → p ∈ ↑{(weight w) d}

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (p ∈ support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) → p ∈ ↑{(weight w) d}
Tactic:
rw [Function.mem_support, ne_eq, mem_coe, coeff_homogeneousComponent, Finset.mem_singleton,
  ite_eq_right_iff, not_forall, exists_prop, and_imp]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (weight w) d = p → ¬(coeff α d) f = 0 → p = (weight w) d

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (weight w) d = p → ¬(coeff α d) f = 0 → p = (weight w) d
Tactic:
intro h _
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : (weight w) d = p
a✝ : ¬(coeff α d) f = 0
⊢ p = (weight w) d

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : (weight w) d = p
a✝ : ¬(coeff α d) f = 0
⊢ p = (weight w) d
Tactic:
exact h.symm
State after:
no goals