Theorem: Hw7.tri_formula (BrownCs22/Homework/Hw7.lean)

State before:
⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1)
Tactic:
basic_induction
State after:
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)

case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)

State before:
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)

case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
{
  dsimp [tri_nums]
}
State after:
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)

State before:
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
{
  intros n h
  dsimp [tri_nums]
  simp
  rewrite [Nat.left_distrib, h]
  linarith
}
State after:
no goals

State before:
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)
Tactic:
dsimp [tri_nums]
State after:
no goals

State before:
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
intros n h
State after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)

State before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
dsimp [tri_nums]
State after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums (n + 0) + (n + 0 + 1)) = (n + 1) * (n + 1 + 1)

State before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums (n + 0) + (n + 0 + 1)) = (n + 1) * (n + 1 + 1)
Tactic:
simp
State after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums n + (n + 1)) = (n + 1) * (n + 1 + 1)

State before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums n + (n + 1)) = (n + 1) * (n + 1 + 1)
Tactic:
rewrite [Nat.left_distrib, h]
State after:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1)

State before:
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ n * (n + 1) + 2 * (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
linarith
State after:
no goals