Theorem: add_tsub_assoc' (Fl/Lemmas.lean)

State before:
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b = a - (b - c)
Tactic:
apply eq_tsub_of_add_eq
State after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + (b - c) = a

State before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + (b - c) = a
Tactic:
rewrite [← add_tsub_assoc_of_le h₂]
State after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + b - c = a

State before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + b - c = a
Tactic:
rewrite [Nat.add_comm a c]
State after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - b + b - c = a

State before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - b + b - c = a
Tactic:
rewrite [tsub_add_cancel_of_le h₁]
State after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - c = a

State before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - c = a
Tactic:
rewrite [Nat.add_comm c a]
State after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - c = a

State before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - c = a
Tactic:
exact add_tsub_cancel_right a c
State after:
no goals