Theorem: Nat.sub_sub_eq_add_sub_of_le (One.lean)

State before:
a b c : ℕ
h : c ≤ b
⊢ a - (b - c) = a + c - b
Tactic:
induction a generalizing b c with
| zero => simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, tsub_le_iff_right, Nat.zero_sub,
  tsub_eq_zero_of_le, zero_add, h]
| succ a ih =>
  cases hle: decide (a ≥ (b-c)) with
  | true => 
    simp only [ decide_eq_true_eq] at hle
    rw [Nat.succ_sub hle]
    simp only [tsub_le_iff_right, ge_iff_le] at hle
    rw [Nat.succ_add, Nat.succ_sub hle, ih h]
  | false =>
    simp only [ decide_eq_false_iff_not, not_le] at hle
    have hle₂ := Nat.succ_le_of_lt hle
    rw [Nat.sub_eq_zero_of_le hle₂]
    have hle₃ := Nat.add_le_of_le_sub h hle₂
    rw [Nat.sub_eq_zero_of_le hle₃]
State after:
no goals

State before:
case zero
b c : ℕ
h : c ≤ b
⊢ zero - (b - c) = zero + c - b
Tactic:
simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, tsub_le_iff_right, Nat.zero_sub,
tsub_eq_zero_of_le, zero_add, h]
State after:
no goals

State before:
case succ
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
⊢ succ a - (b - c) = succ a + c - b
Tactic:
cases hle: decide (a ≥ (b-c)) with
| true => 
  simp only [ decide_eq_true_eq] at hle
  rw [Nat.succ_sub hle]
  simp only [tsub_le_iff_right, ge_iff_le] at hle
  rw [Nat.succ_add, Nat.succ_sub hle, ih h]
| false =>
  simp only [ decide_eq_false_iff_not, not_le] at hle
  have hle₂ := Nat.succ_le_of_lt hle
  rw [Nat.sub_eq_zero_of_le hle₂]
  have hle₃ := Nat.add_le_of_le_sub h hle₂
  rw [Nat.sub_eq_zero_of_le hle₃]
State after:
no goals

State before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : decide (a ≥ b - c) = true
⊢ succ a - (b - c) = succ a + c - b
Tactic:
simp only [ decide_eq_true_eq] at hle
State after:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ a - (b - c) = succ a + c - b

State before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ a - (b - c) = succ a + c - b
Tactic:
rw [Nat.succ_sub hle]
State after:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ (a - (b - c)) = succ a + c - b

State before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a ≥ b - c
⊢ succ (a - (b - c)) = succ a + c - b
Tactic:
simp only [tsub_le_iff_right, ge_iff_le] at hle
State after:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : b ≤ a + c
⊢ succ (a - (b - c)) = succ a + c - b

State before:
case succ.true
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : b ≤ a + c
⊢ succ (a - (b - c)) = succ a + c - b
Tactic:
rw [Nat.succ_add, Nat.succ_sub hle, ih h]
State after:
no goals

State before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : decide (a ≥ b - c) = false
⊢ succ a - (b - c) = succ a + c - b
Tactic:
simp only [ decide_eq_false_iff_not, not_le] at hle
State after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
⊢ succ a - (b - c) = succ a + c - b

State before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
⊢ succ a - (b - c) = succ a + c - b
Tactic:
have hle₂ := Nat.succ_le_of_lt hle
State after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ succ a - (b - c) = succ a + c - b

State before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ succ a - (b - c) = succ a + c - b
Tactic:
rw [Nat.sub_eq_zero_of_le hle₂]
State after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ 0 = succ a + c - b

State before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
⊢ 0 = succ a + c - b
Tactic:
have hle₃ := Nat.add_le_of_le_sub h hle₂
State after:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
hle₃ : succ a + c ≤ b
⊢ 0 = succ a + c - b

State before:
case succ.false
a : ℕ
ih : ∀ {b c : ℕ}, c ≤ b → a - (b - c) = a + c - b
b c : ℕ
h : c ≤ b
hle : a < b - c
hle₂ : succ a ≤ b - c
hle₃ : succ a + c ≤ b
⊢ 0 = succ a + c - b
Tactic:
rw [Nat.sub_eq_zero_of_le hle₃]
State after:
no goals