awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property) v w
have succ : (v_property : List.length.{u_6} (α := β) [] = n + 1) →
  C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) [] v_property) w
Tactic: rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (n + 1)
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
succ :
  (v_property : List.length.{u_6} (α := β) [] = n + 1) →
    C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
      (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) [] v_property) w
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property) v w
have succ₁ : (b : β) →
  (v : List β) →
    (v_property : (b :: v).length = n + 1) →
      C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
        (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property) w
Tactic: rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property) w
have succ : (w_property : List.length.{u_7} (α := γ) [] = n + 1) →
  C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
    (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) [] w_property)
Tactic: rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
succ :
  (w_property : List.length.{u_7} (α := γ) [] = n + 1) →
    C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
      (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
      (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) [] w_property)
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property) w
have succ₁ : (c : γ) →
  (w : List γ) →
    (w_property : (c :: w).length = n + 1) →
      C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
        (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
        (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) (c :: w) w_property)
Tactic: rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
c : γ
w : List γ
w_property : (c :: w).length = n + 1
⊢ C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
    (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) (c :: w) w_property)
have succ : C (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) u sorry)
  (Subtype.mk (p := fun (l : List β) ↦ l.length = n) v sorry) (Subtype.mk (p := fun (l : List γ) ↦ l.length = n) w sorry)
Tactic: apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C u v w
have zero : (u : Vector α 0) → (v : Vector β 0) → (w : Vector γ 0) → C u v w
Tactic: induction n with
  | zero =>
    rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
    cases u_property
    rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
    cases w_property
    apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih
Cleared hypotheses: u, v, w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
zero : (u : Vector α 0) → (v : Vector β 0) → (w : Vector γ 0) → C u v w
⊢ C u v w
have succ : (n : ℕ) →
  (ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w) →
    (u : Vector α (n + 1)) → (v : Vector β (n + 1)) → (w : Vector γ (n + 1)) → C u v w
Tactic: induction n with
  | zero =>
    rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
    cases u_property
    rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
    cases w_property
    apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih
Cleared hypotheses: u, v, w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a_1 a : α
i : Fin (n + 1)
v : Vector α n
⊢ ((↑v : List α).insertIdx (↑i : ℕ) a).length = n + 1
have rw : (if (↑i : ℕ) ≤ n then n + 1 else n) = n + 1
Tactic: rw [List.length_insertIdx, v.2]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a_1 a : α
i : Fin (n + 1)
v : Vector α n
⊢ (if (↑i : ℕ) ≤ n then n + 1 else n) = n + 1
have isTrue : (↑i : ℕ) ≤ n → n + 1 = n + 1
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a_1 a : α
i : Fin (n + 1)
v : Vector α n
isTrue : (↑i : ℕ) ≤ n → n + 1 = n + 1
⊢ (if (↑i : ℕ) ≤ n then n + 1 else n) = n + 1
have isFalse : ¬(↑i : ℕ) ≤ n → n = n + 1
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ eraseIdx ((⟨j, hj⟩ : Fin (n + 2)).succAbove (⟨i, hi⟩ : Fin (n + 1))) (insertIdx a (⟨j, hj⟩ : Fin (n + 2)) v) =
    insertIdx a (⟨i, hi⟩.predAbove ⟨j, hj⟩) (eraseIdx ⟨i, hi⟩ v)
have dsimp : Eq (α := Vector α (n + 1))
  (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
    (((↑v : List α).insertIdx j a).eraseIdx
      (↑(if (⟨i, sorry⟩ : Fin (n + 1 + 1)) < (⟨j, hj⟩ : Fin (n + 2)) then (⟨i, sorry⟩ : Fin (n + 1 + 1))
          else (⟨i + 1, sorry⟩ : Fin (n + 1 + 1))) :
        ℕ))
    sorry)
  (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
    (List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
        List α)
      (↑(if h : (⟨i, sorry⟩ : Fin (n + 1 + 1)) < ⟨j, hj⟩ then ⟨j, hj⟩.pred sorry else ⟨j, hj⟩.castPred sorry) : ℕ) a)
    sorry)
Tactic: dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ Eq (α := Vector α (n + 1))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (((↑v : List α).insertIdx j a).eraseIdx
        (↑(if (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < (⟨j, hj⟩ : Fin (n + 2)) then (⟨i, ⋯⟩ : Fin (n + 1 + 1))
            else (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1))) :
          ℕ))
      ⋯)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (List.insertIdx
        (↑(match (motive := Vector α (n + 1) → Vector α n) v with
            | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
          List α)
        (↑(if h : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯) : ℕ) a)
      ⋯)
have rw : ((↑v : List α).insertIdx j a).eraseIdx
    (↑(if (⟨i, sorry⟩ : Fin (n + 1 + 1)) < (⟨j, hj⟩ : Fin (n + 2)) then (⟨i, sorry⟩ : Fin (n + 1 + 1))
        else (⟨i + 1, sorry⟩ : Fin (n + 1 + 1))) :
      ℕ) =
  List.insertIdx
    (↑(match (motive := Vector α (n + 1) → Vector α n) v with
        | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
      List α)
    (↑(if h : (⟨i, sorry⟩ : Fin (n + 1 + 1)) < ⟨j, hj⟩ then ⟨j, hj⟩.pred sorry else ⟨j, hj⟩.castPred sorry) : ℕ) a
Tactic: rw [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ((↑v : List α).insertIdx j a).eraseIdx
      (↑(if (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < (⟨j, hj⟩ : Fin (n + 2)) then (⟨i, ⋯⟩ : Fin (n + 1 + 1))
          else (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1))) :
        ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑(if h : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯) : ℕ) a
have simp : ((↑v : List α).insertIdx j a).eraseIdx
    (↑(if i < j then (⟨i, sorry⟩ : Fin (n + 1 + 1)) else (⟨i + 1, sorry⟩ : Fin (n + 1 + 1))) : ℕ) =
  List.insertIdx
    (↑(match (motive := Vector α (n + 1) → Vector α n) v with
        | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
      List α)
    (↑(if h : i < j then ⟨j, hj⟩.pred sorry else ⟨j, hj⟩.castPred sorry) : ℕ) a
Tactic: simp only [Fin.lt_def]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ((↑v : List α).insertIdx j a).eraseIdx
      (↑(if i < j then (⟨i, ⋯⟩ : Fin (n + 1 + 1)) else (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1))) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑(if h : i < j then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯) : ℕ) a
have pos : ∀ (hij : i < j),
  ((↑v : List α).insertIdx j a).eraseIdx (↑(⟨i, sorry⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
        List α)
      (↑((⟨j, hj⟩ : Fin (n + 2)).pred sorry) : ℕ) a
Tactic: split_ifs with hij
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
pos :
  ∀ (hij : i < j),
    ((↑v : List α).insertIdx j a).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) =
      List.insertIdx
        (↑(match (motive := Vector α (n + 1) → Vector α n) v with
            | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
          List α)
        (↑((⟨j, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
⊢ ((↑v : List α).insertIdx j a).eraseIdx
      (↑(if i < j then (⟨i, ⋯⟩ : Fin (n + 1 + 1)) else (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1))) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑(if h : i < j then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯) : ℕ) a
have neg : ∀ (hij : ¬i < j),
  ((↑v : List α).insertIdx j a).eraseIdx (↑(⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
        List α)
      (↑((⟨j, hj⟩ : Fin (n + 2)).castPred sorry) : ℕ) a
Tactic: split_ifs with hij
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ ((↑v : List α).insertIdx j a).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
have pos : ∀ (j : ℕ) (hj : j.succ < n + 2) (hij : i < j.succ),
  ((↑v : List α).insertIdx j.succ a).eraseIdx (↑(⟨i, sorry⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred sorry) : ℕ) a
Tactic: rcases Nat.exists_eq_succ_of_ne_zero
        (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v : List α).insertIdx j.succ a).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
have pos : ((↑v : List α).eraseIdx (↑(⟨i, sorry⟩ : Fin (n + 1 + 1)) : ℕ)).insertIdx j a =
  List.insertIdx
    (↑(match (motive := Vector α (n + 1) → Vector α n) v with
        | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
      List α)
    (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred sorry) : ℕ) a
Tactic: rw [← List.insertIdx_eraseIdx_of_ge]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
pos :
  ((↑v : List α).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ)).insertIdx j a =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
⊢ ((↑v : List α).insertIdx j.succ a).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
have pos₁ : (↑(⟨i, sorry⟩ : Fin (n + 1 + 1)) : ℕ) < (↑v : List α).length
Tactic: rw [← List.insertIdx_eraseIdx_of_ge]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
pos :
  ((↑v : List α).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ)).insertIdx j a =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
pos₁ : (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) < (↑v : List α).length
⊢ ((↑v : List α).insertIdx j.succ a).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
have pos₂ : (↑(⟨i, sorry⟩ : Fin (n + 1 + 1)) : ℕ) ≤ j
Tactic: rw [← List.insertIdx_eraseIdx_of_ge]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v : List α).eraseIdx (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ)).insertIdx j a =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j.succ, hj⟩ : Fin (n + 2)).pred ⋯) : ℕ) a
have pos : ((↑v : List α).eraseIdx i).insertIdx j a =
  List.insertIdx
    (↑(match (motive := Vector α (n + 1) → Vector α n) v with
        | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
      List α)
    j a
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v : List α).insertIdx j a).eraseIdx (↑(⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      (↑((⟨j, hj⟩ : Fin (n + 2)).castPred ⋯) : ℕ) a
have neg : ((↑v : List α).insertIdx j a).eraseIdx (i + 1) =
  List.insertIdx
    (↑(match (motive := Vector α (n + 1) → Vector α n) v with
        | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
      List α)
    j a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v : List α).insertIdx j a).eraseIdx (i + 1) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      j a
have neg : ((↑v : List α).eraseIdx i).insertIdx j a =
  List.insertIdx
    (↑(match (motive := Vector α (n + 1) → Vector α n) v with
        | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) sorry) :
      List α)
    j a
Tactic: rw [← List.insertIdx_eraseIdx_of_le]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
neg :
  ((↑v : List α).eraseIdx i).insertIdx j a =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      j a
⊢ ((↑v : List α).insertIdx j a).eraseIdx (i + 1) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      j a
have neg₁ : i < (↑v : List α).length
Tactic: rw [← List.insertIdx_eraseIdx_of_le]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
neg :
  ((↑v : List α).eraseIdx i).insertIdx j a =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      j a
neg₁ : i < (↑v : List α).length
⊢ ((↑v : List α).insertIdx j a).eraseIdx (i + 1) =
    List.insertIdx
      (↑(match (motive := Vector α (n + 1) → Vector α n) v with
          | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
        List α)
      j a
have neg₂ : j ≤ i
Tactic: rw [← List.insertIdx_eraseIdx_of_le]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ insertIdx b j.succ (insertIdx a i (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl)) =
    insertIdx a i.castSucc (insertIdx b j (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl))
have refine : (↑(insertIdx b j.succ (insertIdx a i (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl))) : List α) =
  (↑(insertIdx a i.castSucc (insertIdx b j (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl))) : List α)
Tactic: refine Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ (↑(insertIdx b j.succ (insertIdx a i (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl))) : List α) =
    (↑(insertIdx a i.castSucc (insertIdx b j (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l hl))) : List α)
have simp : (l.insertIdx (↑i : ℕ) a).insertIdx ((↑j : ℕ) + 1) b = (l.insertIdx (↑j : ℕ) b).insertIdx (↑i : ℕ) a
Tactic: simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.val_castAdd]