case inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
b0 : b < 0
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case inr.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : b < 0
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
obtain a0 | a0 := le_or_lt 0 a <;> obtain b0 | b0 := le_or_lt 0 b
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case inr.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : b < 0
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
any_goals simp [a0.le, b0.le, abs_of_nonpos, add_nonpos, add_comm]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
have : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) := by
  simp [a0, a0.le, a0.not_le, b0, abs_of_neg, abs_of_nonneg]
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
⊢ b ≤ 0
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
refine' this.mp ⟨fun h => _, fun h => by simp only [le_antisymm h b0, abs_of_neg a0, add_zero]⟩
case inr.inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : a + b ≤ 0
⊢ b ≤ 0

case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : 0 < a + b
⊢ b ≤ 0
case inr.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
⊢ b ≤ 0
obtain ab | ab := le_or_lt (a + b) 0
no goals
case inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
simp [a0, b0, abs_of_nonneg, add_nonneg a0 b0]
no goals
case inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : 0 ≤ a
b0 : b < 0
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
exact (lt_irrefl (0 : α) <| a0.trans_lt <| hle.trans_lt b0).elim
no goals
case inr.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : b < 0
⊢ abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
simp [a0.le, b0.le, abs_of_nonpos, add_nonpos, add_comm]
no goals
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
⊢ (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
simp [a0, a0.le, a0.not_le, b0, abs_of_neg, abs_of_nonneg]
no goals
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : b ≤ 0
⊢ abs (a + b) = -a + b
simp only [le_antisymm h b0, abs_of_neg a0, add_zero]
case inr.inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : a + b ≤ 0
⊢ -b = b
case inr.inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : a + b ≤ 0
⊢ b ≤ 0
refine' le_of_eq (eq_zero_of_neg_eq _)
no goals
case inr.inl.inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : a + b ≤ 0
⊢ -b = b
rwa [abs_of_nonpos ab, neg_add_rev, add_comm, add_right_inj] at h
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : 0 < a + b
⊢ 0 < 0
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : 0 < a + b
⊢ b ≤ 0
refine' (lt_irrefl (0 : α) _).elim
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : a = -a
ab : 0 < a + b
⊢ 0 < 0
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : abs (a + b) = -a + b
ab : 0 < a + b
⊢ 0 < 0
rw [abs_of_pos ab, add_left_inj] at h
no goals
case inr.inl.inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedAddCommGroup α
a b : α
hle : a ≤ b
a0 : a < 0
b0 : 0 ≤ b
this : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) = abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
h : a = -a
ab : 0 < a + b
⊢ 0 < 0
rwa [eq_zero_of_neg_eq h.symm] at a0