awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n_1 : ℕ
x : α
w : Vector α n_1
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w = Comp.mk (Vector.traverse f <$> Vector.traverse g w)
cons :
  Vector.cons <$> (Comp.mk ∘ Functor.map f ∘ g) x <*> Comp.mk (Vector.traverse f <$> Vector.traverse g w) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ w) = Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))

Tactic:
rw [Vector.traverse_def, ih]

Premises used: List.Vector.traverse_def
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n_1 : ℕ
x : α
w : Vector α n_1
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w = Comp.mk (Vector.traverse f <$> Vector.traverse g w)
⊢ cons <$> (Comp.mk ∘ Functor.map f ∘ g) x <*> Comp.mk (Vector.traverse f <$> Vector.traverse g w) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))

Tactic:
simp [functor_norm, Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : Vector α n
nil :
  Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) Vector.nil =
    Comp.mk (Vector.traverse f <$> Vector.traverse g Vector.nil)
cons :
  ∀ {n : ℕ} {x : α} {w : Vector α n}
    (ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w = Comp.mk (Vector.traverse f <$> Vector.traverse g w)),
    Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ w) =
      Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)

Tactic:
induction x with
  | nil =>
    simp! [cast, *, functor_norm]
    rfl
  | cons ih =>
    rw [Vector.traverse_def, ih]
    simp [functor_norm, Function.comp_def]

Premises used: List.Vector.traverse_def, cast, Function.comp_def, List.Vector.nil, List.Vector.cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α β : Type u_6
f : α → β
x : List α
simp! :
  Eq (α := Id (Vector β x.length)) (traverseAux (pure ∘ f) x)
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = x.length) (List.map f x) ⋯))
⊢ Eq (α := Id (Vector β x.length))
    (Vector.traverse (pure ∘ f) (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))
    (pure (map f (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯)))

Tactic:
simp!
-- Module: Mathlib.Data.Vector.Basic
Goal:
α β : Type u_6
f : α → β
x : List α
nil :
  Eq (α := Id (Vector β (List.length.{u_6} (α := α) []))) (traverseAux (pure ∘ f) [])
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = List.length.{u_6} (α := α) []) (List.map f []) ⋯))
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := Id (Vector β tail.length)) (traverseAux (pure ∘ f) tail)
        (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = tail.length) (List.map f tail) ⋯)) →
      Eq (α := Id (Vector β (head :: tail).length)) (traverseAux (pure ∘ f) (head :: tail))
        (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = (head :: tail).length) (List.map f (head :: tail)) ⋯))
⊢ Eq (α := Id (Vector β x.length)) (traverseAux (pure ∘ f) x)
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = x.length) (List.map f x) ⋯))

Tactic:
induction x
-- Module: Mathlib.Data.Vector.Basic
Goal:
α β : Type u_6
f : α → β
head : α
tail : List α
tail_ih :
  Eq (α := Id (Vector β tail.length)) (traverseAux (pure ∘ f) tail)
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = tail.length) (List.map f tail) ⋯))
⊢ Eq (α := Id (Vector β (head :: tail).length)) (traverseAux (pure ∘ f) (head :: tail))
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = (head :: tail).length) (List.map f (head :: tail)) ⋯))

Tactic:
simp! [*, functor_norm]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α β : Type u_6
f : α → β
⊢ Eq.{u_6 + 1} (α := Id (Vector β 0)) (pure nil) (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯))

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ Eq (α := G (Vector β 0)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f nil))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) nil)

Tactic:
simp! [functor_norm, cast, η.preserves_pure]

Premises used: cast, ApplicativeTransformation.preserves_pure
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n_1 : ℕ
x : α
w : Vector α n_1
ih :
  Eq (α := G (Vector β n_1)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) w)
cons :
  Eq (α := G (Vector β n_1.succ))
    (Vector.cons <$> (fun {α : Type u} ↦ η.app α) (f x) <*> (fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
    (Vector.cons <$> ((fun {α : Type u} ↦ η.app α) ∘ f) x <*> (fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
⊢ Eq (α := G (Vector β n_1.succ)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f (x ::ᵥ w)))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (x ::ᵥ w))

Tactic:
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]

Premises used: List.Vector.traverse_def, ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_map
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n_1 : ℕ
x : α
w : Vector α n_1
ih :
  Eq (α := G (Vector β n_1)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) w)
⊢ Eq (α := G (Vector β n_1.succ))
    (cons <$> (fun {α : Type u} ↦ η.app α) (f x) <*> (fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
    (cons <$> ((fun {α : Type u} ↦ η.app α) ∘ f) x <*> (fun {α : Type u} ↦ η.app α) (Vector.traverse f w))

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
nil :
  Eq (α := G (Vector β 0)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f Vector.nil))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) Vector.nil)
cons :
  ∀ {n : ℕ} {x : α} {w : Vector α n}
    (ih :
      Eq (α := G (Vector β n)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
        (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) w)),
    Eq (α := G (Vector β n.succ)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f (x ::ᵥ w)))
      (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (x ::ᵥ w))
⊢ Eq (α := G (Vector β n)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f x))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)

Tactic:
induction x with
  | nil => simp! [functor_norm, cast, η.preserves_pure]
  | cons ih =>
    rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
    rfl

Premises used: List.Vector.traverse_def, cast, ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure, ApplicativeTransformation.preserves_map, List.Vector.nil, List.Vector.cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 : Type u
x : flip Vector n α_1
mk :
  ∀ (val : List α_1) (property : val.length = n),
    Eq.{u + 1} (α := flip Vector n α_1) (id <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
      (Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
⊢ id <$> x = x

Tactic:
cases x
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 : Type u
val : List α_1
property : val.length = n
⊢ Eq.{u + 1} (α := flip Vector n α_1) (id <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
    (Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)

Tactic:
simp! [(· <$> ·)]

Premises used: Functor.map
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 : Type u
_ : ∀ {β γ : Type u} (g : α_1 → β) (h : β → γ) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x
⊢ ∀ {β γ : Type u} (g : α_1 → β) (h : β → γ) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
_
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 β_1 : Type u
_ : ∀ {γ : Type u} (g : α_1 → β_1) (h : β_1 → γ) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x
⊢ ∀ {γ : Type u} (g : α_1 → β_1) (h : β_1 → γ) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
_
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 β_1 γ_1 : Type u
_ : ∀ (g : α_1 → β_1) (h : β_1 → γ_1) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x
⊢ ∀ (g : α_1 → β_1) (h : β_1 → γ_1) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
_
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
_ : ∀ (h : β_1 → γ_1) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x
⊢ ∀ (h : β_1 → γ_1) (x : flip Vector n α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
_
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : flip Vector n α_1
mk :
  ∀ (val : List α_1) (property : val.length = n),
    Eq (α := flip Vector n γ_1) ((h ∘ g) <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
      (h <$> g <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
⊢ (h ∘ g) <$> x = h <$> g <$> x

Tactic:
cases x
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
val : List α_1
property : val.length = n
⊢ Eq (α := flip Vector n γ_1) ((h ∘ g) <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
    (h <$> g <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)

Tactic:
simp! [(· <$> ·)]

Premises used: Functor.map
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = val ::ᵥ replicate n val

Tactic:
rfl

Premises used: List.replicate, List.Vector.replicate, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
m n : ℕ
x : α
xs : Vector α n
ys : Vector α m
⊢ (x ::ᵥ xs ++ ys).get 0 = x

Tactic:
rfl

Premises used: List.Vector.get, List.get, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
m n : ℕ
x : α
xs : Vector α n
ys : Vector α m
i : Fin (n + m)
h : (↑i : ℕ) + 1 < n.succ + m
⊢ (x ::ᵥ xs ++ ys).get (⟨(↑i : ℕ) + 1, h⟩ : Fin (n.succ + m)) = (xs ++ ys).get i

Tactic:
rfl

Premises used: List.Vector.get, List.get, List.append, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
xs : Vector α n
mk :
  ∀ (val : List α) (property : val.length = n),
    Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property ++ nil =
      Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property
⊢ HAppend.hAppend (β := Vector α 0) xs nil = xs

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

Tactic:
simp only [append_def, append_nil]

Premises used: List.Vector.append_def, List.Vector.append_nil
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
i : Fin 0
⊢ (map₂ f nil nil).get i = f (get nil i) (get nil i)

Tactic:
Fin.elim0 i

Premises used: Fin.elim0
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
i : Fin 0
⊢ (map₂ f nil nil).get i = f (get nil i) (get nil i)

Tactic:
exact Fin.elim0 i

Premises used: Fin.elim0
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
i : Fin n_1.succ
cons : (f a b ::ᵥ map₂ f x y).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
⊢ (map₂ f (a ::ᵥ x) (b ::ᵥ y)).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)

Tactic:
rw [map₂_cons]

Premises used: List.Vector.map₂_cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
i : Fin n_1.succ
cons : (f a b ::ᵥ map₂ f x y).get 0 = f ((a ::ᵥ x).get 0) ((b ::ᵥ y).get 0)
cons₁ : ∀ (i : Fin n_1), (f a b ::ᵥ map₂ f x y).get i.succ = f ((a ::ᵥ x).get i.succ) ((b ::ᵥ y).get i.succ)
⊢ (f a b ::ᵥ map₂ f x y).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)

Tactic:
cases i using Fin.cases
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
⊢ (f a b ::ᵥ map₂ f x y).get 0 = f ((a ::ᵥ x).get 0) ((b ::ᵥ y).get 0)

Tactic:
simp only [get_zero, head_cons]

Premises used: List.Vector.head_cons, List.Vector.get_zero
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
i : Fin n_1
⊢ (f a b ::ᵥ map₂ f x y).get i.succ = f ((a ::ᵥ x).get i.succ) ((b ::ᵥ y).get i.succ)

Tactic:
simp only [get_cons_succ, ih]

Premises used: List.Vector.get_cons_succ
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
nil : ∀ (i : Fin 0), (map₂ f Vector.nil Vector.nil).get i = f (get Vector.nil i) (get Vector.nil i)
cons :
  ∀ {n : ℕ} {a : α} {b : β} {x : Vector α n} {y : Vector β n}
    (ih : ∀ (i : Fin n), (map₂ f x y).get i = f (x.get i) (y.get i)) (i : Fin n.succ),
    (map₂ f (a ::ᵥ x) (b ::ᵥ y)).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
⊢ (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)

Tactic:
induction v₁, v₂ using inductionOn₂ with
  | nil =>
    exact Fin.elim0 i
  | cons ih =>
    rw [map₂_cons]
    cases i using Fin.cases
    · simp only [get_zero, head_cons]
    · simp only [get_cons_succ, ih]

Premises used: List.Vector.head_cons, List.Vector.map₂_cons, List.Vector.nil, List.Vector.get_cons_succ, List.Vector.get_zero, List.Vector.cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
n : ℕ
x : α
s : σ
xs : Vector α n
f : α → σ → σ × β
⊢ mapAccumr f (x ::ᵥ xs) s =
    let r := mapAccumr f xs s;
    let q := f x r.1;
    (q.1, q.2 ::ᵥ r.2)

Tactic:
rfl

Premises used: List.Vector.mapAccumr, List.Vector, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
n : ℕ
x : α
y : β
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
⊢ mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s =
    let r := mapAccumr₂ f xs ys s;
    let q := f x y r.1;
    (q.1, q.2 ::ᵥ r.2)

Tactic:
rfl

Premises used: List.Vector, List.Vector.mapAccumr₂, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n : ℕ
h : List.length.{u_1} (α := α) [] = n.succ
⊢ Eq.{u_1 + 1} (α := Vector α (n.succ - 1).succ)
    (cons (head (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) [] h))
      (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) [] h)))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) [] h)

Tactic:
contradiction
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n_1 : ℕ
p : α → Prop
n m : ℕ
l₁ : List α
h₁ : l₁.length = n
l₂ : List α
h₂ : l₂.length = m
⊢ (l₁ ++ l₂).length = n + m

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n m : ℕ
⊢ Eq (α := Vector α n → Vector α m → Vector α (n + m)) HAppend.hAppend fun (x : Vector α n) (x_1 : Vector α m) ↦
    match (motive := Vector α n → Vector α m → Vector α (n + m)) x, x_1 with
    | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n + m) (l₁ ++ l₂) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β
l : List α
h : l.length = n
⊢ (List.map f l).length = n

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f nil = nil

Tactic:
rfl

Premises used: List.map, List.Vector.map, List.Vector.nil, rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : (a : α) → p a → β
l : List α
h : l.length = n
hp : ∀ (x : α), x ∈ toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h) → p x
⊢ (List.pmap (P := p) f l hp).length = n

Tactic:
simp [h]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hp : ∀ (x : α), Membership.mem (γ := List α) (toList nil) x → p x
⊢ pmap (p := p) f nil hp = nil

Tactic:
rfl

Premises used: List.Vector.pmap, List.pmap, List.Vector.nil, rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → φ
x : List α
property : x.length = n
y : List β
property_1 : y.length = n
⊢ (zipWith f x y).length = n

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.drop i l).length = n - i

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.take i l).length = min i n

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
rw : l.length - 1 = n - 1
rw₁ : (↑i : ℕ) < l.length
⊢ (l.eraseIdx (↑i : ℕ)).length = n - 1

Tactic:
rw [l.length_eraseIdx_of_lt]

Premises used: List.length_eraseIdx_of_lt
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
rw rw₁ : n - 1 = n - 1
⊢ l.length - 1 = n - 1

Tactic:
rw [p]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
rw : (↑i : ℕ) < n
⊢ (↑i : ℕ) < l.length

Tactic:
rw [p]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (↑i : ℕ) < n

Tactic:
i.2

Premises used: Fin.isLt
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (↑i : ℕ) < n

Tactic:
exact i.2

Premises used: Fin.isLt
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → σ → σ × β
x : List α
px : x.length = n
c : σ
res : Prod.{u_3, u_2} σ (List β) := List.mapAccumr f x c
⊢ res.snd.length = n

Tactic:
simp [*, res]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → σ → σ × φ
x : List α
px : x.length = n
y : List β
py : y.length = n
c : σ
res : Prod.{u_3, u_4} σ (List φ) := List.mapAccumr₂ f x y c
⊢ res.snd.length = n

Tactic:
simp [*, res]
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ n - i + min n i = n

Tactic:
simp
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ min n i + min (n - i) n = n

Tactic:
omega
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
v : Vector α 0
⊢ v = nil

Tactic:
v.eq nil (List.eq_nil_of_length_eq_zero v.2)

Premises used: List.Vector.eq, List.eq_nil_of_length_eq_zero, List.Vector.nil, Subtype.property
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n : ℕ
v : List α
P : v.length = n
⊢ toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) v P) = v

Tactic:
rfl

Premises used: List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (toList nil) []

Tactic:
rfl

Premises used: List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ v.toList.length = n

Tactic:
v.2

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

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
⊢ toList (n := n.succ) (cons a (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) =
    a :: toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n m : ℕ
v : Vector α n
w : Vector α m
⊢ (v ++ w).toList = v.toList ++ w.toList

Tactic:
rfl

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

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

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n m : ℕ
v : Vector α m
mk :
  ∀ (val : List α) (property : val.length = m),
    toList (n := min n m) (take n (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property)) =
      List.take n (toList (n := m) (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property))
⊢ (take n v).toList = List.take n v.toList

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n m : ℕ
val : List α
property : val.length = m
⊢ toList (n := min n m) (take n (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property)) =
    List.take n (toList (n := m) (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property))

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < n
⊢ i < v.toList.length

Tactic:
simpa
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i : ℕ
hi : i < n
⊢ getElem (valid := fun (x : Vector α n) (i : ℕ) ↦ i < n) v i hi =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v.toList i ⋯

Tactic:
rfl

Premises used: List.Vector.get, List.Vector.toList, rfl