case pos
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : f = 0
⊢ order (-f) = order f

case neg
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : ¬f = 0
⊢ order (-f) = order f
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
⊢ order (-f) = order f
by_cases hf : f = 0
no goals
case neg
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : ¬f = 0
⊢ order (-f) = order f
simp only [order, support_neg, neg_eq_zero]
no goals
case pos
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : HahnSeries Γ R
hf : f = 0
⊢ order (-f) = order f
simp only [hf, neg_zero]