case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a - b + b = max a b

case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : b ≤ a
⊢ a - b + b = max a b
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b + b = max a b
cases' le_total a b with h h
no goals
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a - b + b = max a b
rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
no goals
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : b ≤ a
⊢ a - b + b = max a b
rw [max_eq_left h, tsub_add_cancel_of_le h]