Theorem: sumOfSequence_eq (LeanMeetup/Exercise02Solutions.lean)

State before:
n : ℕ
⊢ sumOfSequence n = n * (n + 1) / 2
Tactic:
simp [Nat.mul_add]
State after:
n : ℕ
⊢ sumOfSequence n = (n * n + n) / 2

State before:
n : ℕ
⊢ sumOfSequence n = (n * n + n) / 2
Tactic:
induction n
State after:
case zero

⊢ sumOfSequence Nat.zero = (Nat.zero * Nat.zero + Nat.zero) / 2

case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2

State before:
case zero

⊢ sumOfSequence Nat.zero = (Nat.zero * Nat.zero + Nat.zero) / 2

case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2
Tactic:
next      => rfl
State after:
case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2

State before:
case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2
Tactic:
next n ih =>
  simp only [sumOfSequence, ih, Nat.add_succ, add_zero, Nat.succ_mul, Nat.mul_succ, Nat.succ_add]
  simp [
    Nat.add_div (b:=2),
    Nat.add_assoc (_+n) n n,
    ←Nat.mul_two n,
    Nat.add_div (b := n*2)
  ]
State after:
no goals

State before:
⊢ sumOfSequence Nat.zero = (Nat.zero * Nat.zero + Nat.zero) / 2
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
ih : sumOfSequence n = (n * n + n) / 2
⊢ sumOfSequence (Nat.succ n) = (Nat.succ n * Nat.succ n + Nat.succ n) / 2
Tactic:
simp only [sumOfSequence, ih, Nat.add_succ, add_zero, Nat.succ_mul, Nat.mul_succ, Nat.succ_add]
State after:
n : ℕ
ih : sumOfSequence n = (n * n + n) / 2
⊢ Nat.succ ((n * n + n) / 2 + n) = Nat.succ (Nat.succ (n * n + n + n + n)) / 2

State before:
n : ℕ
ih : sumOfSequence n = (n * n + n) / 2
⊢ Nat.succ ((n * n + n) / 2 + n) = Nat.succ (Nat.succ (n * n + n + n + n)) / 2
Tactic:
simp [
  Nat.add_div (b:=2),
  Nat.add_assoc (_+n) n n,
  ←Nat.mul_two n,
  Nat.add_div (b := n*2)
]
State after:
no goals

State before:
n : ℕ
⊢ sumOfSequence n = n * (n + 1) / 2
Tactic:
sorry
State after:
no goals