Theorem: cons_commutes (Saturn/Vector.lean)

State before:
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ get' (head ::ᵥ tail) = head+|get' tail
Tactic:
apply funext
State after:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : ℕ), get' (head ::ᵥ tail) x = (head+|get' tail) x

State before:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : ℕ), get' (head ::ᵥ tail) x = (head+|get' tail) x
Tactic:
intro k
State after:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
k : ℕ
⊢ get' (head ::ᵥ tail) k = (head+|get' tail) k

State before:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
k : ℕ
⊢ get' (head ::ᵥ tail) k = (head+|get' tail) k
Tactic:
induction k with
| zero =>
  apply funext
  intro kw
  rfl
| succ k' =>
  apply funext
  intro kw
  rfl
State after:
no goals

State before:
case h.zero
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ get' (head ::ᵥ tail) zero = (head+|get' tail) zero
Tactic:
apply funext
State after:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : zero < succ n), get' (head ::ᵥ tail) zero x = (head+|get' tail) zero x

State before:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : zero < succ n), get' (head ::ᵥ tail) zero x = (head+|get' tail) zero x
Tactic:
intro kw
State after:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
kw : zero < succ n
⊢ get' (head ::ᵥ tail) zero kw = (head+|get' tail) zero kw

State before:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
kw : zero < succ n
⊢ get' (head ::ᵥ tail) zero kw = (head+|get' tail) zero kw
Tactic:
rfl
State after:
no goals

State before:
case h.succ
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
⊢ get' (head ::ᵥ tail) (succ k') = (head+|get' tail) (succ k')
Tactic:
apply funext
State after:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
⊢ ∀ (x : succ k' < succ n), get' (head ::ᵥ tail) (succ k') x = (head+|get' tail) (succ k') x

State before:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
⊢ ∀ (x : succ k' < succ n), get' (head ::ᵥ tail) (succ k') x = (head+|get' tail) (succ k') x
Tactic:
intro kw
State after:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
kw : succ k' < succ n
⊢ get' (head ::ᵥ tail) (succ k') kw = (head+|get' tail) (succ k') kw

State before:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
kw : succ k' < succ n
⊢ get' (head ::ᵥ tail) (succ k') kw = (head+|get' tail) (succ k') kw
Tactic:
rfl
State after:
no goals