Theorem: Misc.Array.range_size (LeanSAT/Util/Misc.lean)

State before:
n : Nat
⊢ (Array.range n).size = n
Tactic:
induction n
State after:
case zero

⊢ (Array.range 0).size = 0

case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1

State before:
case zero

⊢ (Array.range 0).size = 0

case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Tactic:
. decide
State after:
case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1

State before:
case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Tactic:
. next n ih =>
  simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
  simp only [Array.range, flip] at ih
  exact ih
State after:
no goals

State before:
case zero

⊢ (Array.range 0).size = 0
Tactic:
decide
State after:
no goals

State before:
case succ
n✝ : Nat
a✝ : (Array.range n✝).size = n✝
⊢ (Array.range (n✝ + 1)).size = n✝ + 1
Tactic:
next n ih =>
simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
simp only [Array.range, flip] at ih
exact ih
State after:
no goals

State before:
n : Nat
ih : (Array.range n).size = n
⊢ (Array.range (n + 1)).size = n + 1
Tactic:
simp only [Array.range, Nat.fold, flip, Array.size_push, Nat.succ.injEq]
State after:
n : Nat
ih : (Array.range n).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n

State before:
n : Nat
ih : (Array.range n).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n
Tactic:
simp only [Array.range, flip] at ih
State after:
n : Nat
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n)).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n

State before:
n : Nat
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n)).size = n
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size = n
Tactic:
exact ih
State after:
no goals