Theorem: Nat.two_tri_eq (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
n : Nat
⊢ 2 * n.tri = n * (n + 1)
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  calc
  _ = 2 * (tri n + (n + 1)) := by rfl
  _ = 2 * tri n + 2 * (n + 1) := by rw [Nat.mul_add]
  _ = n * (n + 1) + 2 * (n + 1) := by rw [ih]
  _ = (n + 2) * (n + 1) := by rw [Nat.add_mul]
  _ = (n + 1) * (n + 1 + 1) := by rw [Nat.mul_comm]
State after:
no goals

State before:
case zero

⊢ 2 * tri 0 = 0 * (0 + 1)
Tactic:
rfl
State after:
no goals

State before:
case succ
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n + 1).tri = (n + 1) * (n + 1 + 1)
Tactic:
calc
_ = 2 * (tri n + (n + 1)) := by rfl
_ = 2 * tri n + 2 * (n + 1) := by rw [Nat.mul_add]
_ = n * (n + 1) + 2 * (n + 1) := by rw [ih]
_ = (n + 2) * (n + 1) := by rw [Nat.add_mul]
_ = (n + 1) * (n + 1 + 1) := by rw [Nat.mul_comm]
State after:
no goals

State before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n + 1).tri = 2 * (n.tri + (n + 1))
Tactic:
rfl
State after:
no goals

State before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n.tri + (n + 1)) = 2 * n.tri + 2 * (n + 1)
Tactic:
rw [Nat.mul_add]
State after:
no goals

State before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * n.tri + 2 * (n + 1) = n * (n + 1) + 2 * (n + 1)
Tactic:
rw [ih]
State after:
no goals

State before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ n * (n + 1) + 2 * (n + 1) = (n + 2) * (n + 1)
Tactic:
rw [Nat.add_mul]
State after:
no goals

State before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ (n + 2) * (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
rw [Nat.mul_comm]
State after:
no goals