awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ take (α := motive) (n + m) ⋯ (fun (i : Fin (n + n')) ↦ addCases (motive := fun (x : Fin (n + n')) ↦ motive x) u v i)
      i =
    addCases (motive := fun (x : Fin (n + m)) ↦ motive (castLE ⋯ x)) u
      (take (α := fun (i : Fin n') ↦ motive (natAdd n i)) m h v) i
have h₁ : Eq.{u_2} (α := motive (castLE sorry i))
  (if h_1 : (↑i : ℕ) < n then u ((castLE sorry i).castLT sorry)
  else
    @Eq.rec _ (natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry))
      (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry) = x) ↦ motive x)
      (v (subNat n (Fin.cast sorry (castLE sorry i)) sorry) : motive (natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry))) _ sorry)
  (if h : (↑i : ℕ) < n then u (i.castLT sorry)
  else
    @Eq.rec _ (natAdd n (subNat n (Fin.cast sorry i) sorry))
      (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast sorry i) sorry) = x) ↦ motive (castLE sorry x))
      (v (castLE h (subNat n (Fin.cast sorry i) sorry)) : motive (natAdd n (castLE h (subNat n (Fin.cast sorry i) sorry)))) _ sorry)
Tactic: simp only [take, addCases, val_castLE]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
⊢ Eq.{u_2} (α := motive (castLE ⋯ i))
    (if h_1 : (↑i : ℕ) < n then u ((castLE ⋯ i).castLT ⋯)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))
        (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) = x) ↦ motive x)
        (v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) : motive (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))) _ ⋯)
    (if h : (↑i : ℕ) < n then u (i.castLT ⋯)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ i) ⋯))
        (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast ⋯ i) ⋯) = x) ↦ motive (castLE ⋯ x))
        (v (castLE h (subNat n (Fin.cast ⋯ i) ⋯)) : motive (natAdd n (castLE h (subNat n (Fin.cast ⋯ i) ⋯)))) _ ⋯)
have pos : ∀ (h' : (↑i : ℕ) < n),
  Eq.{u_2} (α := motive (castLE sorry i))
    (if h_1 : (↑i : ℕ) < n then u ((castLE sorry i).castLT sorry)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry))
        (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry) = x) ↦ motive x)
        (v (subNat n (Fin.cast sorry (castLE sorry i)) sorry) : motive (natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry))) _ sorry)
    (if h : (↑i : ℕ) < n then u (i.castLT sorry)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast sorry i) sorry))
        (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast sorry i) sorry) = x) ↦ motive (castLE sorry x))
        (v (castLE h (subNat n (Fin.cast sorry i) sorry)) : motive (natAdd n (castLE h (subNat n (Fin.cast sorry i) sorry)))) _ sorry)
Tactic: by_cases h' : i < n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
pos :
  ∀ (h' : (↑i : ℕ) < n),
    Eq.{u_2} (α := motive (castLE ⋯ i))
      (if h_1 : (↑i : ℕ) < n then u ((castLE ⋯ i).castLT ⋯)
      else
        @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))
          (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) = x) ↦ motive x)
          (v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) : motive (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))) _ ⋯)
      (if h : (↑i : ℕ) < n then u (i.castLT ⋯)
      else
        @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ i) ⋯))
          (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast ⋯ i) ⋯) = x) ↦ motive (castLE ⋯ x))
          (v (castLE h (subNat n (Fin.cast ⋯ i) ⋯)) : motive (natAdd n (castLE h (subNat n (Fin.cast ⋯ i) ⋯)))) _ ⋯)
⊢ Eq.{u_2} (α := motive (castLE ⋯ i))
    (if h_1 : (↑i : ℕ) < n then u ((castLE ⋯ i).castLT ⋯)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))
        (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) = x) ↦ motive x)
        (v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) : motive (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))) _ ⋯)
    (if h : (↑i : ℕ) < n then u (i.castLT ⋯)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ i) ⋯))
        (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast ⋯ i) ⋯) = x) ↦ motive (castLE ⋯ x))
        (v (castLE h (subNat n (Fin.cast ⋯ i) ⋯)) : motive (natAdd n (castLE h (subNat n (Fin.cast ⋯ i) ⋯)))) _ ⋯)
have neg : ∀ (h' : ¬(↑i : ℕ) < n),
  Eq.{u_2} (α := motive (castLE sorry i))
    (if h_1 : (↑i : ℕ) < n then u ((castLE sorry i).castLT sorry)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry))
        (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry) = x) ↦ motive x)
        (v (subNat n (Fin.cast sorry (castLE sorry i)) sorry) : motive (natAdd n (subNat n (Fin.cast sorry (castLE sorry i)) sorry))) _ sorry)
    (if h : (↑i : ℕ) < n then u (i.castLT sorry)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast sorry i) sorry))
        (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast sorry i) sorry) = x) ↦ motive (castLE sorry x))
        (v (castLE h (subNat n (Fin.cast sorry i) sorry)) : motive (natAdd n (castLE h (subNat n (Fin.cast sorry i) sorry)))) _ sorry)
Tactic: by_cases h' : i < n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : (↑i : ℕ) < n
⊢ Eq.{u_2} (α := motive (castLE ⋯ i))
    (if h_1 : (↑i : ℕ) < n then u ((castLE ⋯ i).castLT ⋯)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))
        (fun (x : Fin (n + n')) (h : natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) = x) ↦ motive x)
        (v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯) : motive (natAdd n (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯))) _ ⋯)
    (if h : (↑i : ℕ) < n then u (i.castLT ⋯)
    else
      @Eq.rec _ (natAdd n (subNat n (Fin.cast ⋯ i) ⋯))
        (fun (x : Fin (n + m)) (h_1 : natAdd n (subNat n (Fin.cast ⋯ i) ⋯) = x) ↦ motive (castLE ⋯ x))
        (v (castLE h (subNat n (Fin.cast ⋯ i) ⋯)) : motive (natAdd n (castLE h (subNat n (Fin.cast ⋯ i) ⋯)))) _ ⋯)
have pos : Eq (α := motive (castLE sorry i)) (u ((castLE sorry i).castLT sorry) : motive (castAdd n' ((castLE sorry i).castLT sorry))) (u (i.castLT sorry))
Tactic: simp only [h', ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.take m l).get = take (α := fun (i : Fin l.length) ↦ α) m h l.get ∘ Fin.cast ⋯
have h₁ : ∀ (i : Fin (List.take m l).length),
  (List.take m l).get i = (take (α := fun (i : Fin l.length) ↦ α) m h l.get ∘ Fin.cast sorry) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).get = take (α := fun (i : Fin n) ↦ α) m h v ∘ Fin.cast ⋯
have h₁ : ∀ (i : Fin (List.take m (List.ofFn v)).length),
  (List.take m (List.ofFn v)).get i = (take (α := fun (i : Fin n) ↦ α) m h v ∘ Fin.cast sorry) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u_1
x : α
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x = ![x]
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x i = ![x] i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u_1
x : α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x i = ![x] i
have h : Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x 0 = ![x] 0
Tactic: cases Fin.fin_one_eq_zero i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u
have h : ∀ (x_1 : Fin m), vecTail (vecCons x u) x_1 = u x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x : α
u : Fin 0 → α
⊢ Set.range (vecCons x u) = {x}
have rw : {x} ∪ Set.range u = {x}
Tactic: rw [range_cons, range_empty, Set.union_empty]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x : α
u : Fin 0 → α
rw : {x} ∪ Set.range u = {x}
⊢ Set.range (vecCons x u) = {x}
have rw₁ : Eq (α := Set α) ({x} ∪ ∅) {x}
Tactic: rw [range_cons, range_empty, Set.union_empty]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x : α
u : Fin 0 → α
rw : {x} ∪ Set.range u = {x}
rw₁ : Eq (α := Set α) ({x} ∪ ∅) {x}
⊢ Set.range (vecCons x u) = {x}
have rw₂ : Eq (α := Set α) {x} {x}
Tactic: rw [range_cons, range_empty, Set.union_empty]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}
have rw : {x} ∪ Set.range (vecCons y u) = {x, y}
Tactic: rw [range_cons, range_cons_empty, Set.singleton_union]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x y : α
u : Fin 0 → α
rw : {x} ∪ Set.range (vecCons y u) = {x, y}
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}
have rw₁ : Eq (α := Set α) ({x} ∪ {y}) {x, y}
Tactic: rw [range_cons, range_cons_empty, Set.singleton_union]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x y : α
u : Fin 0 → α
rw : {x} ∪ Set.range (vecCons y u) = {x, y}
rw₁ : Eq (α := Set α) ({x} ∪ {y}) {x, y}
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}
have rw₂ : Eq (α := Set α) {x, y} {x, y}
Tactic: rw [range_cons, range_cons_empty, Set.singleton_union]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x
have rw : vecCons x u 0 = x
Tactic: rw [Fin.forall_fin_one]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho u v = fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩
have h : ∀ (i : Fin o), vecAppend ho u v i = if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩
have h : Eq.{u_1 + 1} (α := α)
  (if hi : (↑(Fin.cast ho i) : ℕ) < m then
    Eq.rec (motive := fun (x : Fin (m + n)) (h : Fin.castAdd n ((Fin.cast ho i).castLT hi) = x) ↦ α)
      (u ((Fin.cast ho i).castLT hi)) sorry
  else
    Eq.rec (motive := fun (x : Fin (m + n)) (h : Fin.natAdd m (Fin.subNat m (Fin.cast sorry (Fin.cast ho i)) sorry) = x) ↦ α)
      (v (Fin.subNat m (Fin.cast sorry (Fin.cast ho i)) sorry)) sorry)
  (if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩)
Tactic: rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ Eq.{u_1 + 1} (α := α)
    (if hi : (↑(Fin.cast ho i) : ℕ) < m then
      Eq.rec (motive := fun (x : Fin (m + n)) (h : Fin.castAdd n ((Fin.cast ho i).castLT hi) = x) ↦ α)
        (u ((Fin.cast ho i).castLT hi)) ⋯
    else
      Eq.rec (motive := fun (x : Fin (m + n)) (h : Fin.natAdd m (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = x) ↦ α)
        (v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) ⋯)
    (if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
have h : ∀ (hi : ¬(↑(Fin.cast ho i) : ℕ) < m),
  Eq.rec (motive := fun (x : Fin (m + n)) (h : Fin.natAdd m (Fin.subNat m (Fin.cast sorry (Fin.cast ho i)) sorry) = x) ↦ α)
      (v (Fin.subNat m (Fin.cast sorry (Fin.cast ho i)) sorry)) sorry =
    v (⟨(↑i : ℕ) - m, sorry⟩ : Fin n)
Tactic: congr with hi
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬(↑(Fin.cast ho i) : ℕ) < m
⊢ Eq.rec (motive := fun (x : Fin (m + n)) (h : Fin.natAdd m (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = x) ↦ α)
      (v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) ⋯ =
    v (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n)
have h : v (Fin.subNat m (Fin.cast sorry (Fin.cast ho i)) sorry) = v ⟨(↑i : ℕ) - m, sorry⟩
Tactic: simp only [eq_rec_constant]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ ![] v = v
have h : ∀ (x : Fin n), vecAppend sorry ![] v x = v x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ v ![] = v
have h : ∀ (x : Fin (n + 0)), vecAppend sorry v ![] x = v x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho (vecCons x u) v = vecCons x (vecAppend ⋯ u v)
have h : ∀ (i : Fin (o + 1)), vecAppend ho (vecCons x u) v i = vecCons x (vecAppend sorry u v) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend ⋯ u v) i
have h : (if h : (↑i : ℕ) < m + 1 then vecCons x u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - (m + 1), sorry⟩) =
  vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u (⟨(↑i : ℕ), h⟩ : Fin m) else v (⟨(↑i : ℕ) - m, sorry⟩ : Fin n)) i
Tactic: simp_rw [vecAppend_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ (if h : (↑i : ℕ) < m + 1 then vecCons x u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - (m + 1), ⋯⟩) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u (⟨(↑i : ℕ), h⟩ : Fin m) else v (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n))
      i
have pos : ∀ (h : (↑i : ℕ) < m + 1),
  vecCons x u (⟨(↑i : ℕ), h⟩ : Fin (m + 1)) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩) i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
pos :
  ∀ (h : (↑i : ℕ) < m + 1),
    vecCons x u (⟨(↑i : ℕ), h⟩ : Fin (m + 1)) =
      vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩) i
⊢ (if h : (↑i : ℕ) < m + 1 then vecCons x u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - (m + 1), ⋯⟩) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u (⟨(↑i : ℕ), h⟩ : Fin m) else v (⟨(↑i : ℕ) - m, ⋯⟩ : Fin n))
      i
have neg : ∀ (h : ¬(↑i : ℕ) < m + 1),
  v (⟨(↑i : ℕ) - (m + 1), sorry⟩ : Fin n) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩) i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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
⊢ vecCons x u (⟨(↑i : ℕ), h⟩ : Fin (m + 1)) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩) i
have pos : ∀ (hi : 0 < o + 1) (h : (↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) < m + 1),
  vecCons x u (⟨(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ), h⟩ : Fin (m + 1)) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩)
      (⟨0, hi⟩ : Fin (o + 1))
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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
pos :
  ∀ (hi : 0 < o + 1) (h : (↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) < m + 1),
    vecCons x u (⟨(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ), h⟩ : Fin (m + 1)) =
      vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩)
        (⟨0, hi⟩ : Fin (o + 1))
⊢ vecCons x u (⟨(↑i : ℕ), h⟩ : Fin (m + 1)) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩) i
have pos₁ : ∀ (i : ℕ) (hi : i + 1 < o + 1) (h : (↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ) < m + 1),
  vecCons x u (⟨(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ), h⟩ : Fin (m + 1)) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩)
      (⟨i + 1, hi⟩ : Fin (o + 1))
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
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
⊢ vecCons x u (⟨(↑(⟨i + 1, hi⟩ : Fin (o + 1)) : ℕ), h⟩ : 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))
have h₁ : i < m
Tactic: simp only [Nat.add_lt_add_iff_right] at h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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
⊢ 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
have neg : ∀ (hi : 0 < o + 1) (h : ¬(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) < m + 1),
  v (⟨(↑(⟨0, hi⟩ : Fin (o + 1)) : ℕ) - (m + 1), sorry⟩ : Fin n) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩)
      (⟨0, hi⟩ : Fin (o + 1))
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
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))
⊢ 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
have 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), sorry⟩ : Fin n) =
    vecCons x (fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, sorry⟩)
      (⟨i + 1, hi⟩ : Fin (o + 1))
Tactic: rcases i with ⟨⟨⟩ | i, hi⟩
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
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
⊢ 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))
have h₁ : m ≤ i
Tactic: rw [not_lt, Fin.val_mk, Nat.add_le_add_iff_right] at h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin n) ↦ n_1 + n_1
have h : ∀ (i : Fin n), vecAlt0 sorry (vecAppend sorry v v) i = (v ∘ fun (n_1 : Fin n) ↦ n_1 + n_1) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun (n_1 : Fin n) ↦ n_1 + n_1) i
have h : (if h : (↑i : ℕ) + (↑i : ℕ) < n then v ⟨(↑i : ℕ) + (↑i : ℕ), sorry⟩ else v ⟨(↑i : ℕ) + (↑i : ℕ) - n, sorry⟩) = v (i + i)
Tactic: simp_rw [Function.comp, vecAlt0, vecAppend_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ (if h : (↑i : ℕ) + (↑i : ℕ) < n then v ⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ else v ⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩) = v (i + i)
have pos : ∀ (h : (↑i : ℕ) + (↑i : ℕ) < n), v (⟨(↑i : ℕ) + (↑i : ℕ), sorry⟩ : Fin n) = v (i + i)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
pos : ∀ (h : (↑i : ℕ) + (↑i : ℕ) < n), v (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin n) = v (i + i)
⊢ (if h : (↑i : ℕ) + (↑i : ℕ) < n then v ⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ else v ⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩) = v (i + i)
have neg : ∀ (h : ¬(↑i : ℕ) + (↑i : ℕ) < n), v (⟨(↑i : ℕ) + (↑i : ℕ) - n, sorry⟩ : Fin n) = v (i + i)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : (↑i : ℕ) + (↑i : ℕ) < n
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ), ⋯⟩ : Fin n) = v (i + i)
have pos : (↑i : ℕ) + (↑i : ℕ) = ((↑i : ℕ) + (↑i : ℕ)) % n
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬(↑i : ℕ) + (↑i : ℕ) < n
⊢ v (⟨(↑i : ℕ) + (↑i : ℕ) - n, ⋯⟩ : Fin n) = v (i + i)
have neg : (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ)) % n
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (hypothesis)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬(↑i : ℕ) + (↑i : ℕ) < n
⊢ (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ)) % n
have h₁ : n ≤ (↑i : ℕ) + (↑i : ℕ)
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 → α
i : Fin n
h : n ≤ (↑i : ℕ) + (↑i : ℕ)
⊢ (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ)) % n
have neg : (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ) - n) % n
Tactic: simp only [Nat.mod_eq_sub_mod h]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ (↑i : ℕ) + (↑i : ℕ)
⊢ (↑i : ℕ) + (↑i : ℕ) - n = ((↑i : ℕ) + (↑i : ℕ) - n) % n
have neg : (↑i : ℕ) + (↑i : ℕ) - n < n
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) → α
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1
have h : ∀ (i : Fin (n + 1)), vecAlt1 sorry (vecAppend sorry v v) i = (v ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun (n_1 : Fin (n + 1)) ↦ n_1 + n_1 + 1) i
have h : (if h : (↑i : ℕ) + (↑i : ℕ) + 1 < n + 1 then v ⟨(↑i : ℕ) + (↑i : ℕ) + 1, sorry⟩
  else v ⟨(↑i : ℕ) + (↑i : ℕ) + 1 - (n + 1), sorry⟩) =
  v (i + i + 1)
Tactic: simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
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)
have 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, sorry⟩
    else
      v
        ⟨(↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + (↑(⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) : ℕ) + 1 -
            HAdd.hAdd (α := ℕ) 0 1,
          sorry⟩) =
    v ((⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + (⟨i, hi⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) + 1)
Tactic: obtain ⟨i, hi⟩ := i
Cleared hypotheses: i