-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_snoc_eq_snoc_cons {β : Sort*} (a : β) (q : Fin n → β) (b : β) :
    @cons n.succ (fun _ ↦ β) a (snoc q b) = snoc (cons a q) b

Proof state:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
⊢ snoc q b j = snoc (cons a q) b j.succ

Tactic:
by_cases h' : j.val < n

Result:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ↑j < n
⊢ snoc q b j = snoc (cons a q) b j.succ

case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ¬↑j < n
⊢ snoc q b j = snoc (cons a q) b j.succ

Proof state:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ↑j < n
⊢ snoc q b j = snoc (cons a q) b j.succ

Tactic:
set k := castLT j h' with jk

Result:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
⊢ snoc q b j = snoc (cons a q) b j.succ

Proof state:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Tactic:
have : i = j.succ := by rw [ji, succ_pred]

Result:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Proof state:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this✝ : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
this : j = k.castSucc
⊢ (if h : ↑k.castSucc < n then cast ⋯ (q (k.castSucc.castLT h)) else cast ⋯ b) = snoc (cons a q) b k.succ.castSucc

Tactic:
simp [pred, snoc, cons]

Result:
no goals

Proof state:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ¬↑j < n
⊢ snoc q b j = snoc (cons a q) b j.succ

Tactic:
rw [eq_last_of_not_lt h', succ_last]

Result:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ¬↑j < n
⊢ snoc q b (last n) = snoc (cons a q) b (last n.succ)

Proof state:
case h
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Tactic:
by_cases h : i = 0

Result:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i

case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Proof state:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this✝ : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
this : j = k.castSucc
⊢ snoc q b j = snoc (cons a q) b j.succ

Tactic:
rw [this, ← castSucc_fin_succ, snoc]

Result:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this✝ : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
this : j = k.castSucc
⊢ (if h : ↑k.castSucc < n then cast ⋯ (q (k.castSucc.castLT h)) else cast ⋯ b) = snoc (cons a q) b k.succ.castSucc

Proof state:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Tactic:
rw [h]

Result:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : i = 0
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0

Proof state:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) = snoc (cons a q) b

Tactic:
ext i

Result:
case h
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Proof state:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Tactic:
rw [this, cons_succ]

Result:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
⊢ snoc q b j = snoc (cons a q) b j.succ

Proof state:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
⊢ j = k.castSucc

Tactic:
rw [jk, castSucc_castLT]

Result:
no goals

Proof state:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Tactic:
set j := pred i h with ji

Result:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Proof state:
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
⊢ i = j.succ

Tactic:
rw [ji, succ_pred]

Result:
no goals

Proof state:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
⊢ snoc q b j = snoc (cons a q) b j.succ

Tactic:
have : j = castSucc k := by rw [jk, castSucc_castLT]

Result:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this✝ : i = j.succ
h' : ↑j < n
k : Fin n := j.castLT h'
jk : k = j.castLT h'
this : j = k.castSucc
⊢ snoc q b j = snoc (cons a q) b j.succ

Proof state:
case neg
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : ¬i = 0
j : Fin (n + 1) := i.pred h
ji : j = i.pred h
this : i = j.succ
h' : ¬↑j < n
⊢ snoc q b (last n) = snoc (cons a q) b (last n.succ)

Tactic:
simp

Result:
no goals

Proof state:
case pos
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
h : i = 0
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0

Tactic:
simp [snoc, castLT]

Result:
no goals