case 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 : α
n : ℕ
a : α
hneg : a ≤ 0
⊢ abs (n • a) = n • abs a

case 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 : α
n : ℕ
a : α
hpos : 0 ≤ a
⊢ abs (n • a) = n • abs a
α : 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 : α
n : ℕ
a : α
⊢ abs (n • a) = n • abs a
cases' le_total a 0 with hneg hpos
case 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 : α
n : ℕ
a : α
hneg : a ≤ 0
⊢ 0 ≤ n • -a
case 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 : α
n : ℕ
a : α
hneg : a ≤ 0
⊢ abs (n • a) = n • abs a
rw [abs_of_nonpos hneg, ← abs_neg, ← neg_nsmul, abs_of_nonneg]
no goals
case 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 : α
n : ℕ
a : α
hneg : a ≤ 0
⊢ 0 ≤ n • -a
exact nsmul_nonneg (neg_nonneg.mpr hneg) n
case 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 : α
n : ℕ
a : α
hpos : 0 ≤ a
⊢ 0 ≤ n • a
case 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 : α
n : ℕ
a : α
hpos : 0 ≤ a
⊢ abs (n • a) = n • abs a
rw [abs_of_nonneg hpos, abs_of_nonneg]
no goals
case 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 : α
n : ℕ
a : α
hpos : 0 ≤ a
⊢ 0 ≤ n • a
exact nsmul_nonneg hpos n