case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i : Fin n
y : α (↑castSucc i)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) = snoc (cons a q) b
ext i
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i

case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i
case h
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i
by_cases h : i = 0
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
⊢ cons a (snoc q b) i = snoc (cons a q) b i
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i
set j := pred i h with ji
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
⊢ cons a (snoc q b) i = snoc (cons a q) b i
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
⊢ cons a (snoc q b) i = snoc (cons a q) b i
have : i = j.succ := by rw [ji, succ_pred]
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
⊢ snoc q b j = snoc (cons a q) b (succ j)
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
⊢ cons a (snoc q b) i = snoc (cons a q) b i
rw [this, cons_succ]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
⊢ snoc q b j = snoc (cons a q) b (succ j)

case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ¬↑j < n
⊢ snoc q b j = snoc (cons a q) b (succ j)
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
⊢ snoc q b j = snoc (cons a q) b (succ j)
by_cases h' : j.val < n
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ¬↑j < n
⊢ snoc q b (last n) = snoc (cons a q) b (last (Nat.succ n))
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ¬↑j < n
⊢ snoc q b j = snoc (cons a q) b (succ j)
rw [eq_last_of_not_lt h', succ_last]
no goals
case neg
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ¬↑j < n
⊢ snoc q b (last n) = snoc (cons a q) b (last (Nat.succ n))
simp
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : i = 0
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : i = 0
⊢ cons a (snoc q b) i = snoc (cons a q) b i
rw [h]
no goals
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : i = 0
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0
simp [snoc, castLT]
no goals
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
⊢ i = succ j
rw [ji, succ_pred]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
⊢ snoc q b j = snoc (cons a q) b (succ j)
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
⊢ snoc q b j = snoc (cons a q) b (succ j)
set k := castLT j h' with jk
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = ↑castSucc k
⊢ snoc q b j = snoc (cons a q) b (succ j)
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
⊢ snoc q b j = snoc (cons a q) b (succ j)
have : j = castSucc k := by rw [jk, castSucc_castLT]
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = ↑castSucc k
⊢ (if h : ↑(↑castSucc k) < n then
      _root_.cast (_ : (fun x => β) (succ (↑castSucc (castLT (↑castSucc k) h))) = (fun x => β) (succ (↑castSucc k)))
        (q (castLT (↑castSucc k) h))
    else _root_.cast (_ : (fun x => β) (succ (last n)) = (fun x => β) (succ (↑castSucc k))) b) =
    snoc (cons a q) b (↑castSucc (succ k))
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = ↑castSucc k
⊢ snoc q b j = snoc (cons a q) b (succ j)
rw [this, ← castSucc_fin_succ, snoc]
no goals
case pos
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this✝ : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
this : j = ↑castSucc k
⊢ (if h : ↑(↑castSucc k) < n then
      _root_.cast (_ : (fun x => β) (succ (↑castSucc (castLT (↑castSucc k) h))) = (fun x => β) (succ (↑castSucc k)))
        (q (castLT (↑castSucc k) h))
    else _root_.cast (_ : (fun x => β) (succ (last n)) = (fun x => β) (succ (↑castSucc k))) b) =
    snoc (cons a q) b (↑castSucc (succ k))
simp [pred, snoc, cons]
no goals
m n : ℕ
α : Fin (n + 1) → Type u
x : α (last n)
q✝ : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (↑castSucc i)
i✝ : Fin n
y : α (↑castSucc i✝)
z : α (last n)
β : Type u_1
a : β
q : Fin n → β
b : β
i : Fin (Nat.succ n + 1)
h : ¬i = 0
j : Fin (n + 1) := pred i h
ji : j = pred i h
this : i = succ j
h' : ↑j < n
k : Fin n := castLT j h'
jk : k = castLT j h'
⊢ j = ↑castSucc k
rw [jk, castSucc_castLT]