awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (snoc nil x) s =
    let q := f x s;
    let r := mapAccumr f nil q.1;
    (r.1, r.2.snoc q.2)

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
n_1 : ℕ
x_1 : α
w : Vector α n_1
h :
  mapAccumr f (w.snoc x) s =
    let q := f x s;
    let r := mapAccumr f w q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f ((x_1 ::ᵥ w).snoc x) s =
    let q := f x s;
    let r := mapAccumr f (x_1 ::ᵥ w) q.1;
    (r.1, r.2.snoc q.2)

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
nil : map₂ f (snoc Vector.nil x) (snoc Vector.nil y) = (map₂ f Vector.nil Vector.nil).snoc (f x y)
cons :
  ∀ {n : ℕ} {a : α} {b : β} {x_1 : Vector α n} {y_1 : Vector β n},
    map₂ f (x_1.snoc x) (y_1.snoc y) = (map₂ f x_1 y_1).snoc (f x y) →
      map₂ f ((a ::ᵥ x_1).snoc x) ((b ::ᵥ y_1).snoc y) = (map₂ f (a ::ᵥ x_1) (b ::ᵥ y_1)).snoc (f x y)
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)

Tactic:
induction xs, ys using Vector.inductionOn₂
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (snoc nil x) (snoc nil y) = (map₂ f nil nil).snoc (f x y)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
n_1 : ℕ
a : α
b : β
x_1 : Vector α n_1
y_1 : Vector β n_1
h : map₂ f (x_1.snoc x) (y_1.snoc y) = (map₂ f x_1 y_1).snoc (f x y)
⊢ map₂ f ((a ::ᵥ x_1).snoc x) ((b ::ᵥ y_1).snoc y) = (map₂ f (a ::ᵥ x_1) (b ::ᵥ y_1)).snoc (f x y)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
s : σ
f : α → β → σ → σ × φ
⊢ mapAccumr₂ f nil nil s = (s, nil)

Tactic:
rfl

Premises used: List.Vector.mapAccumr₂, List.Vector.nil, rfl
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
nil :
  mapAccumr₂ f (snoc Vector.nil x) (snoc Vector.nil y) s =
    let q := f x y s;
    let r := mapAccumr₂ f Vector.nil Vector.nil q.1;
    (r.1, r.2.snoc q.2)
cons :
  ∀ {n : ℕ} {a : α} {b : β} {x_1 : Vector α n} {y_1 : Vector β n},
    (mapAccumr₂ f (x_1.snoc x) (y_1.snoc y) s =
        let q := f x y s;
        let r := mapAccumr₂ f x_1 y_1 q.1;
        (r.1, r.2.snoc q.2)) →
      mapAccumr₂ f ((a ::ᵥ x_1).snoc x) ((b ::ᵥ y_1).snoc y) s =
        let q := f x y s;
        let r := mapAccumr₂ f (a ::ᵥ x_1) (b ::ᵥ y_1) q.1;
        (r.1, r.2.snoc q.2)
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f xs ys q.1;
    (r.1, r.2.snoc q.2)

Tactic:
induction xs, ys using Vector.inductionOn₂
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (snoc nil x) (snoc nil y) s =
    let q := f x y s;
    let r := mapAccumr₂ f nil nil q.1;
    (r.1, r.2.snoc q.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
n_1 : ℕ
a : α
b : β
x_1 : Vector α n_1
y_1 : Vector β n_1
h :
  mapAccumr₂ f (x_1.snoc x) (y_1.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f x_1 y_1 q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr₂ f ((a ::ᵥ x_1).snoc x) ((b ::ᵥ y_1).snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f (a ::ᵥ x_1) (b ::ᵥ y_1) q.1;
    (r.1, r.2.snoc q.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (List.zipWith f (↑x : List α) (↑y : List β)).length = n

Tactic:
simp
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (zipWith f x y).toList = List.zipWith f x.toList y.toList

Tactic:
rfl

Premises used: List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
dsimp :
  (List.zipWith f (↑x : List α) (↑y : List β)).get
      (Fin.cast ⋯ i : Fin (List.zipWith f (↑x : List α) (↑y : List β)).length) =
    f ((↑x : List α).get (Fin.cast ⋯ i)) ((↑y : List β).get (Fin.cast ⋯ i))
⊢ (zipWith f x y).get i = f (x.get i) (y.get i)

Tactic:
dsimp only [Vector.zipWith, Vector.get]

Premises used: List.Vector.get, List.Vector.zipWith
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (List.zipWith f (↑x : List α) (↑y : List β)).get
      (Fin.cast ⋯ i : Fin (List.zipWith f (↑x : List α) (↑y : List β)).length) =
    f ((↑x : List α).get (Fin.cast ⋯ i)) ((↑y : List β).get (Fin.cast ⋯ i))

Tactic:
simp
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
x₁ : ∀ (m : Fin (n - 1)), (zipWith f x y).tail.get m = (zipWith f x.tail y.tail).get m
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail

Tactic:
ext
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m : Fin (n - 1)
⊢ (zipWith f x y).tail.get m = (zipWith f x.tail y.tail).get m

Tactic:
simp [get_tail]

Premises used: List.Vector.get_tail
-- Module: Mathlib.Data.Vector.Zip
Goal:
α : Type u_1
n : ℕ
inst : CommMonoid α
x y : Vector α n
⊢ x.toList.prod * y.toList.prod = prod (toList (zipWith (fun (x1 x2 : α) ↦ x1 * x2) x y))

Tactic:
List.prod_mul_prod_eq_prod_zipWith_of_length_eq x.toList y.toList
    ((toList_length x).trans (toList_length y).symm)

Premises used: List.Vector.toList_length, List.prod_mul_prod_eq_prod_zipWith_of_length_eq, Eq.symm, List.Vector.toList, Eq.trans
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
refine_1 : α
refine_2 : (n : Fin2 n) → α
⊢ α

Tactic:
refine i.cases' ?_ ?_
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
⊢ α

Tactic:
exact a
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
⊢ (n : Fin2 n) → α

Tactic:
exact v
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ (a :: v) fz = a

Tactic:
rfl

Premises used: Vector3.cons, Fin2.cases', rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
i : Fin2 n
⊢ (a :: v) i.fs = v i

Tactic:
rfl

Premises used: Vector3.cons, Fin2.cases', rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
v : Vector3 α 0
⊢ v = []

Tactic:
funext fun i => nomatch i

Premises used: Vector3.nil, funext, Vector3, Eq, _private.0.Vector3.eq_nil.match_1
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
v : Vector3 α (n + 1)
⊢ (v.head :: v.tail) = v

Tactic:
funext fun i => Fin2.cases' rfl (fun _ => rfl) i

Premises used: funext, Vector3, Fin2.cases'
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
rw : C []
⊢ C v

Tactic:
rw [eq_nil v]

Premises used: Vector3.eq_nil
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
C : Vector3 α 0 → Sort u
H : C []
v : Vector3 α 0
⊢ C []

Tactic:
apply H
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
rw : C (v.head :: v.tail)
⊢ C v

Tactic:
rw [← cons_head_tail v]

Premises used: Vector3.cons_head_tail
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
C : Vector3 α (n + 1) → Sort u
H : (a : α) → (t : Vector3 α n) → C (a :: t)
v : Vector3 α (n + 1)
⊢ C (v.head :: v.tail)

Tactic:
apply H
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
C : Vector3 α (n + 1) → Sort u_2
H : (a : α) → (t : Vector3 α n) → C (a :: t)
a : α
t : Vector3 α n
⊢ consElim (C := C) H (a :: t) = H a t

Tactic:
rfl

Premises used: Eq.mpr, Vector3.consElim, Vector3.cons, Fin2.cases', Vector3.tail, Vector3.head, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
C : {n : ℕ} → Vector3 α n → Sort u_2
H0 : C []
Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (a :: w)
⊢ Vector3.recOn (C := @C) [] H0 @Hs = H0

Tactic:
rfl

Premises used: Eq.mpr, Vector3.recOn, Vector3.nilElim, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
C : {n : ℕ} → Vector3 α n → Sort u_2
H0 : C []
Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (a :: w)
n : ℕ
a : α
v : Vector3 α n
⊢ (a :: v).recOn (C := @C) H0 @Hs = Hs a v (v.recOn (C := @C) H0 @Hs)

Tactic:
rfl

Premises used: Eq.mpr, Vector3.recOn, Vector3.consElim, Vector3.cons, Fin2.cases', Vector3.tail, Vector3.head, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
w : Vector3 α n
⊢ [] +-+ w = w

Tactic:
rfl

Premises used: Eq.mpr, Vector3.recOn, Vector3.nilElim, Vector3.append, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
v : Vector3 α m
w : Vector3 α n
⊢ (a :: v) +-+ w = a :: v +-+ w

Tactic:
rfl

Premises used: Vector3.recOn, Vector3.consElim, Vector3.cons, Fin2.cases', Vector3.tail, Vector3.append, Vector3.head, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m : ℕ
v : Vector3 α (m + 1)
x : ℕ
x_1 : Vector3 α x
a : α
_t : Vector3 α m
⊢ ((a :: _t) +-+ x_1) (left x fz) = (a :: _t) fz

Tactic:
simp [*, left]

Premises used: Fin2.left
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m : ℕ
i : Fin2 m
v : Vector3 α (m + 1)
n : ℕ
w : Vector3 α n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (left n i.fs) = (_a :: t) i.fs

Tactic:
simp [append_left, left]

Premises used: Fin2.left
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m : ℕ
v : Vector3 α (m + 1)
n : ℕ
w : Vector3 α n
i : Fin2 n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (i.add (m + 1)) = w i

Tactic:
simp [append_add, add]

Premises used: Fin2.add
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v

Tactic:
funext fun j => j.cases' ?_ ?_

Premises used: funext, Vector3, Fin2.cases'
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
refine_1 : ∀ (j : Fin2 (n + 1)), insert a v fz fz = (a :: v) fz
refine_2 : ∀ (j : Fin2 (n + 1)) (n_1 : Fin2 n), insert a v fz n_1.fs = (a :: v) n_1.fs
⊢ insert a v fz = a :: v

Tactic:
refine funext fun j => j.cases' ?_ ?_

Premises used: funext
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

Tactic:
rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
n_1 : Fin2 n
⊢ insert a v fz n_1.fs = (a :: v) n_1.fs

Tactic:
rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j : Fin2 (n + 1 + 1)
⊢ insert a (b :: v) i.fs fz = (b :: insert a v i) fz

Tactic:
simp [insert, insertPerm]

Premises used: Vector3.insert, Fin2.insertPerm
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j : Fin2 (n + 1 + 1)
refine : ∀ (j : Fin2 (n + 1)), insert a (b :: v) i.fs j.fs = (b :: insert a v i) j.fs
⊢ insert a (b :: v) i.fs j = (b :: insert a v i) j

Tactic:
refine j.cases' (by simp [insert, insertPerm]) fun j => ?_
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j_1 : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
simp :
  (a :: b :: v)
      (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) i.insertPerm j with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) (i.insertPerm j)
⊢ insert a (b :: v) i.fs j.fs = (b :: insert a v i) j.fs

Tactic:
simp only [insert, insertPerm, succ_eq_add_one, cons_fs]

Premises used: Nat.succ_eq_add_one, Vector3.cons_fs, Vector3.insert, Fin2.insertPerm
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j_1 : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) i.insertPerm j with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) (i.insertPerm j)

Tactic:
Fin2.cases' ?_ ?_ (insertPerm i j)

Premises used: Fin2.insertPerm, Fin2.cases'
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j_1 : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
refine_1 :
  (a :: b :: v)
      (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) fz with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) fz
refine_2 :
  ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) n_1.fs with
        | fz => fz
        | k.fs => k.fs.fs) =
      (a :: v) n_1.fs
⊢ (a :: b :: v)
      (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) i.insertPerm j with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) (i.insertPerm j)

Tactic:
refine Fin2.cases' ?_ ?_ (insertPerm i j)
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j_1 : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) fz with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) fz

Tactic:
simp
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j_1 : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n),
    (a :: b :: v)
        (match (motive := Fin2 (n + 1) → Fin2 (n + 1 + 1)) n_1.fs with
        | fz => fz
        | k.fs => k.fs.fs) =
      (a :: v) n_1.fs

Tactic:
simp
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
⊢ insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + m = x) ↦ Fin2 x) e (i.add m)) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + m = x) ↦ Vector3 α x) e (t +-+ insert a v i)

Tactic:
Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e

Premises used: Vector3.recOn
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
refine_1 :
  ∀ (e : n + 1 + 0 = n + 0 + 1),
    insert a ([] +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + 0 = x) ↦ Fin2 x) e (i.add 0)) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + 0 = x) ↦ Vector3 α x) e ([] +-+ insert a v i)
refine_2 :
  ∀ (k : ℕ) (b : α) (t : Vector3 α k)
    (IH :
      ∀ (x : n + 1 + k = n + k + 1),
        insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) x (i.add k)) =
          Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Vector3 α x) x (t +-+ insert a v i))
    (x : n + 1 + (k + 1) = n + (k + 1) + 1),
    insert a ((b :: t) +-+ v)
        (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + (k + 1) = x) ↦ Fin2 x) x (i.add (k + 1))) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + (k + 1) = x) ↦ Vector3 α x) x ((b :: t) +-+ insert a v i)
⊢ insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + m = x) ↦ Fin2 x) e (i.add m)) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + m = x) ↦ Vector3 α x) e (t +-+ insert a v i)

Tactic:
refine Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e_1 : n + 1 + m = n + m + 1
e : n + 1 + 0 = n + 0 + 1
⊢ insert a ([] +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + 0 = x) ↦ Fin2 x) e (i.add 0)) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + 0 = x) ↦ Vector3 α x) e ([] +-+ insert a v i)

Tactic:
rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t_1 : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH :
  ∀ (x : n + 1 + k = n + k + 1),
    insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) x (i.add k)) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Vector3 α x) x (t +-+ insert a v i)
h : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ n + 1 + k = n + k + 1

Tactic:
lia
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t_1 : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH :
  ∀ (x : n + 1 + k = n + k + 1),
    insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) x (i.add k)) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Vector3 α x) x (t +-+ insert a v i)
h : n + 1 + (k + 1) = n + (k + 1) + 1
⊢ n + 1 + k = n + k + 1

Tactic:
have e' : (n + 1) + k = (n + k) + 1 := by lia
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t_1 : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH :
  ∀ (x : n + 1 + k = n + k + 1),
    insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) x (i.add k)) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Vector3 α x) x (t +-+ insert a v i)
h : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
refine_2 :
  insert a (b :: t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Fin2 x) ⋯ (i.add k).fs) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Vector3 α x) ⋯ (b :: t +-+ insert a v i)
⊢ insert a ((b :: t) +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + (k + 1) = x) ↦ Fin2 x) h (i.add (k + 1))) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + (k + 1) = x) ↦ Vector3 α x) h ((b :: t) +-+ insert a v i)

Tactic:
change
    insert a (b :: t +-+ v)
      (Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (fs (add i k))) =
      Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (b :: t +-+ insert a v i)

Premises used: Eq.recOn, Vector3.insert, congr_arg, Vector3.cons, HAdd.hAdd, OfNat.ofNat, Vector3.append
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t_1 : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH :
  ∀ (x : n + 1 + k = n + k + 1),
    insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) x (i.add k)) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Vector3 α x) x (t +-+ insert a v i)
h : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
refine_2 :
  insert a (b :: t +-+ v) (fs (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) e' (i.add k))) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Vector3 α x) ⋯ (b :: t +-+ insert a v i)
⊢ insert a (b :: t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Fin2 x) ⋯ (i.add k).fs) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Vector3 α x) ⋯ (b :: t +-+ insert a v i)

Tactic:
rw [← (Eq.recOn e' rfl :
      fs (Eq.recOn e' (i.add k) : Fin2 ((n + k) + 1)) =
        Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (fs (i.add k)))]

Premises used: Eq.recOn
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
m n : ℕ
a : α
t_1 : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH :
  ∀ (x : n + 1 + k = n + k + 1),
    insert a (t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) x (i.add k)) =
      Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Vector3 α x) x (t +-+ insert a v i)
h : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a (b :: t +-+ v) (fs (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k = x) ↦ Fin2 x) e' (i.add k))) =
    Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Vector3 α x) ⋯ (b :: t +-+ insert a v i)

Tactic:
simpa [IH] using Eq.recOn e' rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
f : Vector3 α 0 → Prop
h : Exists f
v : Vector3 α 0
fv rw : f v
⊢ f []

Tactic:
rw [← eq_nil v]

Premises used: Vector3.eq_nil
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
f : Vector3 α 0 → Prop
h : Exists f
v : Vector3 α 0
fv : f v
⊢ f v

Tactic:
fv
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
f : Vector3 α 0 → Prop
h : Exists f
v : Vector3 α 0
fv : f v
⊢ f v

Tactic:
exact fv
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
h : Exists f
v : Vector3 α n.succ
fv rw : f v
⊢ f (v.head :: v.tail)

Tactic:
rw [cons_head_tail v]

Premises used: Vector3.cons_head_tail
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
h : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v

Tactic:
fv
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
h : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v

Tactic:
exact fv
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
p : α → Prop
⊢ VectorAllP p [] = True

Tactic:
rfl

Premises used: Eq.mpr, Vector3.recOn, Vector3.nilElim, VectorAllP, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
p : α → Prop
x : α
⊢ VectorAllP p (x :: []) = p x

Tactic:
rfl

Premises used: Eq.mpr, Vector3.recOn, Vector3.consElim, Vector3.cons, Vector3.nilElim, Fin2.cases', Vector3.head, VectorAllP, rfl
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
x : α
v : Vector3 α n
⊢ VectorAllP p (x :: v) ↔ p x ∧ VectorAllP p v

Tactic:
Vector3.recOn v (iff_of_eq (and_true _)).symm fun _ _ _ => Iff.rfl

Premises used: Vector3.recOn
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)

Tactic:
v.recOn ?_ ?_

Premises used: Vector3.recOn
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
refine_1 : VectorAllP p [] ↔ ∀ (i : Fin2 0), p []
refine_2 :
  ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)

Tactic:
refine v.recOn ?_ ?_
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []

Tactic:
⟨fun _ => Fin2.elim0, fun _ => trivial⟩

Premises used: trivial, Fin2.elim0, Iff.intro
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []

Tactic:
exact ⟨fun _ => Fin2.elim0, fun _ => trivial⟩
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
refine_2 :
  ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (p a ∧ VectorAllP p w ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))

Tactic:
simp only [vectorAllP_cons]

Premises used: vectorAllP_cons
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h_1 : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) i)

Tactic:
i.cases' ?_ ?_

Premises used: Fin2.cases'
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h_1 : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
refine_1 : p ((a :: v) fz)
refine_2 : ∀ (n_2 : Fin2 n), p ((a :: v) n_2.fs)
⊢ p ((a :: v) i)

Tactic:
refine i.cases' ?_ ?_
-- Module: Mathlib.Data.Vector3
Goal:
α : Type u_1
n_1 : ℕ
p : α → Prop
v_1 : Vector3 α n_1
n : ℕ
a : α
v : Vector3 α n
IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
h_1 : p a ∧ ∀ (i : Fin2 n), p (v i)
i : Fin2 (n + 1)
pa : p a
h : ∀ (i : Fin2 n), p (v i)
⊢ p ((a :: v) fz)

Tactic:
pa

Premises used: Vector3.cons, Fin2.cases'