awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h_1 : (↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) < m + 1
h : i < m
⊢ vecCons x u (⟨(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ), h_1⟩ : Fin (m + 1)) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
      (⟨i + 1, hi⟩ : Fin (o + 1))

Tactic:
simp [h]
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ¬(↑i : ℕ) < m + 1
neg :
  ∀ (hi : 0 < o + 1) (h : ¬(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) < m + 1),
    v (⟨(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) - (m + 1), ⋯⟩ : Fin n) =
      vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
        (⟨0, hi⟩ : Fin (o + 1))
neg₁ :
  ∀ (i : ℕ) (hi : i + 1 < o + 1) (h : ¬(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) < m + 1),
    v (⟨(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) - (m + 1), ⋯⟩ : Fin n) =
      vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
        (⟨i + 1, hi⟩ : Fin (o + 1))
⊢ v (⟨(↑i : ℕ) - (m + 1), ⋯⟩ : Fin n) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : 0 < o + 1
h : ¬(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) < m + 1
⊢ v (⟨(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) - (m + 1), ⋯⟩ : Fin n) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
      (⟨0, hi⟩ : Fin (o + 1))

Tactic:
simp at h
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h : ¬(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) < m + 1
⊢ m ≤ i

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

Premises used: Nat.add_le_add_iff_right, Fin.val_mk, not_lt
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h_1 : ¬(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) < m + 1
h : m ≤ i
⊢ v (⟨(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) - (m + 1), ⋯⟩ : Fin n) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
      (⟨i + 1, hi⟩ : Fin (o + 1))

Tactic:
simp [not_lt.2 h]

Premises used: Iff.mpr, not_lt
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
hm : m = n + n
v : Fin m → α
k : Fin n
⊢ (↑k : ℕ) + (↑k : ℕ) < m

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
h : ∀ (i : Fin n), vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun (n_1 : Fin n) ↦ n_1 + n_1) i
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin n) ↦ n_1 + n_1

Tactic:
ext i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : (if h : (↑i : ℕ) + (↑i : ℕ) < n then v ⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ else v ⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩) = v (i + i)
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun (n_1 : Fin n) ↦ n_1 + n_1) i

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

Premises used: Function.comp, Matrix.vecAlt0, Matrix.vecAppend_eq_ite
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
pos : ∀ (h : (↑i : ℕ) + (↑i : ℕ) < n), v (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin n) = v (i + i)
neg : ∀ (h : ¬(↑i : ℕ) + (↑i : ℕ) < n), v (⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩ : Fin n) = v (i + i)
⊢ (if h : (↑i : ℕ) + (↑i : ℕ) < n then v ⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ else v ⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩) = v (i + i)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : (↑i : ℕ) + (↑i : ℕ) < n
pos : (↑i : ℕ) + (↑i : ℕ) = ((↑i : ℕ) + (↑i : ℕ)) % n
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin n) = v (i + i)

Tactic:
congr
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬(↑i : ℕ) + (↑i : ℕ) < n
neg : (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ)) % n
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩ : Fin n) = v (i + i)

Tactic:
congr
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : (↑i : ℕ) + (↑i : ℕ) < n
⊢ (↑i : ℕ) + (↑i : ℕ) < n

Tactic:
rw [Fin.val_mk] at h

Premises used: Fin.val_mk
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : (↑i : ℕ) + (↑i : ℕ) < n
⊢ (↑i : ℕ) + (↑i : ℕ) = ((↑i : ℕ) + (↑i : ℕ)) % n

Tactic:
(Nat.mod_eq_of_lt h).symm

Premises used: Nat.mod_eq_of_lt, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : (↑i : ℕ) + (↑i : ℕ) < n
⊢ (↑i : ℕ) + (↑i : ℕ) = ((↑i : ℕ) + (↑i : ℕ)) % n

Tactic:
exact (Nat.mod_eq_of_lt h).symm

Premises used: Nat.mod_eq_of_lt, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬(↑i : ℕ) + (↑i : ℕ) < n
⊢ n ≤ (↑i : ℕ) + (↑i : ℕ)

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

Premises used: Fin.val_mk, not_lt
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ (↑i : ℕ) + (↑i : ℕ)
neg : (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ) - n) % n
⊢ (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ)) % n

Tactic:
simp only [Nat.mod_eq_sub_mod h]

Premises used: Nat.mod_eq_sub_mod
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ (↑i : ℕ) + (↑i : ℕ)
⊢ (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ) - n) % n

Tactic:
(Nat.mod_eq_of_lt ?_).symm

Premises used: Nat.mod_eq_of_lt, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ (↑i : ℕ) + (↑i : ℕ)
neg : (↑i : ℕ) + (↑i : ℕ) - n < n
⊢ (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ) - n) % n

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

Premises used: Nat.mod_eq_of_lt, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ (↑i : ℕ) + (↑i : ℕ)
⊢ (↑i : ℕ) + (↑i : ℕ) - n < n

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1) → α
h : ∀ (i : Fin (n + 1)), vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1

Tactic:
ext i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
h :
  (if h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 then v ⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩
    else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1), ⋯⟩) =
    v (i + i + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i

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

Premises used: Matrix.vecAlt1, Function.comp, Matrix.vecAppend_eq_ite
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h :
  ∀ (i : ℕ) (hi : i < HAdd.hAdd (α := ℕ) 0 1),
    (if h :
          (↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 <
            HAdd.hAdd (α := ℕ) 0 1 then
        v ⟨(↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1, ⋯⟩
      else
        v
          ⟨(↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 -
              HAdd.hAdd (α := ℕ) 0 1,
            ⋯⟩) =
      v ((⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + (⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + 1)
⊢ (if h : (↑i : ℕ) + (↑i : ℕ) + 1 < HAdd.hAdd (α := ℕ) 0 1 then v ⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩
    else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) =
    v (i + i + 1)

Tactic:
obtain ⟨i, hi⟩ := i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
i : ℕ
hi : i < HAdd.hAdd (α := ℕ) 0 1
⊢ i = 0

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

Premises used: Nat.lt_one_iff, Nat.zero_add
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
i : ℕ
hi_1 : i < HAdd.hAdd (α := ℕ) 0 1
hi : i = 0
h :
  ∀ (hi : 0 < HAdd.hAdd (α := ℕ) 0 1),
    (if h :
          (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 <
            HAdd.hAdd (α := ℕ) 0 1 then
        v ⟨(↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1, ⋯⟩
      else
        v
          ⟨(↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 -
              HAdd.hAdd (α := ℕ) 0 1,
            ⋯⟩) =
      v ((⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + (⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + 1)
⊢ (if h :
        (↑(⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 <
          HAdd.hAdd (α := ℕ) 0 1 then
      v ⟨(↑(⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1, ⋯⟩
    else
      v
        ⟨(↑(⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 -
            HAdd.hAdd (α := ℕ) 0 1,
          ⋯⟩) =
    v ((⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + (⟨i, hi_1⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + 1)

Tactic:
subst i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
hi : 0 < HAdd.hAdd (α := ℕ) 0 1
⊢ (if h :
        (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 <
          HAdd.hAdd (α := ℕ) 0 1 then
      v ⟨(↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1, ⋯⟩
    else
      v
        ⟨(↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 -
            HAdd.hAdd (α := ℕ) 0 1,
          ⋯⟩) =
    v ((⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + (⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
pos : ∀ (h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1), v (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (n + 1 + 1)) = v (i + i + 1)
neg :
  ∀ (h : ¬(↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1),
    v (⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1), ⋯⟩ : Fin (n + 1 + 1)) = v (i + i + 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
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1
pos : (↑i : ℕ) + (↑i : ℕ) + 1 = (((↑i : ℕ) + (↑i : ℕ)) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (n + 1 + 1)) = v (i + i + 1)

Tactic:
congr
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬(↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1
neg : (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) = (((↑i : ℕ) + (↑i : ℕ)) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1), ⋯⟩ : Fin (n + 1 + 1)) = v (i + i + 1)

Tactic:
congr
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : 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]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬(↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1
⊢ n + 1 + 1 ≤ (↑i : ℕ) + (↑i : ℕ) + 1

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

Premises used: Fin.val_mk, not_lt
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ (↑i : ℕ) + (↑i : ℕ) + 1
⊢ 1 < n + 2

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ (↑i : ℕ) + (↑i : ℕ) + 1
neg : (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) = ((↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1)) % (n + 1 + 1)
⊢ (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) = (((↑i : ℕ) + (↑i : ℕ)) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]

Premises used: Nat.mod_eq_of_lt, Nat.mod_add_mod, Nat.mod_eq_sub_mod
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : 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:
(Nat.mod_eq_of_lt ?_).symm

Premises used: Nat.mod_eq_of_lt, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ (↑i : ℕ) + (↑i : ℕ) + 1
neg : (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) < n + 1 + 1
⊢ (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) = ((↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1)) % (n + 1 + 1)

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

Premises used: Nat.mod_eq_of_lt, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : 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
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
h :
  ∀ (v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α) (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    (if h : (↑i : ℕ) + (↑i : ℕ) + 1 < HAdd.hAdd (α := ℕ) 0 1 then v ⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩
      else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) =
      v (i + i + 1)
h₁ :
  ∀ (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)
⊢ (if h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 then v ⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩
    else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1), ⋯⟩) =
    v (i + i + 1)

Tactic:
cases n with
  | zero =>
    obtain ⟨i, hi⟩ := i
    simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl
  | succ n =>
    split_ifs with h <;> congr
    · simp [Nat.mod_eq_of_lt, h]
    · rw [Fin.val_mk, not_lt] at h
      simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]
      refine (Nat.mod_eq_of_lt ?_).symm
      #adaptation_note /-- After leanprover/lean4#13166, the `lia` tactic was timing out here. -/
      omega

Premises used: Fin.val_mk, Nat.mod_eq_of_lt, Nat.mod_add_mod, not_lt, Nat.lt_one_iff, Nat.zero_add, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
hm : m + 2 = n + 1 + (n + 1)
v : Fin (m + 2) → α
⊢ vecHead (vecAlt0 hm v) = v 0

Tactic:
rfl

Premises used: Fin.ofNat, Matrix.vecHead, Nat.mod, Matrix.vecAlt0, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
hm : m + 2 = n + 1 + (n + 1)
v : Fin (m + 2) → α
⊢ vecHead (vecAlt1 hm v) = v 1

Tactic:
simp [vecHead, vecAlt1]

Premises used: Matrix.vecAlt1, Matrix.vecHead
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
rw : vecCons x u (i + i) = (vecCons x u ∘ fun (n_1 : Fin n.succ) ↦ n_1 + n_1) i
⊢ vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
rw [vecAlt0_vecAppend]

Premises used: Matrix.vecAlt0_vecAppend
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = (vecCons x u ∘ fun (n_1 : Fin n.succ) ↦ n_1 + n_1) i

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
rw : vecCons x u (i + i + 1) = (vecCons x u ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i
⊢ vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
rw [vecAlt1_vecAppend]

Premises used: Matrix.vecAlt1_vecAppend
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
h₁ : ∀ (i : Fin (n + 1)), vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
h₁ : vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (m + 1 + 1)) = vecCons x (vecAlt0 ⋯ u) i
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i

Tactic:
simp_rw [vecAlt0]

Premises used: Matrix.vecAlt0
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
h₁ :
  ∀ (hi : 0 < n + 1),
    vecCons x (vecCons y u) (⟨(↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ), ⋯⟩ : Fin (m + 1 + 1)) =
      vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩
h₂ :
  ∀ (i : ℕ) (hi : i + 1 < n + 1),
    vecCons x (vecCons y u)
        (⟨(↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ), ⋯⟩ : Fin (m + 1 + 1)) =
      vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩
⊢ vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (m + 1 + 1)) = vecCons x (vecAlt0 ⋯ u) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) (⟨(↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ), ⋯⟩ : Fin (m + 1 + 1)) =
    vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u)
      (⟨(↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ), ⋯⟩ : Fin (m + 1 + 1)) =
    vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Tactic:
simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
      vecAlt0]

Premises used: Matrix.cons_val_succ', Nat.add_assoc, Matrix.vecAlt0, Nat.add_right_comm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u_1
h : 0 = HAdd.hAdd (α := ℕ) 0 0
⊢ Eq.{u_1 + 1} (α := (k : Fin 0) → α) (vecAlt0 h ![]) ![]

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
h₁ : ∀ (i : Fin (n + 1)), vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
h₁ : vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) = vecCons y (vecAlt1 ⋯ u) i
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i

Tactic:
simp_rw [vecAlt1]

Premises used: Matrix.vecAlt1
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
h₁ :
  ∀ (hi : 0 < n + 1),
    vecCons x (vecCons y u)
        (⟨(↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) =
      vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩
h₂ :
  ∀ (i : ℕ) (hi : i + 1 < n + 1),
    vecCons x (vecCons y u)
        (⟨(↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) =
      vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩
⊢ vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) = vecCons y (vecAlt1 ⋯ u) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) (⟨(↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) =
    vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u)
      (⟨(↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) =
    vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩

Tactic:
simp [vecAlt1, Nat.add_right_comm, ← Nat.add_assoc]

Premises used: Matrix.vecAlt1, Nat.add_assoc, Nat.add_right_comm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u_1
h : 0 = HAdd.hAdd (α := ℕ) 0 0
⊢ Eq.{u_1 + 1} (α := (k : Fin 0) → α) (vecAlt1 h ![]) ![]

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
x : α
⊢ (fun (x_1 : Fin 1) ↦ x) = ![x]

Tactic:
(cons_fin_one x _).symm

Premises used: Matrix.cons_fin_one, Eq.symm
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
h :
  ∀ (j : Fin n.succ.succ),
    (vecCons a (vecCons b x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ)) j =
      vecCons b (vecCons a x) j
⊢ vecCons a (vecCons b x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ) = vecCons b (vecCons a x)

Tactic:
ext j : 1
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
⊢ Function.comp (α := Fin n.succ.succ) (vecCons a (vecCons b x))
      (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ) 0 =
    vecCons b (vecCons a x) 0

Tactic:
simp
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
⊢ Function.comp (α := Fin n.succ.succ) (vecCons a (vecCons b x))
      (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ) 1 =
    vecCons b (vecCons a x) 1

Tactic:
simp
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ i < n

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ (⟨i + 2, h⟩ : Fin n.succ.succ) = ⟨i, ⋯⟩.succ.succ

Tactic:
grind
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ (⟨i + 2, h⟩ : Fin n.succ.succ) = ⟨i, ⋯⟩.succ.succ

Tactic:
have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = Fin.succ (Fin.succ ⟨i, by lia⟩) := by grind
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = ⟨i, ⋯⟩.succ.succ
⊢ (vecCons a (vecCons b x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ))
      (⟨i + 2, h⟩ : Fin n.succ.succ) =
    vecCons b (vecCons a x) ⟨i + 2, h⟩

Tactic:
simp only [Nat.succ_eq_add_one, h', Function.comp_apply,
      Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero _) (Fin.succ_succ_ne_one _), cons_val_succ]

Premises used: Nat.succ_eq_add_one, Matrix.cons_val_succ, Equiv.swap_apply_of_ne_of_ne, Fin.succ_ne_zero, Fin.succ_succ_ne_one, Function.comp_apply
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
⊢ (vecCons a (vecCons b x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ)) j =
    vecCons b (vecCons a x) j

Tactic:
match j with
  | 0 => simp
  | 1 => simp
  | ⟨i + 2, h⟩ =>
    have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = Fin.succ (Fin.succ ⟨i, by lia⟩) := by grind
    simp only [Nat.succ_eq_add_one, h', Function.comp_apply,
      Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero _) (Fin.succ_succ_ne_one _), cons_val_succ]