[GOAL]
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ max a 1 / max a⁻¹ 1 = a
[PROOFSTEP]
rcases le_total a 1 with (h | h)
[GOAL]
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : a ≤ 1
⊢ max a 1 / max a⁻¹ 1 = a
[PROOFSTEP]
simp [h]
[GOAL]
case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a
⊢ max a 1 / max a⁻¹ 1 = a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ min (a / c) (b / c) = min a b / c
[PROOFSTEP]
simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ max (a / c) (b / c) = max a b / c
[PROOFSTEP]
simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ min (a / b) (a / c) = a / max b c
[PROOFSTEP]
simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a✝ b✝ c✝ a b c : α
⊢ max (a / b) (a / c) = a / min b c
[PROOFSTEP]
simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max a b - max c d ≤ max (a - c) (b - d)
[PROOFSTEP]
simp only [sub_le_iff_le_add, max_le_iff]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ a ≤ max (a - c) (b - d) + max c d ∧ b ≤ max (a - c) (b - d) + max c d
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ a ≤ max (a - c) (b - d) + max c d
case right α : Type u_1 inst✝ : LinearOrderedAddCommGroup α a✝ b✝ c✝ a b c d : α ⊢ b ≤ max (a - c) (b - d) + max c d
[PROOFSTEP]
calc
  a = a - c + c := (sub_add_cancel a c).symm
  _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_left _ _) (le_max_left _ _)
[GOAL]
case right
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ b ≤ max (a - c) (b - d) + max c d
[PROOFSTEP]
calc
  b = b - d + d := (sub_add_cancel b d).symm
  _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_right _ _) (le_max_right _ _)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ |max a b - max c d| ≤ max |a - c| |b - d|
[PROOFSTEP]
refine' abs_sub_le_iff.2 ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max a b - max c d ≤ max |a - c| |b - d|
[PROOFSTEP]
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max |a - c| |b - d|
[PROOFSTEP]
rw [abs_sub_comm a c, abs_sub_comm b d]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|
[PROOFSTEP]
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ |min a b - min c d| ≤ max |a - c| |b - d|
[PROOFSTEP]
simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using abs_max_sub_max_le_max (-a) (-b) (-c) (-d)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c : α
⊢ |max a c - max b c| ≤ |a - b|
[PROOFSTEP]
simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))] using abs_max_sub_max_le_max a c b c
