Theorem: Array.size_init (LeanSAT/Upstream/ToStd.lean)

State before:
n : Nat
α✝ : Type u_1
f : Fin n → α✝
⊢ size (init n f) = n
Tactic:
induction n
State after:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
⊢ size (init Nat.zero f) = Nat.zero

case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝

State before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
⊢ size (init Nat.zero f) = Nat.zero

case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
. simp [size, init_zero]
State after:
case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝

State before:
case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
. next ih =>
  simp [init_succ]; exact ih
State after:
no goals

State before:
case zero
α✝ : Type u_1
f : Fin Nat.zero → α✝
⊢ size (init Nat.zero f) = Nat.zero
Tactic:
simp [size, init_zero]
State after:
no goals

State before:
case succ
α✝ : Type u_1
n✝ : Nat
n_ih✝ : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
next ih =>
simp [init_succ]; exact ih
State after:
no goals

State before:
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init (Nat.succ n✝) f) = Nat.succ n✝
Tactic:
simp [init_succ]
State after:
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init n✝ fun i => f { val := ↑i, isLt := ⋯ }) = n✝

State before:
α✝ : Type u_1
n✝ : Nat
ih : ∀ {f : Fin n✝ → α✝}, size (init n✝ f) = n✝
f : Fin (Nat.succ n✝) → α✝
⊢ size (init n✝ fun i => f { val := ↑i, isLt := ⋯ }) = n✝
Tactic:
exact ih
State after:
no goals