awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
nil :
  ∀ (h : List.length.{u_1} (α := α) [] = n),
    Eq.{u_1 + 1} (α := α) (get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)) (⟨i, ih⟩ : Fin (n - 1)))
      (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h) (⟨i + 1, ⋯⟩ : Fin n))
cons :
  ∀ (head : α) (tail : List α) (h : (head :: tail).length = n),
    get (Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)) (⟨i, ih⟩ : Fin (n - 1)) =
      get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h) (⟨i + 1, ⋯⟩ : Fin n)
⊢ x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨i + 1, ⋯⟩

Tactic:
rcases x with ⟨_ | _, h⟩
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
head : α
tail : List α
h : (head :: tail).length = n
⊢ get (Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)) (⟨i, ih⟩ : Fin (n - 1)) =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h) (⟨i + 1, ⋯⟩ : Fin n)

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
head : α
tail : List α
h : (head :: tail).length = n
⊢ get (Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)) (⟨i, ih⟩ : Fin (n - 1)) =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h) (⟨i + 1, ⋯⟩ : Fin n)

Tactic:
try rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
h : List.length.{u_1} (α := α) [] = n
⊢ 0 = n

Tactic:
rw [List.length] at h

Premises used: List.length
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
h_1 : List.length.{u_1} (α := α) [] = n
h : 0 = n
⊢ i < HSub.hSub (α := ℕ) 0 1

Tactic:
rw [← h] at ih
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
h_1 : List.length.{u_1} (α := α) [] = n
h : 0 = n
ih₁ : i < HSub.hSub (α := ℕ) 0 1
⊢ List.length.{u_1} (α := α) [] = n

Tactic:
rw [← h] at ih
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
h_1 : List.length.{u_1} (α := α) [] = n
h : 0 = n
ih₁ : i < HSub.hSub (α := ℕ) 0 1
h₁ : List.length.{u_1} (α := α) [] = n
⊢ 0 = n

Tactic:
rw [← h] at ih
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n i : ℕ
ih_1 : i < n - 1
ih : i < HSub.hSub (α := ℕ) 0 1
h_1 : List.length.{u_1} (α := α) [] = n
h : 0 = n
⊢ Eq.{u_1 + 1} (α := α)
    (get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h_1)) (⟨i, ih_1⟩ : Fin (n - 1)))
    (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h_1) (⟨i + 1, ⋯⟩ : Fin n))

Tactic:
contradiction
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
simp :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (toList (n := n) (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: l) e) : Vector α (n + 1 - 1)))
      i ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯
⊢ get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (a :: l) e)) (⟨i, h⟩ : Fin n) =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (a :: l) e) (⟨i, h⟩ : Fin n).succ

Tactic:
simp [get_eq_get_toList]

Premises used: List.Vector.get_eq_get_toList
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (toList (n := n) (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: l) e) : Vector α (n + 1 - 1)))
      i ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Vector α (HSub.hSub (α := ℕ) 0 1)) (tail nil) nil

Tactic:
rfl

Premises used: List.Vector.nil, List.Vector.tail, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
e_a : (ofFn f).tail.get = fun (i : Fin n) ↦ f i.succ
⊢ ofFn (ofFn f).tail.get = ofFn fun (i : Fin n) ↦ f i.succ

Tactic:
congr
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
e_a : ∀ (i : Fin (n.succ - 1)), (ofFn f).tail.get i = f i.succ
⊢ (ofFn f).tail.get = fun (i : Fin n) ↦ f i.succ

Tactic:
funext i
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
e_a : f (⟨(↑i : ℕ) + 1, ⋯⟩ : Fin n.succ) = f i.succ
⊢ (ofFn f).tail.get i = f i.succ

Tactic:
rw [get_tail, get_ofFn]

Premises used: List.Vector.get_tail, List.Vector.get_ofFn
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ f (⟨(↑i : ℕ) + 1, ⋯⟩ : Fin n.succ) = f i.succ

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
property : List.length.{u_1} (α := α) [] = n
⊢ Eq.{u_1 + 1} (α := List α)
    (toList (n := n - 1) (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] property)))
    (List.tail (toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] property)))

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
head : α
tail : List α
property : (head :: tail).length = n
⊢ toList (n := n - 1) (Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) property)) =
    (toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) property)).tail

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
v : Vector α 0
⊢ v.toList = []

Tactic:
List.length_eq_zero_iff.mp v.2

Premises used: Iff.mp, List.length_eq_zero_iff, Subtype.property
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
v : Vector α 1
rw : (v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]
⊢ v.toList = [v.head]

Tactic:
rw [← v.cons_head_tail]

Premises used: List.Vector.cons_head_tail
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
v : Vector α 1
⊢ (v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]

Tactic:
simp only [toList_cons, toList_nil, head_cons, singleton_tail]

Premises used: List.Vector.toList_cons, List.Vector.toList_nil, List.Vector.head_cons, List.Vector.singleton_tail
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.isEmpty = false

Tactic:
match v with
  | ⟨_ :: _, _⟩ => rfl

Premises used: List.isEmpty, _private.0.List.Vector.empty_toList_eq_ff.match_1, Bool.false, Eq, List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ ¬v.toList.isEmpty = true

Tactic:
simp only [empty_toList_eq_ff, Bool.coe_sort_false, not_false_iff]

Premises used: Bool.coe_sort_false, not_false_iff, List.Vector.empty_toList_eq_ff
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ (map id v).toList = v.toList

Tactic:
simp only [List.map_id, Vector.toList_map]

Premises used: List.map_id, List.Vector.toList_map
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
obtain :
  ∀ (l : List α),
    (toList (n := l.length) (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l ⋯)).Nodup ↔
      Function.Injective (α := Fin l.length) (get (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l ⋯))
⊢ v.toList.Nodup ↔ Function.Injective v.get

Tactic:
obtain ⟨l, rfl⟩ := v

Premises used: rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
l : List α
⊢ (toList (n := l.length) (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l ⋯)).Nodup ↔
    Function.Injective (α := Fin l.length) (get (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l ⋯))

Tactic:
List.nodup_iff_injective_get

Premises used: List.Vector.get, List.nodup_iff_injective_get, List.Vector.toList
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
l : List α
⊢ (toList (n := l.length) (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l ⋯)).Nodup ↔
    Function.Injective (α := Fin l.length) (get (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l ⋯))

Tactic:
exact List.nodup_iff_injective_get

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
v : Vector α n
⊢ v.toList.reverse.length = n

Tactic:
simp
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ v.reverse.toList = v.toList.reverse

Tactic:
rfl

Premises used: List.reverse, List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
mk :
  ∀ (val : List α) (property : val.length = n),
    Eq (α := Vector α n) (reverse (reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)))
      (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
⊢ v.reverse.reverse = v

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
val : List α
property : val.length = n
⊢ Eq (α := Vector α n) (reverse (reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)

Tactic:
simp [Vector.reverse]

Premises used: List.Vector.reverse
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
rw : (ofFn f).get 0 = f 0
rw₁ rw₂ : f 0 = f 0
⊢ (ofFn f).head = f 0

Tactic:
rw [← get_zero, get_ofFn]

Premises used: List.Vector.get_ofFn, List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (a ::ᵥ v).get 0 = a

Tactic:
simp [get_zero]

Premises used: List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
rw : (a ::ᵥ v).tail.get i = v.get i
rw₁ rw₂ : v.get i = v.get i
⊢ (a ::ᵥ v).get i.succ = v.get i

Tactic:
rw [← get_tail_succ, tail_cons]

Premises used: List.Vector.tail_cons, List.Vector.get_tail_succ
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.last = v.get (Fin.last n)

Tactic:
rfl

Premises used: List.Vector.last, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
rw : v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
⊢ v.reverse.head = v.last

Tactic:
rw [← get_zero, last_def, get_eq_get_toList, get_eq_get_toList]

Premises used: List.Vector.last_def, List.Vector.get_eq_get_toList, List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
simp_rw : v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
simp_rw [toList_reverse]

Premises used: List.Vector.toList_reverse
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
simp
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β_1 : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
rw : v.toList.length + 1 = n + 1
rw₁ rw₂ : n + 1 = n + 1
⊢ (List.scanl f b v.toList).length = n + 1

Tactic:
rw [List.length_scanl, toList_length]

Premises used: List.length_scanl, List.Vector.toList_length
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
x : ∀ (m : Fin (HAdd.hAdd (α := ℕ) 0 1)), (scanl f b nil).get m = (b ::ᵥ nil).get m
⊢ scanl f b nil = b ::ᵥ nil

Tactic:
ext
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
m : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ (scanl f b nil).get m = (b ::ᵥ nil).get m

Tactic:
simp [scanl, get]

Premises used: List.Vector.get, List.Vector.scanl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
a : (scanl f b (x ::ᵥ v)).toList = (b ::ᵥ scanl f (f b x) v).toList
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Tactic:
apply Vector.eq

Premises used: List.Vector.eq
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ (scanl f b (x ::ᵥ v)).toList = (b ::ᵥ scanl f (f b x) v).toList

Tactic:
simp [scanl]

Premises used: List.Vector.scanl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (scanl f b v).toList = List.scanl f b v.toList

Tactic:
rfl

Premises used: List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
rw : scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
rw [← cons_head_tail v]

Premises used: List.Vector.cons_head_tail
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil

Tactic:
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]

Premises used: List.Vector.scanl_nil, List.Vector.head_cons, List.Vector.scanl_cons, List.Vector.singleton_tail
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
zero : ∀ (v : Vector α 0), (scanl f b v).head = b
succ : ∀ (n : ℕ) (v : Vector α (n + 1)), (scanl f b v).head = b
⊢ (scanl f b v).head = b

Tactic:
cases n
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ v = nil

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ v = nil

Tactic:
have : v = nil := by simp only [eq_iff_true_of_subsingleton]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
this : v = nil
⊢ (scanl f b v).head = b

Tactic:
simp only [this, scanl_nil, head_cons]

Premises used: List.Vector.scanl_nil, List.Vector.head_cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
succ : (scanl f b (v.head ::ᵥ v.tail)).head = b
⊢ (scanl f b v).head = b

Tactic:
rw [← cons_head_tail v]

Premises used: List.Vector.cons_head_tail
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
⊢ (scanl f b (v.head ::ᵥ v.tail)).head = b

Tactic:
simp [← get_zero, get_eq_get_toList]

Premises used: List.Vector.get_eq_get_toList, List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
i : Fin n
zero : ∀ (v : Vector α 0) (i : Fin 0), (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
succ :
  ∀ (n : ℕ) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
i : Fin 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
i : Fin 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ i = 0

Tactic:
have i0 : i = 0 := Fin.eq_zero _
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i0 : i = 0
succ : (b ::ᵥ f b v.head ::ᵥ nil).get 1 = f b v.head
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
simp [scanl_singleton, i0, get_zero]

Premises used: List.Vector.scanl_singleton, List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i0 : i = 0
⊢ (b ::ᵥ f b v.head ::ᵥ nil).get 1 = f b v.head

Tactic:
simp [get_eq_get_toList]

Premises used: List.Vector.get_eq_get_toList
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
succ :
  (scanl f (f b v.head) v.tail).get i =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
rw [← cons_head_tail v, scanl_cons, get_cons_succ]

Premises used: List.Vector.cons_head_tail, List.Vector.get_cons_succ, List.Vector.scanl_cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get i =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
succ :
  (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)
succ₁ :
  ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)
⊢ (scanl f (f b v.head) v.tail).get i =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)

Tactic:
simp
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
i' : Fin (n + 1)
⊢ (scanl f (f b v.head) v.tail).get i'.succ =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i'.succ.castSucc) ((v.head ::ᵥ v.tail).get i'.succ)

Tactic:
simp only [hn, Fin.castSucc_succ, get_cons_succ]

Premises used: Fin.castSucc_succ, List.Vector.get_cons_succ
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
succ :
  ∀ (b : β) (v : Vector α (HAdd.hAdd (α := ℕ) 0 1)) (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
succ₁ :
  ∀ (n : ℕ)
    (hn :
      ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
        (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i))
    (b : β) (v : Vector α (n + 1 + 1)) (i : Fin (n + 1 + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
induction n generalizing b with
  | zero =>
    have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]
  | succ n hn =>
    rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp
    · intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]

Premises used: List.Vector.get_eq_get_toList, Fin.castSucc_succ, List.Vector.scanl_singleton, List.Vector.cons_head_tail, List.Vector.get_cons_succ, List.Vector.scanl_cons, List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
m : Type u_6 → Type u_7
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
rw :
  Eq.{u_7 + 1} (α := m (Vector α (n + 1)))
    (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun (i : Fin n) ↦ f i.succ)
      pure (a ::ᵥ v))
    (pure (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ))
⊢ Eq.{u_7 + 1} (α := m (Vector α (n + 1))) (mOfFn fun (i : Fin (n + 1)) ↦ pure (f i)) (pure (ofFn f))

Tactic:
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]

Premises used: List.Vector.ofFn, List.Vector.mOfFn
-- Module: Mathlib.Data.Vector.Basic
Goal:
m : Type u_6 → Type u_7
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ Eq.{u_7 + 1} (α := m (Vector α (n + 1)))
    (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun (i : Fin n) ↦ f i.succ)
      pure (a ::ᵥ v))
    (pure (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ))

Tactic:
simp
-- Module: Mathlib.Data.Vector.Basic
Goal:
m : Type u_6 → Type u_7
inst : Monad m
α : Type u_8
β : Type u_6
f : α → m β
⊢ mmap f nil = pure nil

Tactic:
rfl

Premises used: List.Vector.mmap, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
v : Vector α 0
zero : C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯)
⊢ C v

Tactic:
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯)

Tactic:
exact nil
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v : Vector α (n + 1)
succ :
  (v_property : List.length.{u_1} (α := α) [] = n + 1) →
    C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property)
succ₁ :
  (a : α) →
    (v : List α) →
      (v_property : (a :: v).length = n + 1) →
        C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)
⊢ C v

Tactic:
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v_property : List.length.{u_1} (α := α) [] = n + 1
⊢ C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property)

Tactic:
cases v_property
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)

Tactic:
exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)

Premises used: add_left_inj, Subtype.mk, Iff.mp, OfNat.ofNat