[GOAL]
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a : α
⊢ |(-a)| = |a|
[PROOFSTEP]
rw [abs_eq_max_neg, max_comm, neg_neg, abs_eq_max_neg]
[GOAL]
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : |a| = b
⊢ a = b ∨ a = -b
[PROOFSTEP]
simpa only [← h, eq_comm (a := |a|), neg_eq_iff_eq_neg] using abs_choice a
[GOAL]
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
⊢ |a| = |b| ↔ a = b ∨ a = -b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : |a| = |b|
⊢ a = b ∨ a = -b
[PROOFSTEP]
obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h
[GOAL]
case refine'_1.inl
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
b : α
h : |(|b|)| = |b|
⊢ |b| = b ∨ |b| = -b
[PROOFSTEP]
simpa only [neg_eq_iff_eq_neg (a := |b|), neg_inj, or_comm] using abs_choice b
[GOAL]
case refine'_1.inr
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
b : α
h : |(-|b|)| = |b|
⊢ -|b| = b ∨ -|b| = -b
[PROOFSTEP]
simpa only [neg_eq_iff_eq_neg (a := |b|), neg_inj, or_comm] using abs_choice b
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = b ∨ a = -b
⊢ |a| = |b|
[PROOFSTEP]
cases' h with h h
[GOAL]
case refine'_2.inl
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ |a| = |b|
[PROOFSTEP]
simp [h, abs_neg]
[GOAL]
case refine'_2.inr
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = -b
⊢ |a| = |b|
[PROOFSTEP]
simp [h, abs_neg]
[GOAL]
α : 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 : α
ha : 0 ≤ a
hab : a ≤ b
⊢ |a| ≤ |b|
[PROOFSTEP]
rwa [abs_of_nonneg ha, abs_of_nonneg (ha.trans hab)]
[GOAL]
α : 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 : α
⊢ 0 < |a| ↔ a ≠ 0
[PROOFSTEP]
rcases lt_trichotomy a 0 with (ha | rfl | ha)
[GOAL]
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 : α
ha : a < 0
⊢ 0 < |a| ↔ a ≠ 0
[PROOFSTEP]
simp [abs_of_neg ha, neg_pos, ha.ne, ha]
[GOAL]
case inr.inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : α
⊢ 0 < |0| ↔ 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr.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 : α
ha : 0 < a
⊢ 0 < |a| ↔ a ≠ 0
[PROOFSTEP]
simp [abs_of_pos ha, ha, ha.ne.symm]
[GOAL]
α : 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 a : α
⊢ -|a| ≤ a
[PROOFSTEP]
cases' le_total 0 a with h h
[GOAL]
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 a : α
h : 0 ≤ a
⊢ -|a| ≤ a
[PROOFSTEP]
calc
  -|a| = -a := congr_arg Neg.neg (abs_of_nonneg h)
  _ ≤ 0 := (neg_nonpos.mpr h)
  _ ≤ a := h
[GOAL]
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 a : α
h : a ≤ 0
⊢ -|a| ≤ a
[PROOFSTEP]
calc
  -|a| = - -a := congr_arg Neg.neg (abs_of_nonpos h)
  _ ≤ a := (neg_neg a).le
[GOAL]
α : 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 a : α
⊢ 0 ≤ a + |a|
[PROOFSTEP]
rw [← add_right_neg a]
[GOAL]
α : 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 a : α
⊢ a + -a ≤ a + |a|
[PROOFSTEP]
apply add_le_add_left
[GOAL]
case bc
α : 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 a : α
⊢ -a ≤ |a|
[PROOFSTEP]
exact neg_le_abs_self a
[GOAL]
α : 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 a : α
⊢ -|a| ≤ -a
[PROOFSTEP]
simpa using neg_abs_le_self (-a)
[GOAL]
α : 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
ha : a ≤ 0
hab : b ≤ a
⊢ |a| ≤ |b|
[PROOFSTEP]
rw [abs_of_nonpos ha, abs_of_nonpos (hab.trans ha)]
[GOAL]
α : 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
ha : a ≤ 0
hab : b ≤ a
⊢ -a ≤ -b
[PROOFSTEP]
exact neg_le_neg_iff.mpr hab
[GOAL]
α : 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 ∧ a < b ↔ -b < a ∧ a < b
[PROOFSTEP]
rw [neg_lt]
[GOAL]
α : 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 = |a - b|
[PROOFSTEP]
cases' le_total a b with ab ba
[GOAL]
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 = |a - b|
[PROOFSTEP]
rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub]
[GOAL]
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
[PROOFSTEP]
rwa [sub_nonpos]
[GOAL]
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 = |a - b|
[PROOFSTEP]
rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg]
[GOAL]
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
[PROOFSTEP]
rwa [sub_nonneg]
[GOAL]
α : 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 = |b - a|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
α : 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 = |a - b|
[PROOFSTEP]
exact max_sub_min_eq_abs' _ _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a| ≤ b ↔ -b ≤ a ∧ a ≤ b
[PROOFSTEP]
rw [abs_le', and_comm, @neg_le α]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
[PROOFSTEP]
rw [le_abs, or_comm, @le_neg α]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a| ≤ |b| + |b + a|
[PROOFSTEP]
simpa using abs_add (-b) (b + a)
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a - b| ≤ |a| + |b|
[PROOFSTEP]
rw [sub_eq_add_neg, ← abs_neg b]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a + -b| ≤ |a| + |(-b)|
[PROOFSTEP]
exact abs_add a _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
[PROOFSTEP]
rw [abs_le, neg_le_sub_iff_le_add, sub_le_iff_le_add', and_comm, sub_le_iff_le_add']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a - b| < c ↔ a - b < c ∧ b - a < c
[PROOFSTEP]
rw [@abs_lt α, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |a| = |a - b + b|
[PROOFSTEP]
rw [sub_add_cancel]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |b| - |a| ≤ |a - b|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ |b| - |a| ≤ |b - a|
[PROOFSTEP]
apply abs_sub_abs_le_abs_sub
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ |a| = b ↔ a = b ∨ a = -b
[PROOFSTEP]
refine' ⟨eq_or_eq_neg_of_abs_eq, _⟩
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ a = b ∨ a = -b → |a| = b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a c d : α
hb : 0 ≤ a
⊢ |a| = a
[PROOFSTEP]
simp only [abs_neg, abs_of_nonneg hb]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
b c d : α
hb : 0 ≤ b
⊢ |(-b)| = b
[PROOFSTEP]
simp only [abs_neg, abs_of_nonneg hb]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ≤ max |a| |c|
[PROOFSTEP]
simp [hbc.trans (le_abs_self c)]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ -b ≤ max |a| |c|
[PROOFSTEP]
simp [((@neg_le_neg_iff α ..).mpr hab).trans (neg_le_abs_self a)]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ d a b c : α
⊢ |a - c| = |a - b + (b - c)|
[PROOFSTEP]
rw [sub_add_sub_cancel]
