Theorem: Int.natAbs_le' (Util/Arithmetic.lean)

State before:
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
⊢ ↑(|a|) ≤ b
Tactic:
apply Int.natAbs_eq' a |>.elim <;> (intro h; rwa [h])
State after:
no goals

State before:
case right
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
⊢ ↑(|a|) = -a → ↑(|a|) ≤ b
Tactic:
intro h
State after:
case right
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
h : ↑(|a|) = -a
⊢ ↑(|a|) ≤ b

State before:
case right
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
h : ↑(|a|) = -a
⊢ ↑(|a|) ≤ b
Tactic:
rwa [h]
State after:
no goals