case inl
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : MulZeroOneClass R
h this : Subsingleton R
⊢ order 1 = 0

case inr
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : MulZeroOneClass R
h this : Nontrivial R
⊢ order 1 = 0
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : MulZeroOneClass R
⊢ order 1 = 0
cases' subsingleton_or_nontrivial R with h h <;> haveI := h
no goals
case inl
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : MulZeroOneClass R
h this : Subsingleton R
⊢ order 1 = 0
rw [Subsingleton.elim (1 : HahnSeries Γ R) 0, order_zero]
no goals
case inr
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : MulZeroOneClass R
h this : Nontrivial R
⊢ order 1 = 0
exact order_single one_ne_zero