awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) i
a :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (r : α ⊗ α ⟹ «repeat» (n + 1) Prop)
    (x : { x : α Fin2.fz × α Fin2.fz // ofRepeat (r Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz x.1 x.2)) }),
    comp (α := fun (i : Fin2 (n + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
        Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) Fin2.fz x =
      prod.mk (α := α) (β := α) Fin2.fz (↑x : α Fin2.fz × α Fin2.fz).1 (↑x : α Fin2.fz × α Fin2.fz).2
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
      Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) i x =
    prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2
have a₁ : ∀ {n : ℕ} (a : Fin2 n),
  (∀ {α : TypeVec.{u_1} n} (r : α ⊗ α ⟹ «repeat» n Prop)
      (x : (fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) a),
      comp (α := fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
          Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a x =
        prod.mk (α := α) (β := α) a (↑x : α a × α a).1 (↑x : α a × α a).2) →
    ∀ {α : TypeVec.{u_1} (n + 1)} (r : α ⊗ α ⟹ «repeat» (n + 1) Prop)
      (x : { x : α a.fs × α a.fs // ofRepeat (r a.fs (prod.mk (α := α) (β := α) a.fs x.1 x.2)) }),
      comp (α := fun (i : Fin2 (n + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) })
          (β := Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a.fs x =
        prod.mk (α := α) (β := α) a.fs (↑x : α a.fs × α a.fs).1 (↑x : α a.fs × α a.fs).2
Tactic: induction i
Cleared hypotheses: α, r, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (r : α ⊗ α ⟹ «repeat» n_1 Prop)
    (x : (fun (i : Fin2 n_1) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) a),
    comp (α := fun (i : Fin2 n_1) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
        Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a x =
      prod.mk (α := α) (β := α) a (↑x : α a × α a).1 (↑x : α a × α a).2
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α a.fs × α a.fs // ofRepeat (r a.fs (prod.mk (α := α) (β := α) a.fs x.1 x.2)) }
⊢ comp (α := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
      Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a.fs x =
    prod.mk (α := α) (β := α) a.fs (↑x : α a.fs × α a.fs).1 (↑x : α a.fs × α a.fs).2
have a : subtypeVal (α := (α ⊗ α).drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a
    (toSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a x) =
  prod.mk (α := fun (i : Fin2 n_1) ↦ α i.fs) (β := fun (i : Fin2 n_1) ↦ α i.fs) a (↑x : α a.fs × α a.fs).1
    (↑x : α a.fs × α a.fs).2
Tactic: simp only [toSubtype', comp, subtypeVal, prod.mk] at *
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h :
  ∀ (m : Fin n),
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) v hv) m =
      get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) w hw) m
⊢ (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) v hv) : List α).length =
    (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) w hw) : List α).length
have rw : n = (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) w hw) : List α).length
Tactic: rw [hv, hw]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h :
  ∀ (m : Fin n),
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) v hv) m =
      get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) w hw) m
rw : n = (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) w hw) : List α).length
⊢ (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) v hv) : List α).length =
    (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = n) w hw) : List α).length
have rw₁ : n = n
Tactic: rw [hv, hw]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ v.head ::ᵥ v.tail = a ::ᵥ v'
have rw : a ::ᵥ v.tail = a ::ᵥ v'
Tactic: rw [h.1, h.2]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
rw : a ::ᵥ v.tail = a ::ᵥ v'
⊢ v.head ::ᵥ v.tail = a ::ᵥ v'
have rw₁ : a ::ᵥ v' = a ::ᵥ v'
Tactic: rw [h.1, h.2]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
have rw : ¬v = a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
Tactic: rw [Ne, eq_cons_iff a v v', not_and_or]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
rw : ¬v = a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
have rw₁ : ¬(v.head = a ∧ v.tail = v') ↔ v.head ≠ a ∨ v.tail ≠ v'
Tactic: rw [Ne, eq_cons_iff a v v', not_and_or]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
rw : ¬v = a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
rw₁ : ¬(v.head = a ∧ v.tail = v') ↔ v.head ≠ a ∨ v.tail ≠ v'
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
have rw₂ : ¬v.head = a ∨ ¬v.tail = v' ↔ v.head ≠ a ∨ v.tail ≠ v'
Tactic: rw [Ne, eq_cons_iff a v v', not_and_or]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
f : Fin 0 → α
⊢ (ofFn f).toList = List.ofFn f
have rw : toList nil = List.ofFn f
Tactic: rw [ofFn, List.ofFn_zero, toList, nil]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
f : Fin 0 → α
rw : toList nil = List.ofFn f
⊢ (ofFn f).toList = List.ofFn f
have rw₁ : Eq.{u_1 + 1} (α := List α) (toList nil) []
Tactic: rw [ofFn, List.ofFn_zero, toList, nil]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
f : Fin 0 → α
rw : toList nil = List.ofFn f
rw₁ : Eq.{u_1 + 1} (α := List α) (toList nil) []
⊢ (ofFn f).toList = List.ofFn f
have rw₂ : Eq.{u_1 + 1} (α := List α) (↑nil : List α) []
Tactic: rw [ofFn, List.ofFn_zero, toList, nil]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
f : Fin 0 → α
rw : toList nil = List.ofFn f
rw₁ : Eq.{u_1 + 1} (α := List α) (toList nil) []
rw₂ : Eq.{u_1 + 1} (α := List α) (↑nil : List α) []
⊢ (ofFn f).toList = List.ofFn f
have rw₃ : Eq.{u_1 + 1} (α := List α) (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry) : List α) []
Tactic: rw [ofFn, List.ofFn_zero, toList, nil]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (ofFn f).toList = List.ofFn f
have rw : toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = List.ofFn f
Tactic: rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
rw : toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = List.ofFn f
⊢ (ofFn f).toList = List.ofFn f
have rw₁ : toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ
Tactic: rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
rw : toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = List.ofFn f
rw₁ :
  toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ
⊢ (ofFn f).toList = List.ofFn f
have rw₂ : f 0 :: toList (n := n) (ofFn fun (i : Fin n) ↦ f i.succ) = f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ
Tactic: rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
rw : toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = List.ofFn f
rw₁ :
  toList (n := n + 1) (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ) = f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ
rw₂ : f 0 :: toList (n := n) (ofFn fun (i : Fin n) ↦ f i.succ) = f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ
⊢ (ofFn f).toList = List.ofFn f
have rw₃ : (f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ) = f 0 :: List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ
Tactic: rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ p a
have hp₁ : p a ∧ ∀ (a : α), a ∈ v.toList → p a
Tactic: simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ ∀ (x : α), x ∈ v.toList → p x
have hp₁ : p a ∧ ∀ (a : α), a ∈ v.toList → p a
Tactic: simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
⊢ (map f v).toList = List.map f v.toList
have mk : ∀ (val : List α) (property : val.length = n),
  toList (n := n) (map f (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) =
    List.map f (toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).head = f v.head
have obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (map f v).head = f v.head
Tactic: obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).head = f v.head
have rw : (map f (a ::ᵥ v')).head = f (a ::ᵥ v').head
Tactic: rw [h, map_cons, head_cons, head_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
rw : (map f (a ::ᵥ v')).head = f (a ::ᵥ v').head
⊢ (map f v).head = f v.head
have rw₁ : (f a ::ᵥ map f v').head = f (a ::ᵥ v').head
Tactic: rw [h, map_cons, head_cons, head_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
rw : (map f (a ::ᵥ v')).head = f (a ::ᵥ v').head
rw₁ : (f a ::ᵥ map f v').head = f (a ::ᵥ v').head
⊢ (map f v).head = f v.head
have rw₂ : f a = f (a ::ᵥ v').head
Tactic: rw [h, map_cons, head_cons, head_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
rw : (map f (a ::ᵥ v')).head = f (a ::ᵥ v').head
rw₁ : (f a ::ᵥ map f v').head = f (a ::ᵥ v').head
rw₂ : f a = f (a ::ᵥ v').head
⊢ (map f v).head = f v.head
have rw₃ : f a = f a
Tactic: rw [h, map_cons, head_cons, head_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).tail = map f v.tail
have obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (map f v).tail = map f v.tail
Tactic: obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).tail = map f v.tail
have rw : (map f (a ::ᵥ v')).tail = map f (a ::ᵥ v').tail
Tactic: rw [h, map_cons, tail_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
rw : (map f (a ::ᵥ v')).tail = map f (a ::ᵥ v').tail
⊢ (map f v).tail = map f v.tail
have rw₁ : (f a ::ᵥ map f v').tail = map f (a ::ᵥ v').tail
Tactic: rw [h, map_cons, tail_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
rw : (map f (a ::ᵥ v')).tail = map f (a ::ᵥ v').tail
rw₁ : (f a ::ᵥ map f v').tail = map f (a ::ᵥ v').tail
⊢ (map f v).tail = map f v.tail
have rw₂ : map f v' = map f (a ::ᵥ v').tail
Tactic: rw [h, map_cons, tail_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
rw : (map f (a ::ᵥ v')).tail = map f (a ::ᵥ v').tail
rw₁ : (f a ::ᵥ map f v').tail = map f (a ::ᵥ v').tail
rw₂ : map f v' = map f (a ::ᵥ v').tail
⊢ (map f v).tail = map f v.tail
have rw₃ : map f v' = map f v'
Tactic: rw [h, map_cons, tail_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap (p := p) f v hp).toList = List.pmap (P := p) f v.toList hp
have mk : ∀ (val : List α) (property : val.length = n)
  (hp : ∀ (x : α), x ∈ toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) → p x),
  (pmap (p := p) f (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) hp).toList =
    List.pmap (P := p) f (toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) hp
Tactic: cases v
Cleared hypotheses: v, hp
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head ∈ v.toList
have rw : v.head = v.head ∨ v.head ∈ v.tail.toList
Tactic: rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap (p := p) f v hp).head = f v.head ⋯
have obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (pmap (p := p) f v hp).head = f v.head sorry
Tactic: obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap (p := p) f v hp).head = f v.head ⋯
have simp_rw : (pmap (p := p) f (a ::ᵥ v') sorry).head = f (a ::ᵥ v').head sorry
Tactic: simp_rw [h, pmap_cons, head_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
simp_rw : (pmap (p := p) f (a ::ᵥ v') ⋯).head = f (a ::ᵥ v').head ⋯
⊢ (pmap (p := p) f v hp).head = f v.head ⋯
have simp_rw₁ : (f a sorry ::ᵥ pmap (p := p) f v' sorry).head = f (a ::ᵥ v').head sorry
Tactic: simp_rw [h, pmap_cons, head_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.toList
have rw : x = v.head ∨ x ∈ v.tail.toList
Tactic: rw [← cons_head_tail v, toList_cons, List.mem_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail ⋯
have obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail sorry
Tactic: obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail ⋯
have simp_rw : (pmap (p := p) f (a ::ᵥ v') sorry).tail = pmap (p := p) f (a ::ᵥ v').tail sorry
Tactic: simp_rw [h, pmap_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
simp_rw : (pmap (p := p) f (a ::ᵥ v') ⋯).tail = pmap (p := p) f (a ::ᵥ v').tail ⋯
⊢ (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail ⋯
have simp_rw₁ : (f a sorry ::ᵥ pmap (p := p) f v' sorry).tail = pmap (p := p) f (a ::ᵥ v').tail sorry
Tactic: simp_rw [h, pmap_cons, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : Fin n
⊢ (map f v).get i = f (v.get i)
have mk : ∀ (val : List α) (property : val.length = n),
  get (map f (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) i =
    f (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) i)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ ofFn v.get = v
have x : ∀ (m : Fin n), (ofFn v.get).get m = v.get m
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ x.tail.get i = x.get ⟨(↑i : ℕ) + 1, ⋯⟩
have obtain : ∀ (i : ℕ) (ih : i < n - 1), x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨(↑(⟨i, ih⟩ : Fin (n - 1)) : ℕ) + 1, sorry⟩
Tactic: obtain ⟨i, ih⟩ := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨(↑(⟨i, ih⟩ : Fin (n - 1)) : ℕ) + 1, ⋯⟩
have dsimp : x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨i + 1, sorry⟩
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨i + 1, ⋯⟩
have nil : ∀ (h : List.length.{u_1} (α := α) [] = n),
  Eq.{u_1 + 1} (α := α) (get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)) (⟨i, ih⟩ : Fin (n - 1)))
    (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h) (⟨i + 1, sorry⟩ : Fin n))
Tactic: rcases x with ⟨_ | _, h⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
nil :
  ∀ (h : List.length.{u_1} (α := α) [] = n),
    Eq.{u_1 + 1} (α := α) (get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)) (⟨i, ih⟩ : Fin (n - 1)))
      (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h) (⟨i + 1, ⋯⟩ : Fin n))
⊢ x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨i + 1, ⋯⟩
have cons : ∀ (head : α) (tail : List α) (h : (head :: tail).length = n),
  get (Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)) (⟨i, ih⟩ : Fin (n - 1)) =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h) (⟨i + 1, sorry⟩ : Fin n)
Tactic: rcases x with ⟨_ | _, h⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (hypothesis)
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
h : List.length.{u_1} (α := α) [] = n
⊢ Eq.{u_1 + 1} (α := α) (get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)) (⟨i, ih⟩ : Fin (n - 1)))
    (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h) (⟨i + 1, ⋯⟩ : Fin n))
have h₁ : 0 = n
Tactic: rw [List.length] at h
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (hypothesis)
Goal:
α : Type u_1
n i : ℕ
ih : i < n - 1
h_1 : List.length.{u_1} (α := α) [] = n
h : 0 = n
⊢ Eq.{u_1 + 1} (α := α) (get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h_1)) (⟨i, ih⟩ : Fin (n - 1)))
    (get (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h_1) (⟨i + 1, ⋯⟩ : Fin n))
have ih₁ : i < HSub.hSub (α := ℕ) 0 1
Tactic: rw [← h] at ih
Cleared hypotheses: h_1, h
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ get (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (a :: l) e)) (⟨i, h⟩ : Fin n) =
    get (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (a :: l) e) (⟨i, h⟩ : Fin n).succ
have simp : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
    (toList (n := n) (tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: l) e) : Vector α (n + 1 - 1))) i
    sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry
Tactic: simp [get_eq_get_toList]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ ofFn (ofFn f).tail.get = ofFn fun (i : Fin n) ↦ f i.succ
have e_a : (ofFn f).tail.get = fun (i : Fin n) ↦ f i.succ
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).tail.get = fun (i : Fin n) ↦ f i.succ
have e_a : ∀ (i : Fin (n.succ - 1)), (ofFn f).tail.get i = f i.succ
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ (ofFn f).tail.get i = f i.succ
have e_a : f (⟨(↑i : ℕ) + 1, sorry⟩ : Fin n.succ) = f i.succ
Tactic: rw [get_tail, get_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
v : Vector α 1
⊢ v.toList = [v.head]
have rw : (v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]
Tactic: rw [← v.cons_head_tail]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ v.toList.Nodup ↔ Function.Injective v.get
have obtain : ∀ (l : List α),
  (toList (n := l.length) (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l sorry)).Nodup ↔
    Function.Injective (α := Fin l.length) (get (Subtype.mk (p := fun (l_1 : List α) ↦ l_1.length = l.length) l sorry))
Tactic: obtain ⟨l, rfl⟩ := v
Cleared hypotheses: n, v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ v.reverse.reverse = v
have mk : ∀ (val : List α) (property : val.length = n),
  Eq (α := Vector α n) (reverse (reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).head = f 0
have rw : (ofFn f).get 0 = f 0
Tactic: rw [← get_zero, get_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n.succ → α
rw : (ofFn f).get 0 = f 0
⊢ (ofFn f).head = f 0
have rw₁ : f 0 = f 0
Tactic: rw [← get_zero, get_ofFn]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
⊢ (a ::ᵥ v).get i.succ = v.get i
have rw : (a ::ᵥ v).tail.get i = v.get i
Tactic: rw [← get_tail_succ, tail_cons]