case inl
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ab : a ≤ b
⊢ max a b - min a b = abs (a - b)

case inr
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ba : b ≤ a
⊢ max a b - min a b = abs (a - b)
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = abs (a - b)
cases' le_total a b with ab ba
case inl
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ab : a ≤ b
⊢ a - b ≤ 0
case inl
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ab : a ≤ b
⊢ max a b - min a b = abs (a - b)
rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub]
no goals
case inl
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ab : a ≤ b
⊢ a - b ≤ 0
rwa [sub_nonpos]
case inr
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ba : b ≤ a
⊢ 0 ≤ a - b
case inr
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ba : b ≤ a
⊢ max a b - min a b = abs (a - b)
rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg]
no goals
case inr
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
ba : b ≤ a
⊢ 0 ≤ a - b
rwa [sub_nonneg]