awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
Goal:
α : Type u
v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
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)
have hi₁ : i = 0
Tactic: simp only [Nat.zero_add, Nat.lt_one_iff] at hi
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
v : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
i : ℕ
hi_1 : i < HAdd.hAdd (α := ℕ) 0 1
hi : i = 0
⊢ (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)
have 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, sorry⟩
    else
      v
        ⟨(↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 -
            HAdd.hAdd (α := ℕ) 0 1,
          sorry⟩) =
    v ((⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + (⟨0, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + 1)
Tactic: subst i
Cleared hypotheses: i, hi_1, hi
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : 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)
have pos : ∀ (h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1), v (⟨(↑i : ℕ) + (↑i : ℕ) + 1, sorry⟩ : Fin (n + 1 + 1)) = v (i + i + 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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)
⊢ (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)
have neg : ∀ (h : ¬(↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1),
  v (⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1), sorry⟩ : Fin (n + 1 + 1)) = v (i + i + 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (n + 1 + 1)) = v (i + i + 1)
have pos : (↑i : ℕ) + (↑i : ℕ) + 1 = (((↑i : ℕ) + (↑i : ℕ)) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬(↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 + 1
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1), ⋯⟩ : Fin (n + 1 + 1)) = v (i + i + 1)
have neg : (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) = (((↑i : ℕ) + (↑i : ℕ)) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
Goal:
α : 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)
have h₁ : n + 1 + 1 ≤ (↑i : ℕ) + (↑i : ℕ) + 1
Tactic: rw [Fin.val_mk, not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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 : ℕ)) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
have neg : (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) = ((↑i : ℕ) + (↑i : ℕ) + 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)]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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)
have neg : (↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1) < n + 1 + 1
Tactic: refine (Nat.mod_eq_of_lt ?_).symm
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : 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)
have 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, sorry⟩
    else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - HAdd.hAdd (α := ℕ) 0 1, sorry⟩) =
    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
Cleared hypotheses: n, v, i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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)
⊢ (if h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 then v ⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩
    else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1), ⋯⟩) =
    v (i + i + 1)
have 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, sorry⟩
    else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1 + 1), sorry⟩) =
    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
Cleared hypotheses: n, v, i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i
have rw : vecCons x u (i + i) = (vecCons x u ∘ fun (n_1 : Fin n.succ) ↦ n_1 + n_1) i
Tactic: rw [vecAlt0_vecAppend]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i
have rw : vecCons x u (i + i + 1) = (vecCons x u ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i
Tactic: rw [vecAlt1_vecAppend]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)
have h₁ : ∀ (i : Fin (n + 1)), vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 sorry u) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n : ℕ
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 ⋯ u) i
have h₁ : vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ), sorry⟩ : Fin (m + 1 + 1)) = vecCons x (vecAlt0 sorry u) i
Tactic: simp_rw [vecAlt0]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (m + 1 + 1)) = vecCons x (vecAlt0 ⋯ u) i
have h₁ : ∀ (hi : 0 < n + 1),
  vecCons x (vecCons y u) (⟨(↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ), sorry⟩ : Fin (m + 1 + 1)) =
    vecCons x (vecAlt0 sorry u) ⟨0, hi⟩
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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⟩
⊢ vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin (m + 1 + 1)) = vecCons x (vecAlt0 ⋯ u) i
have h₂ : ∀ (i : ℕ) (hi : i + 1 < n + 1),
  vecCons x (vecCons y u)
      (⟨(↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨i + 1, hi⟩ : Fin (n + 1)) : ℕ), sorry⟩ : Fin (m + 1 + 1)) =
    vecCons x (vecAlt0 sorry u) ⟨i + 1, hi⟩
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)
have h₁ : ∀ (i : Fin (n + 1)), vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 sorry u) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i
have h₁ : vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ) + 1, sorry⟩ : Fin (m + 1 + 1)) = vecCons y (vecAlt1 sorry u) i
Tactic: simp_rw [vecAlt1]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) = vecCons y (vecAlt1 ⋯ u) i
have h₁ : ∀ (hi : 0 < n + 1),
  vecCons x (vecCons y u) (⟨(↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + (↑(⟨0, hi⟩ : Fin (n + 1)) : ℕ) + 1, sorry⟩ : Fin (m + 1 + 1)) =
    vecCons y (vecAlt1 sorry u) ⟨0, hi⟩
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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⟩
⊢ vecCons x (vecCons y u) (⟨(↑i : ℕ) + (↑i : ℕ) + 1, ⋯⟩ : Fin (m + 1 + 1)) = vecCons y (vecAlt1 ⋯ u) i
have 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, sorry⟩ : Fin (m + 1 + 1)) =
    vecCons y (vecAlt1 sorry u) ⟨i + 1, hi⟩
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
⊢ vecCons a (vecCons b x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ) = vecCons b (vecCons a x)
have 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
Tactic: ext j : 1
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
Goal:
α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.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⟩
have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = ⟨i, sorry⟩.succ.succ
Tactic: have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = Fin.succ (Fin.succ ⟨i, by lia⟩) := by grind
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
⊢ Eq (α := Fin n.succ → α) (vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)))
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1)))
have h : ∀ (k : Fin n.succ),
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
Tactic: ext k : 1
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h : vecCons (n := n) a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) 0 =
  Function.comp (α := Fin (n + 1)) (vecCons a x) (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1)) 0
Tactic: rcases eq_or_ne k 0 with rfl | hk₀
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
h :
  vecCons (n := n) a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) 0 =
    Function.comp (α := Fin (n + 1)) (vecCons a x) (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1)) 0
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₁ : ∀ (hk₀ : k ≠ 0),
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
Tactic: rcases eq_or_ne k 0 with rfl | hk₀
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h : ∀ (hk₀ : i.succ ≠ 0),
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) i.succ =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) i.succ
Tactic: rcases eq_or_ne k i.succ with rfl | hki
Cleared hypotheses: k, hk₀
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
h :
  ∀ (hk₀ : i.succ ≠ 0),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) i.succ =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) i.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₁ : ∀ (hki : k ≠ i.succ),
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
Tactic: rcases eq_or_ne k i.succ with rfl | hki
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h : ∀ (hk₀ : j.succ ≠ 0) (hki : j.succ ≠ i.succ),
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) j.succ =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) j.succ
Tactic: rcases eq_or_ne k j.succ with rfl | hkj
Cleared hypotheses: k, hk₀, hki
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
h :
  ∀ (hk₀ : j.succ ≠ 0) (hki : j.succ ≠ i.succ),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) j.succ =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) j.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₁ : ∀ (hkj : k ≠ j.succ),
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
Tactic: rcases eq_or_ne k j.succ with rfl | hkj
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have hk : k = ⟨(↑k : ℕ) - 1, sorry⟩.succ
Tactic: have hk : k = Fin.succ ⟨k - 1, by lia⟩ := by grind
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
  vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₂ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, sorry⟩ : Fin n).succ =
  vecCons a x ⟨(↑k : ℕ) - 1, sorry⟩.succ
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
h₂ :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n).succ =
    vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₃ : (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, sorry⟩ : Fin n) = vecCons a x ⟨(↑k : ℕ) - 1, sorry⟩.succ
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
h₂ :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n).succ =
    vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₃ : (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₄ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, sorry⟩ : Fin n)) = vecCons a x ⟨(↑k : ℕ) - 1, sorry⟩.succ
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
h₂ :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n).succ =
    vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₃ : (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₄ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n)) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₅ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, sorry⟩ : Fin n)) = x ⟨(↑k : ℕ) - 1, sorry⟩
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]