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 : α
n0 : 0 ≤ n
⊢ abs (n • a) = abs 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 : α
n0 : n ≤ 0
⊢ abs (n • a) = abs 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) = abs n • abs a
obtain n0 | n0 := le_total 0 n
case inl.intro
α : 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 a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ abs (↑n • a) = abs ↑n • abs 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 : α
n0 : 0 ≤ n
⊢ abs (n • a) = abs n • abs a
obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
no goals
case inl.intro
α : 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 a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ abs (↑n • a) = abs ↑n • abs a
simp only [abs_nsmul, coe_nat_zsmul, Nat.abs_cast]
case inr.intro
α : 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 : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ abs (n • a) = abs 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 : α
n0 : n ≤ 0
⊢ abs (n • a) = abs n • abs a
obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
case inr.intro
α : 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 : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ abs (m • a) = m • abs a
case inr.intro
α : 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 : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ abs (n • a) = abs n • abs a
rw [← abs_neg, ← neg_zsmul, ← abs_neg n, h, coe_nat_zsmul, Nat.abs_cast, coe_nat_zsmul]
no goals
case inr.intro
α : 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 : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ abs (m • a) = m • abs a
exact abs_nsmul m _