Theorem: Nat.minus_add_cancel (PnP2023/Lec_01_20/NatMinus.lean)

State before:
m n : ℕ
hyp : n ≤ m
⊢ minus m n hyp + n = m
Tactic:
match m, n, hyp with
| m, 0, _ => simp [minus]
| 0, _ +1, pf => contradiction
| m + 1, n + 1 , pf =>
  simp [minus]
  rw [← add_assoc]
  simp [minus_add_cancel]
State after:
no goals

State before:
m✝ n : ℕ
hyp : n ≤ m✝
m : ℕ
x✝ : 0 ≤ m
⊢ minus m 0 x✝ + 0 = m
Tactic:
simp [minus]
State after:
no goals

State before:
m n : ℕ
hyp : n ≤ m
n✝ : ℕ
pf : n✝ + 1 ≤ 0
⊢ minus 0 (n✝ + 1) pf + (n✝ + 1) = 0
Tactic:
contradiction
State after:
no goals

State before:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus (m + 1) (n + 1) pf + (n + 1) = m + 1
Tactic:
simp [minus]
State after:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + (n + 1) = m + 1

State before:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + (n + 1) = m + 1
Tactic:
rw [← add_assoc]
State after:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + n + 1 = m + 1

State before:
m✝ n✝ : ℕ
hyp : n✝ ≤ m✝
m n : ℕ
pf : n + 1 ≤ m + 1
⊢ minus m n ⋯ + n + 1 = m + 1
Tactic:
simp [minus_add_cancel]
State after:
no goals