Theorem: my_equality (LeanCourse/Lectures/Lecture16.lean)

State before:
a b : ℕ
⊢ a + b + a ≤ 2 * (a + b)
Tactic:
set c : ℕ := a + b
State after:
a b : ℕ
c : ℕ := a + b
⊢ c + a ≤ 2 * c

State before:
a b : ℕ
c : ℕ := a + b
⊢ c + a ≤ 2 * c
Tactic:
linarith
State after:
no goals