Theorem: MvPowerSeries.exists_coeff_ne_zero_of_weightedOrder (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, ↑((weight w) d) = weightedOrder w f ∧ (coeff α d) f ≠ 0
Tactic:
classical
simp_rw [weightedOrder, dif_neg ((weightedOrder_finite_iff_ne_zero _ f).mp h), Nat.cast_inj]
generalize_proofs h1
exact Nat.find_spec h1
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, ↑((weight w) d) = weightedOrder w f ∧ (coeff α d) f ≠ 0
Tactic:
simp_rw [weightedOrder, dif_neg ((weightedOrder_finite_iff_ne_zero _ f).mp h), Nat.cast_inj]
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, (weight w) d = Nat.find ⋯ ∧ (coeff α d) f ≠ 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ ∃ d, (weight w) d = Nat.find ⋯ ∧ (coeff α d) f ≠ 0
Tactic:
generalize_proofs h1
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
h1 : ∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0
⊢ ∃ d, (weight w) d = Nat.find h1 ∧ (coeff α d) f ≠ 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ↑(toNat (weightedOrder w f)) = weightedOrder w f
h1 : ∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0
⊢ ∃ d, (weight w) d = Nat.find h1 ∧ (coeff α d) f ≠ 0
Tactic:
exact Nat.find_spec h1
State after:
no goals