no goals
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n
rwa [add_assoc n, add_comm 1, ← add_assoc, ← add_assoc, add_right_cancel_iff,
  add_right_cancel_iff] at h
case h
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 (_ : m = n + n) u) i
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (_ : m = n + n) u)
ext i
case h
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) { val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) i
case h
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 (_ : m = n + n) u) i
simp_rw [vecAlt0]
case h.mk.zero
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : Nat.zero < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi },
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.zero, isLt := hi }

case h.mk.succ
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : Nat.succ i < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi },
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.succ i, isLt := hi }
case h
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) { val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) i
rcases i with ⟨⟨⟩ | i, hi⟩
no goals
case h.mk.zero
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : Nat.zero < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi },
        isLt := (_ : ↑{ val := Nat.zero, isLt := hi } + ↑{ val := Nat.zero, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.zero, isLt := hi }
rfl
no goals
case h.mk.succ
α : Type u
m n o : ℕ
m' : Type ?u.50198
n' : Type ?u.50201
o' : Type ?u.50204
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : Nat.succ i < n + 1
⊢ vecCons x (vecCons y u)
      { val := ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi },
        isLt := (_ : ↑{ val := Nat.succ i, isLt := hi } + ↑{ val := Nat.succ i, isLt := hi } < m + 1 + 1) } =
    vecCons x (fun k => u { val := ↑k + ↑k, isLt := (_ : ↑k + ↑k < m) }) { val := Nat.succ i, isLt := hi }
simp [vecAlt0, Nat.add_succ, Nat.succ_add]