Theorem: concat_empty_seq_id (Saturn/FinSeq.lean)

State before:
α : Type
n : ℕ
⊢ ∀ (seq : FinSeq n α), seq++|FinSeq.empty = seq
Tactic:
intro seq
State after:
α : Type
n : ℕ
seq : FinSeq n α
⊢ seq++|FinSeq.empty = seq

State before:
α : Type
n : ℕ
seq : FinSeq n α
⊢ seq++|FinSeq.empty = seq
Tactic:
apply funext
State after:
case h
α : Type
n : ℕ
seq : FinSeq n α
⊢ ∀ (x : ℕ), (seq++|FinSeq.empty) x = seq x

State before:
case h
α : Type
n : ℕ
seq : FinSeq n α
⊢ ∀ (x : ℕ), (seq++|FinSeq.empty) x = seq x
Tactic:
intro k
State after:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ (seq++|FinSeq.empty) k = seq k

State before:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ (seq++|FinSeq.empty) k = seq k
Tactic:
apply funext
State after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n + zero), (seq++|FinSeq.empty) k x = seq k x

State before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n + zero), (seq++|FinSeq.empty) k x = seq k x
Tactic:
intro kw
State after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n + zero
⊢ (seq++|FinSeq.empty) k kw = seq k kw

State before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n + zero
⊢ (seq++|FinSeq.empty) k kw = seq k kw
Tactic:
apply (concat_aux_eqs rfl seq FinSeq.empty k).left
State after:
no goals