Theorem: div_by_5 (BrownCs22/Demos/01-intro.lean)

State before:
p q r : Prop
⊢ ∀ (n : ℕ), 5 ∣ 11 ^ n - 6
Tactic:
intro n
State after:
p q r : Prop
n : ℕ
⊢ 5 ∣ 11 ^ n - 6

State before:
p q r : Prop
n : ℕ
⊢ 5 ∣ 11 ^ n - 6
Tactic:
induction' n with k ih
State after:
case zero
p q r : Prop
⊢ 5 ∣ 11 ^ Nat.zero - 6

case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6

State before:
case zero
p q r : Prop
⊢ 5 ∣ 11 ^ Nat.zero - 6

case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6
Tactic:
. simp
State after:
case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6

State before:
case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6
Tactic:
. cases' ih with w hw
  have : 11 ^ k = 5*w + 6 
  . sorry
  simp [Nat.pow_succ, this, add_mul]
  use w*11
  ring
State after:
no goals