Theorem: Nat.add_sub_assoc' (Algdata/Init/Nat.lean)

State before:
m k : Nat
⊢ m ≤ k → ∀ (n : Nat), n + m - k = n - (k - m)
Tactic:
intro hmk n
State after:
m k : Nat
hmk : m ≤ k
n : Nat
⊢ n + m - k = n - (k - m)

State before:
m k : Nat
hmk : m ≤ k
n : Nat
⊢ n + m - k = n - (k - m)
Tactic:
have : k = (k-m) + m := Eq.symm $ Nat.sub_add_cancel hmk
State after:
m k : Nat
hmk : m ≤ k
n : Nat
this : k = k - m + m
⊢ n + m - k = n - (k - m)

State before:
m k : Nat
hmk : m ≤ k
n : Nat
this : k = k - m + m
⊢ n + m - k = n - (k - m)
Tactic:
conv => lhs; rw [this, Nat.add_sub_add_right]
State after:
no goals