awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
⊢ Eq (α := Vector α (n + 1)) (reverse (snoc (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) x))
    (x ::ᵥ reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
have mk : Eq (α := Vector α (n + 1))
  (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
    (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
          (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] sorry)).toList.reverse
    sorry)
  (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (x :: val.reverse) sorry)
Tactic: simp only [reverse, snoc, cons, toList_mk]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
⊢ Eq (α := Vector α (n + 1))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
            (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)).toList.reverse
      ⋯)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (x :: val.reverse) ⋯)
have mk : (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] sorry)).toList.reverse =
  x :: val.reverse
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
| Eq (α := Vector α (n + 1 + 1)) (val ::ᵥ replicate (n + 1) val) (snoc (replicate (n + 1) val) val)
have rhs : snoc (replicate (n + 1) val) val
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
| Eq (α := Vector α (n + 1 + 1)) (val ::ᵥ replicate (n + 1) val) (snoc (replicate (n + 1) val) val)
have rw : (val ::ᵥ replicate n val).snoc val
Tactic: rhs; rw [replicate_succ]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (val ::ᵥ replicate n val).snoc val
have succ : val ::ᵥ replicate (n + 1) val = val ::ᵥ (replicate n val).snoc val
Tactic: rw [snoc_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
succ : val ::ᵥ replicate (n + 1) val = val ::ᵥ (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (val ::ᵥ replicate n val).snoc val
have succ₁ : val ::ᵥ (replicate n val).snoc val = val ::ᵥ (replicate n val).snoc val
Tactic: rw [snoc_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = (replicate n val).snoc val
have zero : Eq (α := Vector α (HAdd.hAdd (α := ℕ) 0 1)) (replicate (HAdd.hAdd (α := ℕ) 0 1) val) (snoc (replicate 0 val) val)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [replicate_succ]
    conv => rhs; rw [replicate_succ]
    rw [snoc_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
val : α
zero : Eq (α := Vector α (HAdd.hAdd (α := ℕ) 0 1)) (replicate (HAdd.hAdd (α := ℕ) 0 1) val) (snoc (replicate 0 val) val)
⊢ replicate (n + 1) val = (replicate n val).snoc val
have succ : ∀ (n : ℕ) (ih : replicate (n + 1) val = (replicate n val).snoc val),
  Eq (α := Vector α (n + 1 + 1)) (replicate (n + 1 + 1) val) (snoc (replicate (n + 1) val) val)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [replicate_succ]
    conv => rhs; rw [replicate_succ]
    rw [snoc_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (xs.snoc x) = (map f xs).snoc (f x)
have nil : map f (snoc nil x) = (map f nil).snoc (f x)
Tactic: induction xs
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
nil : map f (snoc Vector.nil x) = (map f Vector.nil).snoc (f x)
⊢ map f (xs.snoc x) = (map f xs).snoc (f x)
have cons : ∀ {n : ℕ} {x_1 : α} {w : Vector α n},
  map f (w.snoc x) = (map f w).snoc (f x) → map f ((x_1 ::ᵥ w).snoc x) = (map f (x_1 ::ᵥ w)).snoc (f x)
Tactic: induction xs
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
⊢ mapAccumr f (xs.snoc x) s =
    let q := f x s;
    let r := mapAccumr f xs q.1;
    (r.1, r.2.snoc q.2)
have nil : 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: induction xs
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
nil :
  mapAccumr f (snoc Vector.nil x) s =
    let q := f x s;
    let r := mapAccumr f Vector.nil q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr f (xs.snoc x) s =
    let q := f x s;
    let r := mapAccumr f xs q.1;
    (r.1, r.2.snoc q.2)
have cons : ∀ {n : ℕ} {x_1 : α} {w : Vector α n},
  (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: induction xs
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)
have nil : map₂ f (snoc nil x) (snoc nil y) = (map₂ f nil nil).snoc (f x y)
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
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)
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)
have 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)
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
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 (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)
have nil : 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: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
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)
⊢ 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)
have 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)
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.Zip (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
i : Fin n
⊢ (zipWith f x y).get i = f (x.get i) (y.get i)
have dsimp : (List.zipWith f (↑x : List α) (↑y : List β)).get
    (Fin.cast sorry i : Fin (List.zipWith f (↑x : List α) (↑y : List β)).length) =
  f ((↑x : List α).get (Fin.cast sorry i)) ((↑y : List β).get (Fin.cast sorry i))
Tactic: dsimp only [Vector.zipWith, Vector.get]
-- Lean 4 proof step from Mathlib.Data.Vector.Zip (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail
have x₁ : ∀ (m : Fin (n - 1)), (zipWith f x y).tail.get m = (zipWith f x.tail y.tail).get m
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
m n : ℕ
a : α
v : Vector3 α n
i : Fin2 (n + 1)
refine_1 : α
⊢ α
have refine_2 : (n : Fin2 n) → α
Tactic: refine i.cases' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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
have rw : C (v.head :: v.tail)
Tactic: rw [← cons_head_tail v]
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
⊢ insert a v fz = a :: v
have refine_1 : ∀ (j : Fin2 (n + 1)), insert a v fz fz = (a :: v) fz
Tactic: refine funext fun j => j.cases' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
refine_1 : ∀ (j : Fin2 (n + 1)), insert a v fz fz = (a :: v) fz
⊢ insert a v fz = a :: v
have refine_2 : ∀ (j : Fin2 (n + 1)) (n_1 : Fin2 n), insert a v fz n_1.fs = (a :: v) n_1.fs
Tactic: refine funext fun j => j.cases' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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 j = (b :: insert a v i) j
have refine : ∀ (j : Fin2 (n + 1)), insert a (b :: v) i.fs j.fs = (b :: insert a v i) j.fs
Tactic: refine j.cases' (by simp [insert, insertPerm]) fun j => ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j_1 : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ insert a (b :: v) i.fs j.fs = (b :: insert a v i) j.fs
have 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)
Tactic: simp only [insert, insertPerm, succ_eq_add_one, cons_fs]
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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)
have 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
Tactic: refine Fin2.cases' ?_ ?_ (insertPerm i j)
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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
⊢ (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)
have 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
Tactic: refine Fin2.cases' ?_ ?_ (insertPerm i j)
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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)
have 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)
Tactic: refine Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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)
⊢ 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)
have 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)
Tactic: refine Vector3.recOn t (fun e => ?_) (@fun k b t IH _ => ?_) e
-- Lean 4 proof step from Mathlib.Data.Vector3 (hypothesis)
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
⊢ 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)
have e' : n + 1 + k = n + k + 1
Tactic: have e' : (n + 1) + k = (n + k) + 1 := by lia
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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) (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)
have refine_2 : insert a (b :: t +-+ v) (Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Fin2 x) sorry (i.add k).fs) =
  Eq.recOn (motive := fun (x : ℕ) (x_1 : n + 1 + k + 1 = x) ↦ Vector3 α x) sorry (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)
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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) (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)
have 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) sorry (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)))]
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
have refine_1 : VectorAllP p [] ↔ ∀ (i : Fin2 0), p []
Tactic: refine v.recOn ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
refine_1 : VectorAllP p [] ↔ ∀ (i : Fin2 0), p []
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)
have 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))
Tactic: refine v.recOn ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {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))
have 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))
Tactic: simp only [vectorAllP_cons]
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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)
have refine_1 : p ((a :: v) fz)
Tactic: refine i.cases' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
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)
⊢ p ((a :: v) i)
have refine_2 : ∀ (n_2 : Fin2 n), p ((a :: v) n_2.fs)
Tactic: refine i.cases' ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {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))
have refine_2 : ∀ {n : ℕ} (a : α) (v : Vector3 α n) (IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i))
  (h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)), p a
Tactic: refine fun {n} a v IH =>
      (and_congr_right fun _ => IH).trans
        ⟨fun ⟨pa, h⟩ i => by
          refine i.cases' ?_ ?_
          exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Vector3 (goal)
Goal:
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
refine_2 :
  ∀ {n : ℕ} (a : α) (v : Vector3 α n) (IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i))
    (h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)), p a
⊢ ∀ {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))
have refine_2₁ : ∀ {n : ℕ} (a : α) (v : Vector3 α n) (IH : VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i))
  (h : ∀ (i : Fin2 (n + 1)), p ((a :: v) i)) (i : Fin2 n), p (v i)
Tactic: refine fun {n} a v IH =>
      (and_congr_right fun _ => IH).trans
        ⟨fun ⟨pa, h⟩ i => by
          refine i.cases' ?_ ?_
          exacts [pa, h], fun h => ⟨?_, fun i => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType β
a₂ : α
f₂ : β a₂ → WType β
h : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₂ f₂)
⊢ mk (β := β) a₁ f₁ = mk (β := β) a₂ f₂
have obtain : ∀ (f₂ : β a₁ → WType β) (h : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₁ f₂))
  (h :
    HEq (α := β a₁ → γ) fun (b : β a₁) ↦ elim (β := β) γ fγ (f₁ b) (β := β a₁ → γ) fun (b : β a₁) ↦
      elim (β := β) γ fγ (f₂ b)),
  mk (β := β) a₁ f₁ = mk (β := β) a₁ f₂
Tactic: obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
Cleared hypotheses: a₂, f₂, h
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType β
h_1 : elim (β := β) γ fγ (mk (β := β) a₁ f₁) = elim (β := β) γ fγ (mk (β := β) a₁ f₂)
h :
  HEq (α := β a₁ → γ) fun (b : β a₁) ↦ elim (β := β) γ fγ (f₁ b) (β := β a₁ → γ) fun (b : β a₁) ↦
    elim (β := β) γ fγ (f₂ b)
⊢ mk (β := β) a₁ f₁ = mk (β := β) a₁ f₂
have e_f : ∀ (x : β a₁), f₁ x = f₂ x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Data.W.Basic (hypothesis)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
⊢ False
have hba : b ≠ a
Tactic: have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False
have n : Function.Injective (β := WType β) fun (n : ℕ) ↦
  have this : WType β :=
    Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
      mk (β := β) a fun (x : β a) ↦ ih;
  this
Tactic: refine
      not_injective_infinite_finite
        (fun n : ℕ =>
          show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩)
        ?_
-- Lean 4 proof step from Mathlib.Data.W.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty.{u_2 + 1} (β a)
he : IsEmpty.{u_2 + 1} (β b)
hf : Finite (WType β)
hba : b ≠ a
m : ℕ
h :
  Eq (α := WType β)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      0)
    ((fun (n : ℕ) ↦
        have this : WType β :=
          Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
            mk (β := β) a fun (x : β a) ↦ ih;
        this)
      m)
⊢ 0 = m
have zero : ∀
  (h :
    Eq (α := WType β)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        0)
      ((fun (n : ℕ) ↦
          have this : WType β :=
            Nat.recOn (motive := fun (x : ℕ) ↦ WType β) n (mk (β := β) b he.elim') fun (x : ℕ) (ih : WType β) ↦
              mk (β := β) a fun (x : β a) ↦ ih;
          this)
        0)),
  Eq (α := ℕ) 0 0
Tactic: rcases m with - | m
Cleared hypotheses: m, h