-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_add_of_weightedOrder_ne (h : f.weightedOrder w ≠ g.weightedOrder w) :
    weightedOrder w (f + g) = weightedOrder w f ⊓ weightedOrder w g

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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₁]

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f ⊓ weightedOrder w g

Tactic:
refine le_antisymm ?_ (min_weightedOrder_le_add w)

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ weightedOrder w f ⊓ weightedOrder w g

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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₂]

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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₁⟩

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
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⟩

Result:
no goals