-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_snoc {α : Sort*} (as : Fin n → α) (bs : Fin m → α) (b : α) :
    Fin.append as (snoc bs b) = snoc (Fin.append as bs) b

Proof state:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : ¬i < n + m
⊢ b = b

Tactic:
try rfl

Result:
no goals

Proof state:
case h.mk
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b) =
    if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b

Tactic:
split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl)

Result:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b

case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩

Proof state:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

Tactic:
obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt

Result:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
isLt : n + m < n + (m + 1)
lt_n : ¬n + m < n
sub_lt : n + m - n < m
nlt_add : ¬n + m < n + m
⊢ bs ⟨n + m - n, ⋯⟩ = b

Proof state:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
this : i < n + m
⊢ as ⟨i, ⋯⟩ = b

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add

Result:
case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
this : i - n < m
⊢ b = bs ⟨i - n, ⋯⟩

Proof state:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
⊢ append as (snoc bs b) = snoc (append as bs) b

Tactic:
funext i

Result:
case h
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : Fin (n + (m + 1))
⊢ append as (snoc bs b) i = snoc (append as bs) b i

Proof state:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
isLt : n + m < n + (m + 1)
lt_n : ¬n + m < n
sub_lt : n + m - n < m
nlt_add : ¬n + m < n + m
⊢ bs ⟨n + m - n, ⋯⟩ = b

Tactic:
simp [Nat.add_comm n m] at sub_lt

Result:
no goals

Proof state:
case h.mk
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ append as (snoc bs b) ⟨i, isLt⟩ = snoc (append as bs) b ⟨i, isLt⟩

Tactic:
simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
  cast_eq, eq_rec_constant, Nat.add_eq, Nat.add_zero, castLT_mk]

Result:
case h.mk
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ (if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b) =
    if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b

Proof state:
case h
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : Fin (n + (m + 1))
⊢ append as (snoc bs b) i = snoc (append as bs) b i

Tactic:
rcases i with ⟨i, isLt⟩

Result:
case h.mk
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ append as (snoc bs b) ⟨i, isLt⟩ = snoc (append as bs) b ⟨i, isLt⟩

Proof state:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : ¬i < n + m
⊢ b = b

Tactic:
rfl

Result:
no goals

Proof state:
case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
this : i - n < m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
contradiction

Result:
no goals

Proof state:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b

Tactic:
have := Nat.lt_add_right m lt_n

Result:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
this : i < n + m
⊢ as ⟨i, ⋯⟩ = b