case h
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) i = (v ∘ bit0) i
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) = v ∘ bit0
ext i
case h
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v { val := ↑i + ↑i, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } < n) }
    else v { val := ↑i + ↑i - n, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } - n < n) }) =
    v (i + i)
case h
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
⊢ vecAlt0 (_ : n + n = n + n) (vecAppend (_ : n + n = n + n) v v) i = (v ∘ bit0) i
simp_rw [Function.comp, bit0, vecAlt0, vecAppend_eq_ite]
case h.inl.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n

case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
case h
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v { val := ↑i + ↑i, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } < n) }
    else v { val := ↑i + ↑i - n, isLt := (_ : ↑{ val := ↑i + ↑i, isLt := (_ : ↑i + ↑i < n + n) } - n < n) }) =
    v (i + i)
split_ifs with h <;> congr
case h.inl.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
case h.inl.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
rw [Fin.val_mk] at h
case h.inl.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
case h.inl.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk]
no goals
case h.inl.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n
exact (Nat.mod_eq_of_lt h).symm
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
rw [Fin.val_mk, not_lt] at h
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i - n) % n
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_eq_sub_mod h]
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i - n) % n
refine' (Nat.mod_eq_of_lt _).symm
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i < n + n
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n
rw [tsub_lt_iff_left h]
no goals
case h.inr.e_a.e_val
α : Type u
m n o : ℕ
m' : Type ?u.38823
n' : Type ?u.38826
o' : Type ?u.38829
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i < n + n
exact add_lt_add i.2 i.2