awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Take
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₁ :
  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) ⋯)))) _ ⋯)
⊢ 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

Tactic:
simp only [take, addCases, val_castLE]

Premises used: Fin.take, Fin.val_castLE
-- Module: Mathlib.Data.Fin.Tuple.Take
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) ⋯)))) _ ⋯)
neg :
  ∀ (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) ⋯)))) _ ⋯)

Tactic:
by_cases h' : i < n
-- Module: Mathlib.Data.Fin.Tuple.Take
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
pos :
  Eq (α := motive (castLE ⋯ i)) (u ((castLE ⋯ i).castLT ⋯) : motive (castAdd n' ((castLE ⋯ i).castLT ⋯)))
    (u (i.castLT ⋯))
⊢ 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) ⋯)))) _ ⋯)

Tactic:
simp only [h', ↓reduceDIte]

Premises used: reduceDIte
-- Module: Mathlib.Data.Fin.Tuple.Take
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 (α := motive (castLE ⋯ i)) (u ((castLE ⋯ i).castLT ⋯) : motive (castAdd n' ((castLE ⋯ i).castLT ⋯)))
    (u (i.castLT ⋯))

Tactic:
congr
-- Module: Mathlib.Data.Fin.Tuple.Take
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) ⋯)))) _ ⋯)

Tactic:
simp only [h', ↓reduceDIte, subNat, castLE, Fin.cast, eqRec_eq_cast]

Premises used: eqRec_eq_cast, Fin.castLE, reduceDIte, Fin.cast, Fin.subNat
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
α : Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → α
v : (i : Fin n') → α
⊢ take (α := fun (a : Fin (n + n')) ↦ α) (n + m) ⋯ (append u v) = append u (take (α := fun (i : Fin n') ↦ α) m h v)

Tactic:
take_addCases_right m h _ _

Premises used: Fin.take_addCases_right, Fin.append
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Type u_2
m : ℕ
h : m ≤ n
v : Fin n → α
⊢ (List.ofFn (take (α := fun (i : Fin n) ↦ α) m h v)).length = (List.take m (List.ofFn v)).length

Tactic:
simp [h]
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n_1 : ℕ
α : Type u_2
m : ℕ
h : m ≤ n_1
v : Fin n_1 → α
n : ℕ
h1 : n < (List.ofFn (take (α := fun (i : Fin n_1) ↦ α) m h v)).length
h2 : n < (List.take m (List.ofFn v)).length
⊢ (List.ofFn (take (α := fun (i : Fin n_1) ↦ α) m h v)).get
      (⟨n, h1⟩ : Fin (List.ofFn (take (α := fun (i : Fin n_1) ↦ α) m h v)).length) =
    (List.take m (List.ofFn v)).get (⟨n, h2⟩ : Fin (List.take m (List.ofFn v)).length)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.ofFn (take (α := fun (i : Fin l.length) ↦ α) m h l.get)).length = (List.take m l).length

Tactic:
simp [h]
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
n : ℕ
h1 : n < (List.ofFn (take (α := fun (i : Fin l.length) ↦ α) m h l.get)).length
h2 : n < (List.take m l).length
⊢ (List.ofFn (take (α := fun (i : Fin l.length) ↦ α) m h l.get)).get
      (⟨n, h1⟩ : Fin (List.ofFn (take (α := fun (i : Fin l.length) ↦ α) m h l.get)).length) =
    (List.take m l).get (⟨n, h2⟩ : Fin (List.take m l).length)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
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 ⋯) i
⊢ (List.take m l).get = take (α := fun (i : Fin l.length) ↦ α) m h l.get ∘ Fin.cast ⋯

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
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 ⋯) i

Tactic:
simp only [List.get_eq_getElem, List.getElem_take, comp_apply, take_apply, val_castLE, val_cast]

Premises used: List.get_eq_getElem, Fin.take_apply, List.getElem_take, Fin.val_cast, Function.comp_apply, Fin.val_castLE
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α_1 : Fin n → Sort u_1
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).length = m

Tactic:
simp [h]
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
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 ⋯) i
⊢ (List.take m (List.ofFn v)).get = take (α := fun (i : Fin n) ↦ α) m h v ∘ Fin.cast ⋯

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
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 ⋯) i

Tactic:
simp [castLE]

Premises used: Fin.castLE
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
v : Fin 0 → α
⊢ v = ![]

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
⊢ (vecHead (n := n) fun (x : Fin (n + 1)) ↦ a) = a

Tactic:
rfl

Premises used: Matrix.vecHead, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecCons x u 0 = x

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
h : 0 < m.succ
x : α
u : Fin m → α
⊢ vecCons x u (⟨0, h⟩ : Fin m.succ) = x

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m → α
i : Fin m
⊢ vecCons x u i.succ = u i

Tactic:
simp [vecCons]

Premises used: Matrix.vecCons
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m i : ℕ
h : i.succ < m.succ
x : α
u : Fin m → α
⊢ vecCons x u (⟨i.succ, h⟩ : Fin m.succ) = u ⟨i, ⋯⟩

Tactic:
simp only [vecCons, Fin.cons, Fin.cases_succ']

Premises used: Fin.cons, Fin.cases_succ', Matrix.vecCons
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u_1
x : α
⊢ Fin.cons (α := fun (a : Fin (Nat.succ 0)) ↦ α) x ![] = ![x]

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u_1
x : α
h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x i = ![x] i
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x = ![x]

Tactic:
ext i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u_1
x : α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h : Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x 0 = ![x] 0
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x i = ![x] i

Tactic:
cases Fin.fin_one_eq_zero i

Premises used: Fin.fin_one_eq_zero
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u_1
x : α
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0)) ↦ α) ![] x 0 = ![x] 0

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
n : ℕ
α : Type u_1
x y : α
p : Fin n → α
⊢ Fin.cons (α := fun (a : Fin n.succ.succ) ↦ α) x (vecCons y p) = vecCons x (vecCons y p)

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
n : ℕ
α : Type u_1
x y : α
p : Fin n → α
⊢ Eq (α := (i : Fin (n + 1 + 1)) → α) (Fin.snoc (α := fun (a : Fin (n + 1).succ) ↦ α) (vecCons y p) x)
    (vecCons y (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) p x))

Tactic:
Fin.cons_snoc_eq_snoc_cons .. |>.symm

Premises used: Fin.cons_snoc_eq_snoc_cons, Eq.symm, Matrix.vecCons
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecHead (vecCons x u) = x

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Matrix.vecHead, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m → α
h : ∀ (x_1 : Fin m), vecTail (vecCons x u) x_1 = u x_1
⊢ vecTail (vecCons x u) = u

Tactic:
ext
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m → α
x_1 : Fin m
⊢ vecTail (vecCons x u) x_1 = u x_1

Tactic:
simp [vecTail]

Premises used: Matrix.vecTail
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x : α
t : Fin n → α
⊢ Fin.tail (α := fun (a : Fin (n + 1)) ↦ α) (vecCons x t) = t

Tactic:
rfl

Premises used: Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Fin.tail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n' : Type u_1
j : n'
⊢ Eq.{u + 1} (α := (i : Fin 0) → α) (fun (i : Fin 0) ↦ ![] i j) ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
u : Fin m.succ → α
⊢ vecCons (vecHead u) (vecTail u) = u

Tactic:
Fin.cons_self_tail _

Premises used: Fin.cons_self_tail, Matrix.vecHead, Matrix.vecTail, Matrix.vecCons
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u

Tactic:
simp [Fin.exists_fin_succ, eq_comm]

Premises used: eq_comm, Fin.exists_fin_succ
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
u : Fin 0 → α
⊢ Set.range u = ∅

Tactic:
Set.range_eq_empty _

Premises used: Set.range_eq_empty
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
x : α
u : Fin 0 → α
rw : {x} ∪ Set.range u = {x}
rw₁ : Eq (α := Set α) ({x} ∪ ∅) {x}
rw₂ rw₃ : Eq (α := Set α) {x} {x}
⊢ Set.range (vecCons x u) = {x}

Tactic:
rw [range_cons, range_empty, Set.union_empty]

Premises used: Matrix.range_cons, Set.union_empty, Matrix.range_empty
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
x y : α
u : Fin 0 → α
rw : {x} ∪ Set.range (vecCons y u) = {x, y}
rw₁ : Eq (α := Set α) ({x} ∪ {y}) {x, y}
rw₂ rw₃ : Eq (α := Set α) {x, y} {x, y}
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}

Tactic:
rw [range_cons, range_cons_empty, Set.singleton_union]

Premises used: Matrix.range_cons, Set.singleton_union, Matrix.range_cons_empty
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
⊢ Eq (α := Fin n.succ → α) (vecCons a fun (x : Fin n) ↦ a) fun (x : Fin n.succ) ↦ a

Tactic:
funext <| Fin.forall_iff_succ.2 ⟨rfl, cons_val_succ _ _⟩

Premises used: Iff.mpr, Matrix.cons_val_succ, funext, Fin.forall_iff_succ, And.intro, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
a : α
⊢ ![a] = fun (x : Fin (Nat.succ 0)) ↦ a

Tactic:
let _ : Unique (Fin 1) := inferInstance
  funext <| Unique.forall_iff.2 rfl

Premises used: Iff.mpr, inferInstance, Unique.forall_iff, funext, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m.succ → α
⊢ vecCons x u 1 = u 0

Tactic:
rfl

Premises used: Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Nat.mod, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m.succ.succ → α
⊢ vecCons x u 2 = vecHead (vecTail u)

Tactic:
rfl

Premises used: Fin.succ, Fin.cons, Fin.induction, Matrix.vecHead, Nat.mod, Fin.cases, Matrix.vecTail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m.succ.succ.succ → α
⊢ vecCons x u 3 = vecHead (vecTail (vecTail u))

Tactic:
rfl

Premises used: Fin.succ, Fin.cons, Fin.induction, Matrix.vecHead, Nat.mod, Fin.cases, Matrix.vecTail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m : ℕ
x : α
u : Fin m.succ.succ.succ.succ → α
⊢ vecCons x u 4 = vecHead (vecTail (vecTail (vecTail u)))

Tactic:
rfl

Premises used: Fin.succ, Fin.cons, Fin.induction, Matrix.vecHead, Nat.mod, Fin.cases, Matrix.vecTail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
x : α
u : Fin 0 → α
rw : vecCons x u 0 = x
⊢ ∀ (i : Fin 1), vecCons x u i = x

Tactic:
rw [Fin.forall_fin_one]

Premises used: Fin.forall_fin_one
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
x : α
u : Fin 0 → α
⊢ vecCons x u = fun (x_1 : Fin (Nat.succ 0)) ↦ x

Tactic:
funext (cons_val_fin_one x u)

Premises used: Matrix.cons_val_fin_one, funext
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
x y : α
u v : Fin n → α
⊢ vecCons x u = vecCons y v ↔ x = y ∧ u = v

Tactic:
Fin.cons_inj

Premises used: Fin.cons_inj, Matrix.vecCons
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α_1 : Type u
m n o_1 : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
h : ¬(↑i : ℕ) < m
⊢ (↑i : ℕ) - m < n

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
h : ∀ (i : Fin o), vecAppend ho u v i = if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩
⊢ vecAppend ho u v = fun (i : Fin o) ↦ if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩

Tactic:
ext i
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
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)) ⋯
    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, ⋯⟩)
⊢ vecAppend ho u v i = if h : (↑i : ℕ) < m then u ⟨(↑i : ℕ), h⟩ else v ⟨(↑i : ℕ) - m, ⋯⟩

Tactic:
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]

Premises used: Matrix.vecAppend, Function.comp_apply, Fin.append
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
h :
  ∀ (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)
⊢ 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, ⋯⟩)

Tactic:
congr with hi
-- Module: Mathlib.Data.Fin.VecNotation
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
h : v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨(↑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)

Tactic:
simp only [eq_rec_constant]

Premises used: eq_rec_constant
-- Module: Mathlib.Data.Fin.VecNotation
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
⊢ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨(↑i : ℕ) - m, ⋯⟩

Tactic:
rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
m n : ℕ
α : Type u_1
o : ℕ
ho : o + 1 = m + 1 + n
u : Fin (m + 1) → α
v : Fin n → α
⊢ vecAppend ho u v 0 = u 0

Tactic:
rfl

Premises used: Matrix.vecAppend, Fin.ofNat, Fin.addCases, dite, Nat.mod, Fin.append, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
h : ∀ (x : Fin n), vecAppend ⋯ ![] v x = v x
⊢ vecAppend ⋯ ![] v = v

Tactic:
ext
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
x : Fin n
⊢ vecAppend ⋯ ![] v x = v x

Tactic:
simp [vecAppend_eq_ite]

Premises used: Matrix.vecAppend_eq_ite
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
h : ∀ (x : Fin (n + 0)), vecAppend ⋯ v ![] x = v x
⊢ vecAppend ⋯ v ![] = v

Tactic:
ext
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
v : Fin n → α
x : Fin (n + 0)
⊢ vecAppend ⋯ v ![] x = v x

Tactic:
simp [vecAppend_eq_ite]

Premises used: Matrix.vecAppend_eq_ite
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ o = m + n

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

Tactic:
ext i
-- 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 :
  (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
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend ⋯ u v) i

Tactic:
simp_rw [vecAppend_eq_ite]

Premises used: Matrix.vecAppend_eq_ite
-- 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)
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
neg :
  ∀ (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
⊢ (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

Tactic:
split_ifs with 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
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))
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, ⋯⟩)
        (⟨i + 1, 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

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
⊢ 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))

Tactic:
simp
-- 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
⊢ i < m

Tactic:
simp only [Nat.add_lt_add_iff_right] at h

Premises used: Nat.add_lt_add_iff_right