awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
rw :
  ((↑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
⊢ 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)
      ⋯)

Tactic:
rw [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
simp :
  ((↑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
⊢ ((↑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

Tactic:
simp only [Fin.lt_def]

Premises used: Fin.lt_def
-- Module: Mathlib.Data.Vector.Basic
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
neg :
  ∀ (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
⊢ ((↑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

Tactic:
split_ifs with hij
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
pos :
  ∀ (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
⊢ ((↑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

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⟩

Premises used: Nat.zero_le, lt_of_le_of_lt, Nat.pos_iff_ne_zero, Nat.exists_eq_succ_of_ne_zero, Iff.mp, rfl
-- Module: Mathlib.Data.Vector.Basic
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
pos₂ : (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) ≤ j
⊢ ((↑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

Tactic:
rw [← List.insertIdx_eraseIdx_of_ge]

Premises used: List.insertIdx_eraseIdx_of_ge
-- Module: Mathlib.Data.Vector.Basic
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).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 α).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

Tactic:
simp
-- Module: Mathlib.Data.Vector.Basic
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).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

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
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
⊢ (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) < (↑v : List α).length

Tactic:
simpa
-- Module: Mathlib.Data.Vector.Basic
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
⊢ (↑(⟨i, ⋯⟩ : Fin (n + 1 + 1)) : ℕ) ≤ j

Tactic:
simpa [Nat.lt_succ_iff] using hij

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Data.Vector.Basic
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 α).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
⊢ ((↑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

Tactic:
dsimp
-- Module: Mathlib.Data.Vector.Basic
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
neg₂ : j ≤ i
⊢ ((↑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

Tactic:
rw [← List.insertIdx_eraseIdx_of_le]

Premises used: List.insertIdx_eraseIdx_of_le
-- Module: Mathlib.Data.Vector.Basic
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 α).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

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v : List α).length

Tactic:
simpa
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
simpa [not_lt] using hij

Premises used: not_lt
-- Module: Mathlib.Data.Vector.Basic
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))

Tactic:
Subtype.ext ?_

Premises used: List.Vector, Subtype.ext
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
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 α)
⊢ 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))

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
simp : (l.insertIdx (↑i : ℕ) a).insertIdx ((↑j : ℕ) + 1) b = (l.insertIdx (↑j : ℕ) b).insertIdx (↑i : ℕ) a
⊢ (↑(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:
simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.val_castAdd]

Premises used: Fin.val_succ, Fin.val_castAdd, Fin.castSucc, List.Vector.insertIdx_val
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
x : (↑i : ℕ) ≤ (↑j : ℕ)
x₁ : (↑j : ℕ) ≤ l.length
⊢ (l.insertIdx (↑i : ℕ) a).insertIdx ((↑j : ℕ) + 1) b = (l.insertIdx (↑j : ℕ) b).insertIdx (↑i : ℕ) a

Tactic:
apply List.insertIdx_comm

Premises used: List.insertIdx_comm
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ (↑i : ℕ) ≤ (↑j : ℕ)

Tactic:
assumption
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
x : (↑j : ℕ) ≤ n
⊢ (↑j : ℕ) ≤ l.length

Tactic:
rw [hl]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ (↑j : ℕ) ≤ n

Tactic:
Nat.le_of_succ_le_succ j.2

Premises used: Fin.isLt, Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ (↑j : ℕ) ≤ n

Tactic:
exact Nat.le_of_succ_le_succ j.2

Premises used: Fin.isLt, Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.Vector.Basic
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
v : Vector α n
i : Fin n
a : α
⊢ ((↑v : List α).set (↑i : ℕ) a).length = n

Tactic:
simp
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList = v.toList.set (↑i : ℕ) a

Tactic:
rfl

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

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
i : Fin n
a : α
val : List α
property : val.length = n
mk :
  ∀ (val_1 : ℕ) (isLt : val_1 < n),
    (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_1, isLt⟩ : Fin n) a).get
        (⟨val_1, isLt⟩ : Fin n) =
      a
⊢ (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) i a).get i = a

Tactic:
cases i
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
val_1 : ℕ
isLt : val_1 < n
⊢ (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_1, isLt⟩ : Fin n) a).get
      (⟨val_1, isLt⟩ : Fin n) =
    a

Tactic:
simp [Vector.set, get_eq_get_toList]

Premises used: List.Vector.get_eq_get_toList, List.Vector.set
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
mk :
  ∀ (val : List α) (property : val.length = n),
    (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) i a).get j =
      get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) j
⊢ (v.set i a).get j = v.get j

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
i j : Fin n
h : i ≠ j
a : α
val : List α
property : val.length = n
mk :
  ∀ (val_1 : ℕ) (isLt : val_1 < n) (h : (⟨val_1, isLt⟩ : Fin n) ≠ j),
    (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_1, isLt⟩ : Fin n) a).get j =
      get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) j
⊢ (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) i a).get j =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) j

Tactic:
cases i
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
j : Fin n
a : α
val : List α
property : val.length = n
val_1 : ℕ
isLt : val_1 < n
h : (⟨val_1, isLt⟩ : Fin n) ≠ j
mk :
  ∀ (val_2 : ℕ) (isLt_1 : val_2 < n) (h : (⟨val_1, isLt⟩ : Fin n) ≠ ⟨val_2, isLt_1⟩),
    (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_1, isLt⟩ : Fin n) a).get
        (⟨val_2, isLt_1⟩ : Fin n) =
      get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_2, isLt_1⟩ : Fin n)
⊢ (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_1, isLt⟩ : Fin n) a).get j =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) j

Tactic:
cases j
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
val_1 : ℕ
isLt : val_1 < n
val_2 : ℕ
isLt_1 : val_2 < n
h : (⟨val_1, isLt⟩ : Fin n) ≠ ⟨val_2, isLt_1⟩
mk :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (val.set val_1 a) val_2 ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) val val_2 ⋯
⊢ (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_1, isLt⟩ : Fin n) a).get
      (⟨val_2, isLt_1⟩ : Fin n) =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) (⟨val_2, isLt_1⟩ : Fin n)

Tactic:
simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]

Premises used: List.Vector.toList_mk, List.get_eq_getElem, List.Vector.get_eq_get_toList, List.Vector.toList_set, Fin.cast_mk
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
val_1 : ℕ
isLt : val_1 < n
val_2 : ℕ
isLt_1 : val_2 < n
h : (⟨val_1, isLt⟩ : Fin n) ≠ ⟨val_2, isLt_1⟩
mk : val_1 ≠ val_2
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (val.set val_1 a) val_2 ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) val val_2 ⋯

Tactic:
rw [List.getElem_set_of_ne]

Premises used: List.getElem_set_of_ne
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
val_1 : ℕ
isLt : val_1 < n
val_2 : ℕ
isLt_1 : val_2 < n
h : (⟨val_1, isLt⟩ : Fin n) ≠ ⟨val_2, isLt_1⟩
⊢ val_1 ≠ val_2

Tactic:
simpa using h
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
pos : i = j → (v.set i a).get j = a
neg : ¬i = j → (v.set i a).get j = v.get j
⊢ (v.set i a).get j = if i = j then a else v.get j

Tactic:
split_ifs
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h : i = j
⊢ (v.set i a).get j = a

Tactic:
simp [*]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h : i = j
⊢ (v.set i a).get j = a

Tactic:
try simp [*]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h : ¬i = j
neg : v.get j = v.get j
neg₁ : i ≠ j
neg₂ : v.get j = v.get j
neg₃ neg₄ neg₅ : i ≠ j
⊢ (v.set i a).get j = v.get j

Tactic:
rwa [get_set_of_ne]

Premises used: List.Vector.get_set_of_ne
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
inst : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod =
    (toList (n := min (↑i : ℕ) n) (take (↑i : ℕ) v)).prod * a *
      (toList (n := n - ((↑i : ℕ) + 1)) (drop ((↑i : ℕ) + 1) v)).prod

Tactic:
(List.prod_set v.toList i a).trans ?_

Premises used: List.prod_set, Fin.val, List.Vector.toList, Eq.trans
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
inst : Monoid α
v : Vector α n
i : Fin n
a : α
refine :
  ((List.take (↑i : ℕ) v.toList).prod * if (↑i : ℕ) < v.toList.length then a else 1) *
      (List.drop ((↑i : ℕ) + 1) v.toList).prod =
    (toList (n := min (↑i : ℕ) n) (take (↑i : ℕ) v)).prod * a *
      (toList (n := n - ((↑i : ℕ) + 1)) (drop ((↑i : ℕ) + 1) v)).prod
⊢ (v.set i a).toList.prod =
    (toList (n := min (↑i : ℕ) n) (take (↑i : ℕ) v)).prod * a *
      (toList (n := n - ((↑i : ℕ) + 1)) (drop ((↑i : ℕ) + 1) v)).prod

Tactic:
refine (List.prod_set v.toList i a).trans ?_

Premises used: List.prod_set, Fin.val, List.Vector.toList, Eq.trans
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
inst : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ ((List.take (↑i : ℕ) v.toList).prod * if (↑i : ℕ) < v.toList.length then a else 1) *
      (List.drop ((↑i : ℕ) + 1) v.toList).prod =
    (toList (n := min (↑i : ℕ) n) (take (↑i : ℕ) v)).prod * a *
      (toList (n := n - ((↑i : ℕ) + 1)) (drop ((↑i : ℕ) + 1) v)).prod

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
inst : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Tactic:
(List.prod_set' v.toList i a).trans ?_

Premises used: Fin.val, List.prod_set', List.Vector.toList, Eq.trans
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
inst : CommGroup α
v : Vector α n
i : Fin n
a : α
refine :
  (v.toList.prod *
      if hn : (↑i : ℕ) < v.toList.length then
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v.toList (↑i : ℕ) hn)⁻¹ * a
      else 1) =
    v.toList.prod * (v.get i)⁻¹ * a
⊢ (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Tactic:
refine (List.prod_set' v.toList i a).trans ?_

Premises used: Fin.val, List.prod_set', List.Vector.toList, Eq.trans
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
inst : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (v.toList.prod *
      if hn : (↑i : ℕ) < v.toList.length then
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v.toList (↑i : ℕ) hn)⁻¹ * a
      else 1) =
    v.toList.prod * (v.get i)⁻¹ * a

Tactic:
simp [get_eq_get_toList, mul_assoc]

Premises used: mul_assoc, List.Vector.get_eq_get_toList
-- Module: Mathlib.Data.Vector.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : v.length = n
rw rw₁ : F (Vector β n) = F (Vector β n)
⊢ F (Vector β v.length) = F (Vector β n)

Tactic:
rw [Hv]
-- Module: Mathlib.Data.Vector.Basic
Goal:
F : Type u → Type u
inst : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Eq (α := F (Vector β xs.length.succ))
    (Vector.traverse f (x ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = xs.length) xs ⋯))
    (cons <$> f x <*> Vector.traverse f (Subtype.mk (p := fun (l : List α) ↦ l.length = xs.length) xs ⋯))

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u
x : List α
dsimp :
  Eq (α := Id (Vector α x.length)) (traverseAux pure x)
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))
⊢ Eq (α := Id (Vector α x.length)) (Vector.traverse pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))

Tactic:
dsimp [Vector.traverse, cast]

Premises used: List.Vector.traverse, cast
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Id (Vector α (List.length.{u} (α := α) []))) (traverseAux pure [])
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = List.length.{u} (α := α) []) [] ⋯))

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u
x : α
xs : List α
IH :
  Eq (α := Id (Vector α xs.length)) (traverseAux pure xs)
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = xs.length) xs ⋯))
⊢ Eq (α := Id (Vector α (x :: xs).length)) (traverseAux pure (x :: xs))
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = (x :: xs).length) (x :: xs) ⋯))

Tactic:
simp! [IH]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u
x : List α
nil :
  Eq.{u + 1} (α := Id (Vector α (List.length.{u} (α := α) []))) (traverseAux pure [])
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = List.length.{u} (α := α) []) [] ⋯))
cons :
  ∀ (x : α) (xs : List α)
    (IH :
      Eq (α := Id (Vector α xs.length)) (traverseAux pure xs)
        (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = xs.length) xs ⋯))),
    Eq (α := Id (Vector α (x :: xs).length)) (traverseAux pure (x :: xs))
      (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = (x :: xs).length) (x :: xs) ⋯))
⊢ Eq (α := Id (Vector α x.length)) (traverseAux pure x)
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))

Tactic:
induction x with | nil => rfl | cons x xs IH => simp! [IH]

Premises used: List.Vector.nil, List.Vector.cons
-- 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 β
nil : Eq.{u + 1} (α := Comp G F (Vector γ 0)) (pure Vector.nil) (Comp.mk (pure (pure Vector.nil)))
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) Vector.nil =
    Comp.mk (Vector.traverse f <$> Vector.traverse g Vector.nil)

Tactic:
simp! [cast, *, functor_norm]

Premises used: cast
-- 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 β
⊢ Eq.{u + 1} (α := Comp G F (Vector γ 0)) (pure nil) (Comp.mk (pure (pure nil)))

Tactic:
rfl