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

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

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

State before:
a b c : ℕ
h : c = a + b
⊢ a + b + a ≤ 2 * (a + b)
Tactic:
rw [← h]
State after:
a b c : ℕ
h : c = a + b
⊢ c + a ≤ 2 * c

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