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)
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) (↑castSucc i) y j
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)
⊢ snoc (update p i y) x = update (snoc p x) (↑castSucc i) y
ext 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)
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (update p i y) x j = update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x j = update (snoc p x) (↑castSucc i) y j
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)
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) (↑castSucc i) y j
by_cases h : j.val < n
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)
j : Fin (n + 1)
h : ↑j < n
⊢ (if h : ↑j < n then _root_.cast (_ : α (↑castSucc (castLT j h)) = α j) (update p i y (castLT j h))
    else _root_.cast (_ : α (last n) = α j) x) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (update p i y) x j = update (snoc p x) (↑castSucc i) y j
rw [snoc]
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)
j : Fin (n + 1)
h : ↑j < n
⊢ (if h_1 : True then
      _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n)))
    else _root_.cast (_ : α (last n) = α j) x) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
⊢ (if h : ↑j < n then _root_.cast (_ : α (↑castSucc (castLT j h)) = α j) (update p i y (castLT j h))
    else _root_.cast (_ : α (last n) = α j) x) =
    update (snoc p x) (↑castSucc i) y j
simp only [h]
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)
j : Fin (n + 1)
h : ↑j < n
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
⊢ (if h_1 : True then
      _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n)))
    else _root_.cast (_ : α (last n) = α j) x) =
    update (snoc p x) (↑castSucc i) y j
simp only [dif_pos]
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y j
by_cases h' : j = castSucc 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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y j
have C1 : α (castSucc i) = α j := by rw [h']
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y j
have C2 : α (castSucc i) = α (castSucc (castLT j h)) := by rw [castSucc_castLT, h']
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
E2 : update p i y (castLT j h) = _root_.cast C2 y
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (_root_.cast C2 y) = _root_.cast C1 y
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
E2 : update p i y (castLT j h) = _root_.cast C2 y
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y j
rw [E1, E2]
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
E2 : update p i y (castLT j h) = _root_.cast C2 y
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (_root_.cast C2 y) = _root_.cast C1 y
exact eq_rec_compose (Eq.trans C2.symm C1) C2 y
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
⊢ α (↑castSucc i) = α j
rw [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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
⊢ update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
⊢ update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
have : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y := by simp
case h.e'_2.h.e'_5
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
⊢ ↑castSucc i = j

case h.e'_2.h.e'_6
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
e_5✝ : ↑castSucc i = j
⊢ HEq y (_root_.cast C1 y)
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
⊢ update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
convert this
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
⊢ update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
simp
no goals
case h.e'_2.h.e'_5
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
⊢ ↑castSucc i = j
exact h'.symm
no goals
case h.e'_2.h.e'_6
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
this : update (snoc p x) j (_root_.cast C1 y) j = _root_.cast C1 y
e_5✝ : ↑castSucc i = j
⊢ HEq y (_root_.cast C1 y)
exact heq_of_cast_eq (congr_arg α (Eq.symm h')) rfl
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
⊢ α (↑castSucc i) = α (↑castSucc (castLT j h))
rw [castSucc_castLT, 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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
⊢ update p i y (castLT j h) = _root_.cast C2 y
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
⊢ update p i y (castLT j h) = _root_.cast C2 y
have : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y := by simp
case h.e'_2.h.e'_5
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
⊢ i = castLT j h

case h.e'_2.h.e'_6
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
e_5✝ : i = castLT j h
⊢ HEq y (_root_.cast C2 y)
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
⊢ update p i y (castLT j h) = _root_.cast C2 y
convert this
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
⊢ update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
simp
no goals
case h.e'_2.h.e'_5
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
⊢ i = castLT j h
simp [h, h']
no goals
case h.e'_2.h.e'_6
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)
j : Fin (n + 1)
h : ↑j < n
h' : j = ↑castSucc i
C1 : α (↑castSucc i) = α j
E1 : update (snoc p x) (↑castSucc i) y j = _root_.cast C1 y
C2 : α (↑castSucc i) = α (↑castSucc (castLT j h))
this : update p (castLT j h) (_root_.cast C2 y) (castLT j h) = _root_.cast C2 y
e_5✝ : i = castLT j h
⊢ HEq y (_root_.cast C2 y)
exact heq_of_cast_eq C2 rfl
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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
this : ¬castLT j h = i
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y 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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y j
have : ¬castLT j h = i := by
  intro E
  apply h'
  rw [← E, castSucc_castLT]
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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
this : ¬castLT j h = i
⊢ _root_.cast (_ : α (↑castSucc (castLT j (_ : ↑j < n))) = α j) (update p i y (castLT j (_ : ↑j < n))) =
    update (snoc p x) (↑castSucc i) y j
simp [h', this, snoc, 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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
E : castLT j h = i
⊢ False
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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
⊢ ¬castLT j h = i
intro E
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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
E : castLT j h = i
⊢ j = ↑castSucc 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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
E : castLT j h = i
⊢ False
apply h'
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)
j : Fin (n + 1)
h : ↑j < n
h' : ¬j = ↑castSucc i
E : castLT j h = i
⊢ j = ↑castSucc i
rw [← E, castSucc_castLT]
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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x (last n) = update (snoc p x) (↑castSucc i) y (last 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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x j = update (snoc p x) (↑castSucc i) y j
rw [eq_last_of_not_lt h]
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)
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (update p i y) x (last n) = update (snoc p x) (↑castSucc i) y (last n)
simp [Ne.symm (ne_of_lt (castSucc_lt_last i))]