Theorem: List.length_ofFn_go (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
n : Nat
α : Type u_1
f : Fin n → α
i j : Nat
h : i + j = n
⊢ (ofFn.go f i j h).length = i
Tactic:
induction i generalizing j with
| zero => simp[ofFn.go]
| succ n ih =>
  dsimp [ofFn.go]
  rw [ih]
State after:
no goals

State before:
case zero
n : Nat
α : Type u_1
f : Fin n → α
j : Nat
h : 0 + j = n
⊢ (ofFn.go f 0 j h).length = 0
Tactic:
simp[ofFn.go]
State after:
no goals

State before:
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f (n + 1) j h).length = n + 1
Tactic:
dsimp [ofFn.go]
State after:
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f n (j + 1) ⋯).length + 1 = n + 1

State before:
case succ
n✝ : Nat
α : Type u_1
f : Fin n✝ → α
n : Nat
ih : ∀ {j : Nat} {h : n + j = n✝}, (ofFn.go f n j h).length = n
j : Nat
h : n + 1 + j = n✝
⊢ (ofFn.go f n (j + 1) ⋯).length + 1 = n + 1
Tactic:
rw [ih]
State after:
no goals