awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
inst : Nonempty α
⊢ Nonempty.{u + 1} (PLift α)

Tactic:
Equiv.plift.nonempty

Premises used: Equiv.plift, Equiv.nonempty
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
inst : IsEmpty α
⊢ IsEmpty.{u + 1} (PLift α)

Tactic:
Equiv.plift.isEmpty

Premises used: Equiv.isEmpty, Equiv.plift
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
⊢ Injective.{u, u + 1} (α := α) up

Tactic:
Equiv.plift.symm.injective

Premises used: Equiv.plift, Equiv.injective, Equiv.symm
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
⊢ Surjective.{u, u + 1} (α := α) up

Tactic:
Equiv.plift.symm.surjective

Premises used: Equiv.plift, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
⊢ Bijective.{u, u + 1} (α := α) up

Tactic:
Equiv.plift.symm.bijective

Premises used: Equiv.bijective, Equiv.plift, Equiv.symm
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
x y : α
⊢ { down := x : PLift α } = { down := y } ↔ x = y

Tactic:
simp
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
⊢ Surjective.{u + 1, u} (α := PLift α) down

Tactic:
Equiv.plift.surjective

Premises used: Equiv.plift, Equiv.surjective
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
⊢ Bijective.{u + 1, u} (α := PLift α) down

Tactic:
Equiv.plift.bijective

Premises used: Equiv.bijective, Equiv.plift
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
p : PLift α → Prop
⊢ (∀ (x : PLift α), p x) ↔ ∀ (x : α), p { down := x }

Tactic:
up_surjective.forall

Premises used: PLift.up_surjective, Function.Surjective.forall
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
p : PLift α → Prop
⊢ (∃ (x : PLift α), p x) ↔ ∃ (x : α), p { down := x }

Tactic:
up_surjective.exists

Premises used: PLift.up_surjective, Function.Surjective.exists
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
⊢ Injective (PLift.map f) ↔ Injective f

Tactic:
(Injective.of_comp_iff' _ down_bijective).trans <| up_injective.of_comp_iff _

Premises used: PLift.down_bijective, Function.Injective.of_comp_iff', PLift.map, Iff.trans, PLift.up_injective, Function.Injective.of_comp_iff
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
⊢ Surjective (PLift.map f) ↔ Surjective f

Tactic:
(down_surjective.of_comp_iff _).trans <| Surjective.of_comp_iff' up_bijective _

Premises used: Function.Surjective.of_comp_iff', PLift.map, Function.Surjective.of_comp_iff, PLift.down_surjective, Iff.trans, PLift.up_bijective
-- Module: Mathlib.Data.ULift
Goal:
α : Sort u
β : Sort v
f : α → β
⊢ Bijective (PLift.map f) ↔ Bijective f

Tactic:
(down_bijective.of_comp_iff _).trans <| Bijective.of_comp_iff' up_bijective _

Premises used: PLift.down_bijective, PLift.map, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', Iff.trans, PLift.up_bijective
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
β : Type v
f : α → β
inst : Nonempty α
⊢ Nonempty (ULift.{u_1, u} α)

Tactic:
Equiv.ulift.nonempty

Premises used: Equiv.ulift, Equiv.nonempty
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
β : Type v
f : α → β
inst : IsEmpty α
⊢ IsEmpty (ULift.{u_1, u} α)

Tactic:
Equiv.ulift.isEmpty

Premises used: Equiv.ulift, Equiv.isEmpty
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
⊢ Injective (α := α) up

Tactic:
Equiv.ulift.symm.injective

Premises used: Equiv.ulift, Equiv.injective, Equiv.symm
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
⊢ Surjective (α := α) up

Tactic:
Equiv.ulift.symm.surjective

Premises used: Equiv.ulift, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
⊢ Bijective (α := α) up

Tactic:
Equiv.ulift.symm.bijective

Premises used: Equiv.bijective, Equiv.ulift, Equiv.symm
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
x y : α
⊢ { down := x : ULift.{u_1, u} α } = { down := y } ↔ x = y

Tactic:
simp
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
⊢ Surjective (α := ULift.{u_1, u} α) down

Tactic:
Equiv.ulift.surjective

Premises used: Equiv.ulift, Equiv.surjective
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
⊢ Bijective (α := ULift.{u_1, u} α) down

Tactic:
Equiv.ulift.bijective

Premises used: Equiv.bijective, Equiv.ulift
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
p : ULift.{u_1, u} α → Prop
⊢ (∀ (x : ULift.{u_1, u} α), p x) ↔ ∀ (x : α), p { down := x }

Tactic:
up_surjective.forall

Premises used: Function.Surjective.forall, ULift.up_surjective
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
p : ULift.{u_1, u} α → Prop
⊢ (∃ (x : ULift.{u_1, u} α), p x) ↔ ∃ (x : α), p { down := x }

Tactic:
up_surjective.exists

Premises used: Function.Surjective.exists, ULift.up_surjective
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
β : Type v
f : α → β
⊢ Injective (ULift.map f) ↔ Injective f

Tactic:
(Injective.of_comp_iff' _ down_bijective).trans <| up_injective.of_comp_iff _

Premises used: Function.Injective.of_comp_iff', ULift.down_bijective, ULift.up_injective, Iff.trans, ULift.map, Function.Injective.of_comp_iff
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
β : Type v
f : α → β
⊢ Surjective (ULift.map f) ↔ Surjective f

Tactic:
(down_surjective.of_comp_iff _).trans <| Surjective.of_comp_iff' up_bijective _

Premises used: ULift.up_bijective, ULift.down_surjective, Function.Surjective.of_comp_iff', Function.Surjective.of_comp_iff, Iff.trans, ULift.map
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
β : Type v
f : α → β
⊢ Bijective (ULift.map f) ↔ Bijective f

Tactic:
(down_bijective.of_comp_iff _).trans <| Bijective.of_comp_iff' up_bijective _

Premises used: ULift.up_bijective, ULift.down_bijective, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', Iff.trans, ULift.map
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
x y : ULift.{u_1, u} α
h : x.down = y.down
⊢ x = y

Tactic:
congrArg up h

Premises used: congrArg, ULift.up
-- Module: Mathlib.Data.ULift
Goal:
α : Type u
β : ULift.{u_2, u} α → Type u_1
inst : DecidableEq α
f : (a : α) → β { down := a }
a : α
x : β { down := a }
⊢ (fun (t : ULift.{u_2, u} α) ↦
      rec (motive := fun (x : ULift.{u_2, u} α) ↦ β x) (update (β := fun (down : α) ↦ β { down := down }) f a x) t) =
    update (β := β) (fun (t : ULift.{u_2, u} α) ↦ rec (motive := fun (x : ULift.{u_2, u} α) ↦ β x) f t)
      { down := a : ULift.{u_2, u} α } x

Tactic:
Function.rec_update up_injective (ULift.rec ·) (fun _ _ => rfl) (fun
    | _, _, .up _, h => (h _ rfl).elim) _ _ _

Premises used: ULift.rec, ULift.up_injective, Function.rec_update
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Vector α n) toList

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective, List.Vector, List.Vector.toList
-- Module: Mathlib.Data.Vector.Basic
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
rw₁ rw₂ : n = n
⊢ (↑(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

Tactic:
rw [hv, hw]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
⊢ Subsingleton.{u_1 + 1} (Vector α 0)

Tactic:
⟨fun _ _ => Vector.ext fun m => Fin.elim0 m⟩

Premises used: List.Vector.ext, Subsingleton.intro, Fin.elim0
-- Module: Mathlib.Data.Vector.Basic
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'
rw₁ rw₂ : a ::ᵥ v' = a ::ᵥ v'
⊢ v.head ::ᵥ v.tail = a ::ᵥ v'

Tactic:
rw [h.1, h.2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.Vector.Basic
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'
rw₂ rw₃ : ¬v.head = a ∨ ¬v.tail = v' ↔ v.head ≠ a ∨ v.tail ≠ v'
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

Tactic:
rw [Ne, eq_cons_iff a v v', not_and_or]

Premises used: List.Vector.eq_cons_iff, Ne, not_and_or
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n.succ
⊢ ∃ (a : α), ∃ (as : Vector α n), v = a ::ᵥ as

Tactic:
⟨v.head, v.tail, (eq_cons_iff v.head v v.tail).2 ⟨rfl, rfl⟩⟩

Premises used: Iff.mpr, List.Vector.eq_cons_iff, List.Vector.head, And.intro, Exists.intro, List.Vector.tail, rfl
-- Module: Mathlib.Data.Vector.Basic
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 α) []
rw₃ rw₄ : Eq.{u_1 + 1} (α := List α) (↑(Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) : List α) []
⊢ (ofFn f).toList = List.ofFn f

Tactic:
rw [ofFn, List.ofFn_zero, toList, nil]

Premises used: List.Vector.ofFn, List.ofFn_zero, List.Vector.nil, List.Vector.toList
-- Module: Mathlib.Data.Vector.Basic
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
rw₃ 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
⊢ (ofFn f).toList = List.ofFn f

Tactic:
rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

Premises used: List.Vector.ofFn, List.Vector.toList_cons, List.ofFn_succ
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
⊢ (↑v : List α).length = n

Tactic:
v.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Vector.Basic
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 ∧ ∀ (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

Premises used: Nat.succ_eq_add_one, forall_eq_or_imp, List.Vector.toList_cons, List.mem_cons
-- Module: Mathlib.Data.Vector.Basic
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 : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ p a

Tactic:
hp.1

Premises used: And.left
-- Module: Mathlib.Data.Vector.Basic
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 : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ p a

Tactic:
exact hp.1

Premises used: And.left
-- Module: Mathlib.Data.Vector.Basic
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 : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ ∀ (x : α), x ∈ v.toList → p x

Tactic:
hp.2

Premises used: And.right
-- Module: Mathlib.Data.Vector.Basic
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 : p a ∧ ∀ (a : α), a ∈ v.toList → p a
⊢ ∀ (x : α), x ∈ v.toList → p x

Tactic:
exact hp.2

Premises used: And.right
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x
⊢ pmap (p := p) f (a ::ᵥ v) hp = f a ⋯ ::ᵥ pmap (p := p) f v ⋯

Tactic:
rfl

Premises used: List.Vector.pmap, List.pmap, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Basic
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
ha : p a
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ ∀ (x : α), x ∈ (a ::ᵥ v).toList → p x

Tactic:
simpa [ha]
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
ha : p a
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ f a ha ::ᵥ pmap (p := p) f v hp = pmap (p := p) f (a ::ᵥ v) ⋯

Tactic:
rfl

Premises used: List.Vector.pmap, List.pmap, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
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))
⊢ (map f v).toList = List.map f v.toList

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
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:
rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (map f v).head = f v.head
⊢ (map f v).head = f v.head

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Premises used: List.Vector.exists_eq_cons
-- Module: Mathlib.Data.Vector.Basic
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
rw₃ rw₄ : f a = f a
⊢ (map f v).head = f v.head

Tactic:
rw [h, map_cons, head_cons, head_cons]

Premises used: List.Vector.map_cons, List.Vector.head_cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (map f v).tail = map f v.tail
⊢ (map f v).tail = map f v.tail

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Premises used: List.Vector.exists_eq_cons
-- Module: Mathlib.Data.Vector.Basic
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
rw₃ rw₄ : map f v' = map f v'
⊢ (map f v).tail = map f v.tail

Tactic:
rw [h, map_cons, tail_cons, tail_cons]

Premises used: List.Vector.tail_cons, List.Vector.map_cons
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : ℕ
hi : i < n
⊢ getElem (valid := fun (x : Vector β n) (i : ℕ) ↦ i < n) (map f v) i hi =
    f (getElem (valid := fun (x : Vector α n) (i : ℕ) ↦ i < n) v i hi)

Tactic:
simp only [getElem_def, toList_map, List.getElem_map]

Premises used: List.Vector.getElem_def, List.Vector.toList_map, List.getElem_map
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
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
⊢ (pmap (p := p) f v hp).toList = List.pmap (P := p) f v.toList hp

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
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:
rfl
-- Module: Mathlib.Data.Vector.Basic
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
rw : v.head = v.head ∨ v.head ∈ v.tail.toList
⊢ v.head ∈ v.toList

Tactic:
rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]

Premises used: List.Vector.toList_cons, List.Vector.cons_head_tail, List.Vector.head_cons, List.mem_cons
-- Module: Mathlib.Data.Vector.Basic
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.head ∨ v.head ∈ v.tail.toList

Tactic:
.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Vector.Basic
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.head ∨ v.head ∈ v.tail.toList

Tactic:
exact .inl rfl
-- Module: Mathlib.Data.Vector.Basic
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
obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (pmap (p := p) f v hp).head = f v.head ⋯
⊢ (pmap (p := p) f v hp).head = f v.head ⋯

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Premises used: List.Vector.exists_eq_cons
-- Module: Mathlib.Data.Vector.Basic
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 ⋯
simp_rw₁ : (f a ⋯ ::ᵥ pmap (p := p) f v' ⋯).head = f (a ::ᵥ v').head ⋯
⊢ (pmap (p := p) f v hp).head = f v.head ⋯

Tactic:
simp_rw [h, pmap_cons, head_cons]

Premises used: List.Vector.pmap_cons, List.Vector.head_cons
-- Module: Mathlib.Data.Vector.Basic
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
rw : x = v.head ∨ x ∈ v.tail.toList
⊢ x ∈ v.toList

Tactic:
rw [← cons_head_tail v, toList_cons, List.mem_cons]

Premises used: List.Vector.toList_cons, List.Vector.cons_head_tail, List.mem_cons
-- Module: Mathlib.Data.Vector.Basic
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.head ∨ x ∈ v.tail.toList

Tactic:
.inr hx

Premises used: Or.inr
-- Module: Mathlib.Data.Vector.Basic
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.head ∨ x ∈ v.tail.toList

Tactic:
exact .inr hx
-- Module: Mathlib.Data.Vector.Basic
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
obtain : ∀ (a : α) (v' : Vector α n) (h : v = a ::ᵥ v'), (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail ⋯
⊢ (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail ⋯

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Premises used: List.Vector.exists_eq_cons
-- Module: Mathlib.Data.Vector.Basic
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 ⋯
simp_rw₁ : (f a ⋯ ::ᵥ pmap (p := p) f v' ⋯).tail = pmap (p := p) f (a ::ᵥ v').tail ⋯
⊢ (pmap (p := p) f v hp).tail = pmap (p := p) f v.tail ⋯

Tactic:
simp_rw [h, pmap_cons, tail_cons]

Premises used: List.Vector.tail_cons, List.Vector.pmap_cons
-- Module: Mathlib.Data.Vector.Basic
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
hp : ∀ (x : α), x ∈ v.toList → p x
i : ℕ
hi : i < n
⊢ getElem (valid := fun (x : Vector α n) (i : ℕ) ↦ i < n) v i hi ∈ v.toList

Tactic:
simp [getElem_def, List.getElem_mem]

Premises used: List.Vector.getElem_def, List.getElem_mem
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
i : ℕ
hi : i < n
⊢ getElem (valid := fun (x : Vector β n) (i : ℕ) ↦ i < n) (pmap (p := p) f v hp) i hi =
    f (getElem (valid := fun (x : Vector α n) (i : ℕ) ↦ i < n) v i hi) ⋯

Tactic:
simp only [getElem_def, toList_pmap, List.getElem_pmap]

Premises used: List.Vector.getElem_def, List.getElem_pmap, List.Vector.toList_pmap
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i : Fin n
⊢ v.get i = v.toList.get (Fin.cast ⋯ i)

Tactic:
rfl

Premises used: List.Vector.get, List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
i : Fin n
⊢ (replicate n a).get i = a

Tactic:
apply List.getElem_replicate

Premises used: List.getElem_replicate
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : Fin n
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)
⊢ (map f v).get i = f (v.get i)

Tactic:
cases v
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
i : Fin n
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:
simp [Vector.map, get_eq_get_toList]

Premises used: List.Vector.map, List.Vector.get_eq_get_toList
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f nil nil = nil

Tactic:
rfl

Premises used: List.zipWith, List.Vector.nil, List.Vector.map₂, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
hd₁ : α
tl₁ : Vector α n
hd₂ : β
tl₂ : Vector β n
f : α → β → γ
⊢ map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ map₂ f tl₁ tl₂

Tactic:
rfl

Premises used: List.zipWith, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).get i = f i

Tactic:
simp [get_eq_get_toList]

Premises used: List.Vector.get_eq_get_toList
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
x : ∀ (m : Fin n), (ofFn v.get).get m = v.get m
⊢ ofFn v.get = v

Tactic:
ext
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
v : Vector α n
m : Fin n
⊢ (ofFn v.get).get m = v.get m

Tactic:
apply List.Vector.get_ofFn

Premises used: List.Vector.get_ofFn
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ (↑i : ℕ) + 1 < n

Tactic:
lia
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : Fin (n - 1)
obtain : ∀ (i : ℕ) (ih : i < n - 1), x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨(↑(⟨i, ih⟩ : Fin (n - 1)) : ℕ) + 1, ⋯⟩
⊢ x.tail.get i = x.get ⟨(↑i : ℕ) + 1, ⋯⟩

Tactic:
obtain ⟨i, ih⟩ := i
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
dsimp : x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨i + 1, ⋯⟩
⊢ x.tail.get (⟨i, ih⟩ : Fin (n - 1)) = x.get ⟨(↑(⟨i, ih⟩ : Fin (n - 1)) : ℕ) + 1, ⋯⟩

Tactic:
dsimp