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

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
rcases eq_or_ne f 0 with (rfl | hf)
State after:
case inl
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
n : ℕ
⊢ weightedOrder w 0 = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) 0 ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) 0 = 0

case inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0

State before:
case inl
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
n : ℕ
⊢ weightedOrder w 0 = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) 0 ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) 0 = 0
Tactic:
simp only [weightedOrder_zero, ENat.top_ne_coe, map_zero, ne_eq, not_true, and_false,
  exists_false, implies_true, forall_const, and_true]
State after:
no goals

State before:
case inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ weightedOrder w f = ↑n ↔
    (∃ d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
simp only [weightedOrder, dif_neg hf, ne_eq, Nat.cast_inj, Nat.find_eq_iff]
State after:
case inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ((∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔
    (∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0

State before:
case inr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ((∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔
    (∃ d, (weight w) d = n ∧ ¬(coeff α d) f = 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
apply and_congr_right'
State after:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0

State before:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ n_1 < n, ¬∃ d, (weight w) d = n_1 ∧ ¬(coeff α d) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
simp only [not_exists, not_and, Classical.not_not, imp_forall_iff]
State after:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (n_1 : ℕ) (x : σ →₀ ℕ), n_1 < n → (weight w) x = n_1 → (coeff α x) f = 0) ↔
    ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0

State before:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (n_1 : ℕ) (x : σ →₀ ℕ), n_1 < n → (weight w) x = n_1 → (coeff α x) f = 0) ↔
    ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
rw [forall_swap]
State after:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (y : σ →₀ ℕ), ∀ x < n, (weight w) y = x → (coeff α y) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0

State before:
case inr.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ (∀ (y : σ →₀ ℕ), ∀ x < n, (weight w) y = x → (coeff α y) f = 0) ↔ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
Tactic:
apply forall_congr'
State after:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ∀ (a : σ →₀ ℕ), (∀ x < n, (weight w) a = x → (coeff α a) f = 0) ↔ (weight w) a < n → (coeff α a) f = 0

State before:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
⊢ ∀ (a : σ →₀ ℕ), (∀ x < n, (weight w) a = x → (coeff α a) f = 0) ↔ (weight w) a < n → (coeff α a) f = 0
Tactic:
intro d
State after:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) ↔ (weight w) d < n → (coeff α d) f = 0

State before:
case inr.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) ↔ (weight w) d < n → (coeff α d) f = 0
Tactic:
constructor
State after:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) → (weight w) d < n → (coeff α d) f = 0

case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ ((weight w) d < n → (coeff α d) f = 0) → ∀ x < n, (weight w) d = x → (coeff α d) f = 0

State before:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ (∀ x < n, (weight w) d = x → (coeff α d) f = 0) → (weight w) d < n → (coeff α d) f = 0
Tactic:
intro h hd
State after:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : ∀ x < n, (weight w) d = x → (coeff α d) f = 0
hd : (weight w) d < n
⊢ (coeff α d) f = 0

State before:
case inr.h.h.mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : ∀ x < n, (weight w) d = x → (coeff α d) f = 0
hd : (weight w) d < n
⊢ (coeff α d) f = 0
Tactic:
exact h (weight w d) hd rfl
State after:
no goals

State before:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
⊢ ((weight w) d < n → (coeff α d) f = 0) → ∀ x < n, (weight w) d = x → (coeff α d) f = 0
Tactic:
intro h m hm hd
State after:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : m < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0

State before:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : m < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0
Tactic:
rw [← hd] at hm
State after:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : (weight w) d < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0

State before:
case inr.h.h.mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
hf : f ≠ 0
d : σ →₀ ℕ
h : (weight w) d < n → (coeff α d) f = 0
m : ℕ
hm : (weight w) d < n
hd : (weight w) d = m
⊢ (coeff α d) f = 0
Tactic:
exact h hm
State after:
no goals