-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b

Proof state:
a b : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
⊢ (a + b).natAbs ≤ a.natAbs + b.natAbs

Tactic:
match a, b with
| (a:Nat), (b:Nat) => rw [ofNat_add_ofNat, natAbs_ofNat]; apply Nat.le_refl
| (a:Nat), -[b+1]  => rw [natAbs_ofNat, natAbs_negSucc]; apply this
| -[a+1],  (b:Nat) =>
  rw [natAbs_negSucc, natAbs_ofNat, Nat.succ_add, Nat.add_comm a b]; apply this
| -[a+1],  -[b+1]  => rw [natAbs_negSucc, succ_add]; apply Nat.le_refl

Result:
no goals

Proof state:
a b : Int
⊢ ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ

Tactic:
refine fun a b => subNatNat_elim a b.succ
  (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
  (fun i n (e : (n + i).succ = _) => ?_) rfl

Result:
case refine_1
a✝ b✝ : Int
a b : Nat
⊢ ∀ (i n : Nat), (fun m n i => n = b.succ → i.natAbs ≤ (m + b).succ) (n + i) n ↑i

case refine_2
a✝ b✝ : Int
a b i n : Nat
e : (n + i).succ = b.succ
⊢ -[i+1].natAbs ≤ (n + b).succ

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (-[a+1] + ↑b).natAbs ≤ (b + a).succ

Tactic:
apply this

Result:
no goals

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ a + b ≤ (↑a).natAbs + (↑b).natAbs

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : (n + i).succ = b.succ
⊢ i ≤ i + (n + n)

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
case refine_1
a✝ b✝ : Int
a b i n : Nat
h : n = b.succ
⊢ (↑i).natAbs ≤ (n + i + b).succ

Tactic:
subst h

Result:
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ (↑i).natAbs ≤ (b.succ + i + b).succ

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (↑a + -[b+1]).natAbs ≤ a + b.succ

Tactic:
apply this

Result:
no goals

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (-[a+1] + -[b+1]).natAbs ≤ -[a+1].natAbs + -[b+1].natAbs

Tactic:
rw [natAbs_negSucc, succ_add]

Result:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (-[a+1] + -[b+1]).natAbs ≤ (a + -[b+1].natAbs).succ

Proof state:
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ (↑i).natAbs ≤ (i + (b.succ + b)).succ

Tactic:
exact Nat.le_add_right i (b.succ + b).succ

Result:
no goals

Proof state:
a b : Int
⊢ (a + b).natAbs ≤ a.natAbs + b.natAbs

Tactic:
suffices ∀ a b : Nat, natAbs (subNatNat a b.succ) ≤ (a + b).succ by
  match a, b with
  | (a:Nat), (b:Nat) => rw [ofNat_add_ofNat, natAbs_ofNat]; apply Nat.le_refl
  | (a:Nat), -[b+1]  => rw [natAbs_ofNat, natAbs_negSucc]; apply this
  | -[a+1],  (b:Nat) =>
    rw [natAbs_negSucc, natAbs_ofNat, Nat.succ_add, Nat.add_comm a b]; apply this
  | -[a+1],  -[b+1]  => rw [natAbs_negSucc, succ_add]; apply Nat.le_refl

Result:
a b : Int
⊢ ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (↑a + -[b+1]).natAbs ≤ (↑a).natAbs + -[b+1].natAbs

Tactic:
rw [natAbs_ofNat, natAbs_negSucc]

Result:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (↑a + -[b+1]).natAbs ≤ a + b.succ

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (-[a+1] + -[b+1]).natAbs ≤ (a + -[b+1].natAbs).succ

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (↑a + ↑b).natAbs ≤ (↑a).natAbs + (↑b).natAbs

Tactic:
rw [ofNat_add_ofNat, natAbs_ofNat]

Result:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ a + b ≤ (↑a).natAbs + (↑b).natAbs

Proof state:
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : (n + i).succ = b.succ
⊢ i ≤ n + b

Tactic:
rw [← succ.inj e, ← Nat.add_assoc, Nat.add_comm]

Result:
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : (n + i).succ = b.succ
⊢ i ≤ i + (n + n)

Proof state:
case refine_1
a✝ b✝ : Int
a b : Nat
⊢ ∀ (i n : Nat), (fun m n i => n = b.succ → i.natAbs ≤ (m + b).succ) (n + i) n ↑i

Tactic:
intro i n h

Result:
case refine_1
a✝ b✝ : Int
a b i n : Nat
h : n = b.succ
⊢ (↑i).natAbs ≤ (n + i + b).succ

Proof state:
case refine_2
a✝ b✝ : Int
a b i n : Nat
e : (n + i).succ = b.succ
⊢ -[i+1].natAbs ≤ (n + b).succ

Tactic:
apply succ_le_succ

Result:
case refine_2.a
a✝ b✝ : Int
a b i n : Nat
e : (n + i).succ = b.succ
⊢ i ≤ n + b

Proof state:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (-[a+1] + ↑b).natAbs ≤ -[a+1].natAbs + (↑b).natAbs

Tactic:
rw [natAbs_negSucc, natAbs_ofNat, Nat.succ_add, Nat.add_comm a b]

Result:
a✝ b✝ : Int
this : ∀ (a b : Nat), (subNatNat a b.succ).natAbs ≤ (a + b).succ
a b : Nat
⊢ (-[a+1] + ↑b).natAbs ≤ (b + a).succ

Proof state:
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ (↑i).natAbs ≤ (b.succ + i + b).succ

Tactic:
rw [Nat.add_comm _ i, Nat.add_assoc]

Result:
case refine_1
a✝ b✝ : Int
a b i : Nat
⊢ (↑i).natAbs ≤ (i + (b.succ + b)).succ