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

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f ⊓ weightedOrder w g
Tactic:
refine' le_antisymm _ (le_weightedOrder_add w _ _)
State after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
by_cases H₁ : f.weightedOrder w < g.weightedOrder w
State after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

State before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
simp only [le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₁]
State after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g

State before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g
Tactic:
exact ⟨le_rfl, le_of_lt H₁⟩
State after:
no goals

State before:
case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
by_cases H₂ : g.weightedOrder w < f.weightedOrder w
State after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : ¬weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

State before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
simp only [add_comm f g, le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₂]
State after:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w g ≤ weightedOrder w f ∧ weightedOrder w g ≤ weightedOrder w g

State before:
case pos
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : weightedOrder w g < weightedOrder w f
⊢ weightedOrder w g ≤ weightedOrder w f ∧ weightedOrder w g ≤ weightedOrder w g
Tactic:
exact ⟨le_of_lt H₂, le_rfl⟩
State after:
no goals

State before:
case neg
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
H₂ : ¬weightedOrder w g < weightedOrder w f
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g
Tactic:
exact absurd (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁)) h
State after:
no goals