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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
⊢ weightedOrder w ((monomial α d) a) = if a = 0 then ⊤ else ↑((weight w) d)
Tactic:
split_ifs with h
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial α d) a) = ⊤

case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial α d) a) = ⊤
Tactic:
rw [h, weightedOrder_eq_top_iff, LinearMap.map_zero]
State after:
no goals

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Tactic:
rw [weightedOrder_eq_nat]
State after:
case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0
Tactic:
constructor
State after:
case neg.left
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0

case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0

State before:
case neg.left
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (weight w) d_1 = (weight w) d ∧ (coeff α d_1) ((monomial α d) a) ≠ 0
Tactic:
use d
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (weight w) d = (weight w) d ∧ (coeff α d) ((monomial α d) a) ≠ 0

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (weight w) d = (weight w) d ∧ (coeff α d) ((monomial α d) a) ≠ 0
Tactic:
simp only [coeff_monomial_same, eq_self_iff_true, ne_eq, true_and_iff]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ¬a = 0

State before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ¬a = 0
Tactic:
exact h
State after:
no goals

State before:
case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff α d_1) ((monomial α d) a) = 0
Tactic:
intro b hb
State after:
case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff α b) ((monomial α d) a) = 0

State before:
case neg.right
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff α b) ((monomial α d) a) = 0
Tactic:
rw [coeff_monomial, if_neg]
State after:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d

State before:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d
Tactic:
intro h
State after:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h✝ : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
h : b = d
⊢ False

State before:
case neg.right.hnc
σ : Type u_1
α : Type u_2
inst✝¹ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
inst✝ : Decidable (a = 0)
h✝ : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
h : b = d
⊢ False
Tactic:
simp only [h, lt_self_iff_false] at hb
State after:
no goals