-- Mathlib/Data/Fin/VecNotation.lean
theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) :
    vecAlt1 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ (n + n) + 1)

Proof state:
case h.zero.mk
α : Type u
v : Fin (0 + 1) → α
hi : 0 < 0 + 1
⊢ (if h : ↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨0, hi⟩ + ⟨0, hi⟩ + 1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
v : Fin (n + 1) → α
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 => n_1 + n_1 + 1

Tactic:
ext i

Result:
case h
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 => n_1 + n_1 + 1) i

Proof state:
case h
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 => n_1 + n_1 + 1) i

Tactic:
simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]

Result:
case h
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1), ⋯⟩) = v (i + i + 1)

Proof state:
case h.zero.mk
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi : i < 0 + 1
⊢ (if h : ↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi⟩ + ⟨i, hi⟩ + 1)

Tactic:
simp only [Nat.zero_add, Nat.lt_one_iff] at hi

Result:
case h.zero.mk
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi✝ : i < 0 + 1
hi : i = 0
⊢ (if h : ↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi✝⟩ + ⟨i, hi✝⟩ + 1)

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = (↑i + ↑i + 1 - (n + 1 + 1)) % (n + 1 + 1)

Tactic:
refine (Nat.mod_eq_of_lt ?_).symm

Result:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) < n + 1 + 1

Proof state:
case pos.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
simp [Nat.mod_eq_of_lt, h]

Result:
no goals

Proof state:
case h.zero
α : Type u
v : Fin (0 + 1) → α
i : Fin (0 + 1)
⊢ (if h : ↑i + ↑i + 1 < 0 + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (0 + 1), ⋯⟩) = v (i + i + 1)

Tactic:
obtain ⟨i, hi⟩ := i

Result:
case h.zero.mk
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi : i < 0 + 1
⊢ (if h : ↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi⟩ + ↑⟨i, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi⟩ + ⟨i, hi⟩ + 1)

Proof state:
case h.zero.mk
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi✝ : i < 0 + 1
hi : i = 0
⊢ (if h : ↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi✝⟩ + ⟨i, hi✝⟩ + 1)

Tactic:
subst i

Result:
case h.zero.mk
α : Type u
v : Fin (0 + 1) → α
hi : 0 < 0 + 1
⊢ (if h : ↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨0, hi⟩ + ⟨0, hi⟩ + 1)

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one,
  Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by omega)]

Result:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = (↑i + ↑i + 1 - (n + 1 + 1)) % (n + 1 + 1)

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) < n + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
rw [Fin.val_mk, not_lt] at h

Result:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Proof state:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ 1 < n + 2

Tactic:
omega

Result:
no goals

Proof state:
case h.succ
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
⊢ (if h : ↑i + ↑i + 1 < n + 1 + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1 + 1), ⋯⟩) = v (i + i + 1)

Tactic:
split_ifs with h <;> congr

Result:
case pos.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)