-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_cons {α : Sort*} (a : α) (as : Fin n → α) (bs : Fin m → α) :
    Fin.append (cons a as) bs
    = cons a (Fin.append as bs) ∘ (Fin.cast <| Nat.add_right_comm n 1 m)

Proof state:
case pos
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : i + 1 < n + 1
⊢ cases a as ⟨i + 1, ⋯⟩ = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
have : i < n := Nat.lt_of_succ_lt_succ h

Result:
case pos
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : i + 1 < n + 1
this : i < n
⊢ cases a as ⟨i + 1, ⋯⟩ = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Proof state:
case h.mk
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i < n + 1 + m
⊢ (if h : i < n + 1 then cases a as ⟨i, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i, isLt✝⟩)

Tactic:
rcases i with - | i

Result:
case h.mk.zero
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
isLt✝ : 0 < n + 1 + m
⊢ (if h : 0 < n + 1 then cases a as ⟨0, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨0, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨0, isLt✝⟩)

case h.mk.succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Proof state:
case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
this : ¬i < n
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
simp [addCases, this]

Result:
no goals

Proof state:
case h
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : Fin (n + 1 + m)
⊢ append (cons a as) bs i = (cons a (append as bs) ∘ Fin.cast ⋯) i

Tactic:
rcases i with ⟨i, -⟩

Result:
case h.mk
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i < n + 1 + m
⊢ append (cons a as) bs ⟨i, isLt✝⟩ = (cons a (append as bs) ∘ Fin.cast ⋯) ⟨i, isLt✝⟩

Proof state:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
⊢ append (cons a as) bs = cons a (append as bs) ∘ Fin.cast ⋯

Tactic:
funext i

Result:
case h
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : Fin (n + 1 + m)
⊢ append (cons a as) bs i = (cons a (append as bs) ∘ Fin.cast ⋯) i

Proof state:
case pos
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : i + 1 < n + 1
this : i < n
⊢ cases a as ⟨i + 1, ⋯⟩ = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
simp [addCases, this]

Result:
no goals

Proof state:
case h.mk.succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
split_ifs with h

Result:
case pos
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : i + 1 < n + 1
⊢ cases a as ⟨i + 1, ⋯⟩ = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Proof state:
case h.mk.zero
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
isLt✝ : 0 < n + 1 + m
⊢ (if h : 0 < n + 1 then cases a as ⟨0, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨0, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨0, isLt✝⟩)

Tactic:
simp

Result:
no goals

Proof state:
case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
have : ¬i < n := Nat.not_le.mpr <| Nat.lt_succ.mp <| Nat.not_le.mp h

Result:
case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
this : ¬i < n
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Proof state:
case h.mk
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i < n + 1 + m
⊢ append (cons a as) bs ⟨i, isLt✝⟩ = (cons a (append as bs) ∘ Fin.cast ⋯) ⟨i, isLt✝⟩

Tactic:
simp only [append, addCases, cons, castLT, cast, comp_apply]

Result:
case h.mk
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i < n + 1 + m
⊢ (if h : i < n + 1 then cases a as ⟨i, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i, isLt✝⟩)