awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' ys s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (ys.snoc y) s

Tactic:
simp [h x y s, ih]
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
nil : ∀ {s : σ}, mapAccumr₂ f Vector.nil Vector.nil s = mapAccumr f' Vector.nil s
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β)
    (ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' ys s) {s : σ},
    mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (ys.snoc y) s
⊢ mapAccumr₂ f xs ys s = mapAccumr f' ys s

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s with
  | nil => rfl
  | snoc xs ys x y ih => simp [h x y s, ih]

Premises used: List.Vector.nil, List.Vector.snoc
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr f' nil s

Tactic:
rfl
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' xs s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (xs.snoc x) s

Tactic:
simp [h x y s, ih]
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
nil : ∀ {s : σ}, mapAccumr₂ f Vector.nil Vector.nil s = mapAccumr f' Vector.nil s
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β)
    (ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr f' xs s) {s : σ},
    mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr f' (xs.snoc x) s
⊢ mapAccumr₂ f xs ys s = mapAccumr f' xs s

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s with
  | nil => rfl
  | snoc xs ys x y ih => simp [h x y s, ih]

Premises used: List.Vector.nil, List.Vector.snoc
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
nil : map₂ f Vector.nil Vector.nil = map₂ f Vector.nil Vector.nil
cons :
  ∀ {n : ℕ} {a b : α} {x y : Vector α n},
    map₂ f x y = map₂ f y x → map₂ f (a ::ᵥ x) (b ::ᵥ y) = map₂ f (b ::ᵥ y) (a ::ᵥ x)
⊢ map₂ f xs ys = map₂ f ys xs

Tactic:
induction xs, ys using Vector.inductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f nil nil = map₂ f nil nil

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
n_1 : ℕ
a b : α
x y : Vector α n_1
h : map₂ f x y = map₂ f y x
⊢ map₂ f (a ::ᵥ x) (b ::ᵥ y) = map₂ f (b ::ᵥ y) (a ::ᵥ x)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs ys : Vector α n
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
nil : ∀ {s : σ}, mapAccumr₂ f Vector.nil Vector.nil s = mapAccumr₂ f Vector.nil Vector.nil s
cons :
  ∀ {n : ℕ} {a b : α} {x y : Vector α n},
    (∀ {s : σ}, mapAccumr₂ f x y s = mapAccumr₂ f y x s) →
      ∀ {s : σ}, mapAccumr₂ f (a ::ᵥ x) (b ::ᵥ y) s = mapAccumr₂ f (b ::ᵥ y) (a ::ᵥ x) s
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s

Tactic:
induction xs, ys using Vector.inductionOn₂ generalizing s
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ f nil nil s

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
n_1 : ℕ
a b : α
x y : Vector α n_1
h : ∀ {s : σ}, mapAccumr₂ f x y s = mapAccumr₂ f y x s
s : σ
⊢ mapAccumr₂ f (a ::ᵥ x) (b ::ᵥ y) s = mapAccumr₂ f (b ::ᵥ y) (a ::ᵥ x) s

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
nil : map₂ f Vector.nil Vector.nil = map₂ (flip f) Vector.nil Vector.nil
cons :
  ∀ {n : ℕ} {a : α} {b : β} {x : Vector α n} {y : Vector β n},
    map₂ f x y = map₂ (flip f) y x → map₂ f (a ::ᵥ x) (b ::ᵥ y) = map₂ (flip f) (b ::ᵥ y) (a ::ᵥ x)
⊢ map₂ f xs ys = map₂ (flip f) ys xs

Tactic:
induction xs, ys using Vector.inductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil

Tactic:
simp_all [flip]

Premises used: flip
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
h : map₂ f x y = map₂ (flip f) y x
⊢ map₂ f (a ::ᵥ x) (b ::ᵥ y) = map₂ (flip f) (b ::ᵥ y) (a ::ᵥ x)

Tactic:
simp_all [flip]

Premises used: flip
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
nil : mapAccumr₂ f Vector.nil Vector.nil s = mapAccumr₂ (flip f) Vector.nil Vector.nil s
cons :
  ∀ {n : ℕ} {a : α} {b : β} {x : Vector α n} {y : Vector β n},
    mapAccumr₂ f x y s = mapAccumr₂ (flip f) y x s →
      mapAccumr₂ f (a ::ᵥ x) (b ::ᵥ y) s = mapAccumr₂ (flip f) (b ::ᵥ y) (a ::ᵥ x) s
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s

Tactic:
induction xs, ys using Vector.inductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s

Tactic:
simp_all [flip]

Premises used: flip
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
h : mapAccumr₂ f x y s = mapAccumr₂ (flip f) y x s
⊢ mapAccumr₂ f (a ::ᵥ x) (b ::ᵥ y) s = mapAccumr₂ (flip f) (b ::ᵥ y) (a ::ᵥ x) s

Tactic:
simp_all [flip]

Premises used: flip
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
i : Fin n
v : Vector α n
⊢ v.get i ∈ v.toList

Tactic:
List.get_mem _ _

Premises used: List.Vector.get, List.get_mem, List.Vector.toList
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
simp :
  (∃ (i : ℕ), ∃ (h : i < v.toList.length), v.toList.get (⟨i, h⟩ : Fin v.toList.length) = a) ↔
    ∃ (i : ℕ), ∃ (h : i < n), v.toList.get (Fin.cast ⋯ (⟨i, h⟩ : Fin n)) = a
⊢ a ∈ v.toList ↔ ∃ (i : Fin n), v.get i = a

Tactic:
simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get_toList]

Premises used: List.mem_iff_get, List.Vector.get_eq_get_toList, Fin.exists_iff
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
h_1 : ∃ (i : ℕ), ∃ (h : i < v.toList.length), v.toList.get (⟨i, h⟩ : Fin v.toList.length) = a
i : ℕ
hi : i < v.toList.length
h : v.toList.get (⟨i, hi⟩ : Fin v.toList.length) = a
rwa rwa₁ rwa₂ rwa₃ : ∀ (hi_1 : i < n) (h : v.toList.get (⟨i, hi⟩ : Fin v.toList.length) = a), i < n
⊢ i < n

Tactic:
rwa [toList_length] at hi

Premises used: List.Vector.toList_length
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
h_1 : ∃ (i : ℕ), ∃ (h : i < n), v.toList.get (Fin.cast ⋯ (⟨i, h⟩ : Fin n)) = a
i : ℕ
hi : i < n
h : v.toList.get (Fin.cast ⋯ (⟨i, hi⟩ : Fin n)) = a
rwa rwa₁ rwa₂ rwa₃ : i < n
⊢ i < v.toList.length

Tactic:
rwa [toList_length]

Premises used: List.Vector.toList_length
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (∃ (i : ℕ), ∃ (h : i < v.toList.length), v.toList.get (⟨i, h⟩ : Fin v.toList.length) = a) ↔
    ∃ (i : ℕ), ∃ (h : i < n), v.toList.get (Fin.cast ⋯ (⟨i, h⟩ : Fin n)) = a

Tactic:
exact
    ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi, h⟩, fun ⟨i, hi, h⟩ =>
      ⟨i, by rwa [toList_length], h⟩⟩
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
a : α
⊢ ¬Membership.mem (γ := List α) (toList nil) a

Tactic:
simp
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
a : α
v : Vector α 0
⊢ ¬a ∈ v.toList

Tactic:
(Vector.eq_nil v).symm ▸ notMem_nil a

Premises used: List.Vector.eq_nil, Eq.rec, List.Vector.notMem_nil, Eq.symm
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a a' : α
v : Vector α n
rw : a' ∈ a :: v.toList ↔ a' = a ∨ a' ∈ v.toList
rw₁ rw₂ : a' = a ∨ a' ∈ v.toList ↔ a' = a ∨ a' ∈ v.toList
⊢ a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList

Tactic:
rw [Vector.toList_cons, List.mem_cons]

Premises used: List.Vector.toList_cons, List.mem_cons
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
obtain : ∀ (a' : α) (v' : Vector α n) (h : v = a' ::ᵥ v'), a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

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

Premises used: List.Vector.exists_eq_cons
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
simp_rw : a ∈ (a' ::ᵥ v').toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList
simp_rw₁ : a = a' ∨ a ∈ v'.toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList
simp_rw₂ : a = a' ∨ a ∈ v'.toList ↔ a = a' ∨ a ∈ (a' ::ᵥ v').tail.toList
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

Tactic:
simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]

Premises used: List.Vector.tail_cons, List.Vector.mem_cons_iff, List.Vector.head_cons
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ a ∈ (a ::ᵥ v).toList

Tactic:
(Vector.mem_iff_get a (a ::ᵥ v)).2 ⟨0, Vector.get_cons_zero a v⟩

Premises used: Iff.mpr, List.Vector.get_cons_zero, List.Vector.mem_iff_get, Exists.intro, OfNat.ofNat, List.Vector.cons
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.head ∈ v.toList

Tactic:
(Vector.mem_iff_get v.head v).2 ⟨0, Vector.get_zero v⟩

Premises used: Iff.mpr, List.Vector.head, List.Vector.mem_iff_get, Exists.intro, List.Vector.get_zero, OfNat.ofNat
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a a' : α
v : Vector α n
ha' : a' ∈ v.toList
⊢ a' ∈ (a ::ᵥ v).toList

Tactic:
(Vector.mem_cons_iff a a' v).2 (Or.inr ha')

Premises used: Iff.mpr, List.Vector.mem_cons_iff, Or.inr
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α 0
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
False.elim (Vector.notMem_zero a v.tail ha)

Premises used: False.elim, List.Vector.notMem_zero, List.Vector.tail
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α 0
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
exact False.elim (Vector.notMem_zero a v.tail ha)

Premises used: False.elim, List.Vector.notMem_zero, List.Vector.tail
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n_1 : ℕ
a : α
n : ℕ
h : ∀ (v : Vector α n) (ha : a ∈ v.tail.toList), a ∈ v.toList
v : Vector α (n + 1)
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
(mem_succ_iff a v).2 (Or.inr ha)

Premises used: Iff.mpr, List.Vector.mem_succ_iff, Or.inr
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n_1 : ℕ
a : α
n : ℕ
h : ∀ (v : Vector α n) (ha : a ∈ v.tail.toList), a ∈ v.toList
v : Vector α (n + 1)
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
exact (mem_succ_iff a v).2 (Or.inr ha)

Premises used: Iff.mpr, List.Vector.mem_succ_iff, Or.inr
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
ha : a ∈ v.tail.toList
zero : ∀ (v : Vector α 0) (ha : a ∈ v.tail.toList), a ∈ v.toList
succ :
  ∀ (n : ℕ),
    (∀ (v : Vector α n) (ha : a ∈ v.tail.toList), a ∈ v.toList) →
      ∀ (v : Vector α (n + 1)) (ha : a ∈ v.tail.toList), a ∈ v.toList
⊢ a ∈ v.toList

Tactic:
induction n with
  | zero => exact False.elim (Vector.notMem_zero a v.tail ha)
  | succ n _ => exact (mem_succ_iff a v).2 (Or.inr ha)
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α n
f : α → β
rw : b ∈ List.map f v.toList ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b
rw₁ rw₂ : (∃ (a : α), a ∈ v.toList ∧ f a = b) ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b
⊢ b ∈ (map f v).toList ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b

Tactic:
rw [Vector.toList_map, List.mem_map]

Premises used: List.Vector.toList_map, List.mem_map
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
β : Type u_2
b : β
v : Vector α 0
f : α → β
⊢ ¬b ∈ (map f v).toList

Tactic:
simpa only [Vector.eq_nil v, Vector.map_nil, Vector.toList_nil] using List.not_mem_nil

Premises used: List.Vector.eq_nil, List.Vector.toList_nil, List.Vector.map_nil, List.not_mem_nil
-- Module: Mathlib.Data.Vector.Mem
Goal:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
rw : b = (map f v).head ∨ b ∈ (map f v).tail.toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
rw₁ : b = f v.head ∨ b ∈ (map f v).tail.toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
rw₂ : b = f v.head ∨ b ∈ (map f v.tail).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
rw₃ : (b = f v.head ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b) ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
rw₄ rw₅ :
  (f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b) ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b

Tactic:
rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]

Premises used: List.Vector.mem_map_iff, eq_comm, List.Vector.head_map, List.Vector.tail_map, List.Vector.mem_succ_iff
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
y : α
⊢ (x ::ᵥ xs).snoc y = x ::ᵥ xs.snoc y

Tactic:
rfl

Premises used: List.append, List.Vector.snoc, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
x : α
⊢ snoc nil x = x ::ᵥ nil

Tactic:
rfl

Premises used: List.append, List.Vector.snoc, List.Vector.cons, rfl
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
mk :
  ∀ (val : List α) (property : val.length = n),
    Eq (α := Vector α n.succ) (reverse (x ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
      (snoc (reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) x)
⊢ (x ::ᵥ xs).reverse = xs.reverse.snoc x

Tactic:
cases xs
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
mk :
  Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (val.reverse ++ [x]) ⋯ =
    HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val.reverse ⋯)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)
⊢ Eq (α := Vector α n.succ) (reverse (x ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
    (snoc (reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) x)

Tactic:
simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]

Premises used: List.Vector.toList_mk, List.reverse_cons, List.Vector.snoc, List.Vector.reverse, List.Vector.cons
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
⊢ Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (val.reverse ++ [x]) ⋯ =
    HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val.reverse ⋯)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)

Tactic:
congr
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
mk :
  ∀ (val : List α) (property : val.length = n),
    Eq (α := Vector α (n + 1)) (reverse (snoc (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) x))
      (x ::ᵥ reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
⊢ (xs.snoc x).reverse = x ::ᵥ xs.reverse

Tactic:
cases xs
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
mk :
  Eq (α := Vector α (n + 1))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
            (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)).toList.reverse
      ⋯)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (x :: val.reverse) ⋯)
⊢ Eq (α := Vector α (n + 1)) (reverse (snoc (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) x))
    (x ::ᵥ reverse (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))

Tactic:
simp only [reverse, snoc, cons, toList_mk]

Premises used: List.Vector.toList_mk, List.Vector.snoc, List.Vector.reverse, List.Vector.cons
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
mk :
  (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
          (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)).toList.reverse =
    x :: val.reverse
⊢ Eq (α := Vector α (n + 1))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
            (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)).toList.reverse
      ⋯)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (x :: val.reverse) ⋯)

Tactic:
congr
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
x : α
val : List α
property : val.length = n
⊢ (HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)
          (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] ⋯)).toList.reverse =
    x :: val.reverse

Tactic:
simp [toList, append_def]

Premises used: List.Vector.append_def, List.Vector.toList
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
val : α
⊢ Eq (α := Vector α (HAdd.hAdd (α := ℕ) 0 1)) (replicate (HAdd.hAdd (α := ℕ) 0 1) val) (snoc (replicate 0 val) val)

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
rhs : snoc (replicate (n + 1) val) val
| Eq (α := Vector α (n + 1 + 1)) (val ::ᵥ replicate (n + 1) val) (snoc (replicate (n + 1) val) val)

Tactic:
rhs
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
rw : (val ::ᵥ replicate n val).snoc val
| Eq (α := Vector α (n + 1 + 1)) (val ::ᵥ replicate (n + 1) val) (snoc (replicate (n + 1) val) val)

Tactic:
rhs; rw [replicate_succ]

Premises used: List.Vector.replicate_succ
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n_1 : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
succ : val ::ᵥ replicate (n + 1) val = val ::ᵥ (replicate n val).snoc val
succ₁ succ₂ : val ::ᵥ (replicate n val).snoc val = val ::ᵥ (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (val ::ᵥ replicate n val).snoc val

Tactic:
rw [snoc_cons, ih]

Premises used: List.Vector.snoc_cons
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
n : ℕ
val : α
zero : Eq (α := Vector α (HAdd.hAdd (α := ℕ) 0 1)) (replicate (HAdd.hAdd (α := ℕ) 0 1) val) (snoc (replicate 0 val) val)
succ :
  ∀ (n : ℕ) (ih : replicate (n + 1) val = (replicate n val).snoc val),
    Eq (α := Vector α (n + 1 + 1)) (replicate (n + 1 + 1) val) (snoc (replicate (n + 1) val) val)
⊢ replicate (n + 1) val = (replicate n val).snoc val

Tactic:
induction n with
  | zero => rfl
  | succ n ih =>
    rw [replicate_succ]
    conv => rhs; rw [replicate_succ]
    rw [snoc_cons, ih]

Premises used: List.Vector.replicate_succ, List.Vector.snoc_cons
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n_1 : ℕ
x : α
s : σ
xs : Vector α n_1
C : {n : ℕ} → Vector α n → Sort u_5
n : ℕ
v : Vector α n
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)
⊢ (fun {n : ℕ} (v : Vector α n) ↦ C v.reverse) v.reverse = C v

Tactic:
simp
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n_1 : ℕ
x_1 : α
s : σ
xs_1 : Vector α n_1
C : {n : ℕ} → Vector α n → Sort u_5
n_2 : ℕ
v : Vector α n_2
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)
n : ℕ
x : α
xs : Vector α n
r : C xs.reverse
⊢ C (xs.reverse.snoc x) = (fun {n : ℕ} (v : Vector α n) ↦ C v.reverse) (x ::ᵥ xs)

Tactic:
simp
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n_1 : ℕ
x : α
s : σ
xs : Vector α n_1
C : {n : ℕ} → Vector α n → Vector β n → Sort u_5
n : ℕ
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)
⊢ (fun {n : ℕ} (v : Vector α n) (w : Vector β n) ↦ C v.reverse w.reverse) v.reverse w.reverse = C v w

Tactic:
simp
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n_1 : ℕ
x_1 : α
s : σ
xs_1 : Vector α n_1
C : {n : ℕ} → Vector α n → Vector β n → Sort u_5
n_2 : ℕ
v : Vector α n_2
w : Vector β n_2
nil : C Vector.nil Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)
n : ℕ
x : α
y : β
xs : Vector α n
ys : Vector β n
r : C xs.reverse ys.reverse
⊢ C (xs.reverse.snoc x) (ys.reverse.snoc y) =
    (fun {n : ℕ} (v : Vector α n) (w : Vector β n) ↦ C v.reverse w.reverse) (x ::ᵥ xs) (y ::ᵥ ys)

Tactic:
simp
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
nil : map f (snoc Vector.nil x) = (map f Vector.nil).snoc (f x)
cons :
  ∀ {n : ℕ} {x_1 : α} {w : Vector α n},
    map f (w.snoc x) = (map f w).snoc (f x) → map f ((x_1 ::ᵥ w).snoc x) = (map f (x_1 ::ᵥ w)).snoc (f x)
⊢ map f (xs.snoc x) = (map f xs).snoc (f x)

Tactic:
induction xs
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (snoc nil x) = (map f nil).snoc (f x)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
n_1 : ℕ
x_1 : α
w : Vector α n_1
h : map f (w.snoc x) = (map f w).snoc (f x)
⊢ map f ((x_1 ::ᵥ w).snoc x) = (map f (x_1 ::ᵥ w)).snoc (f x)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
f : α → σ → σ × β
s : σ
⊢ mapAccumr f nil s = (s, nil)

Tactic:
rfl

Premises used: List.Vector.mapAccumr, List.Vector.nil, rfl
-- Module: Mathlib.Data.Vector.Snoc
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
f : α → σ → σ × β
s : σ
nil :
  mapAccumr f (snoc Vector.nil x) s =
    let q := f x s;
    let r := mapAccumr f Vector.nil q.1;
    (r.1, r.2.snoc q.2)
cons :
  ∀ {n : ℕ} {x_1 : α} {w : Vector α n},
    (mapAccumr f (w.snoc x) s =
        let q := f x s;
        let r := mapAccumr f w q.1;
        (r.1, r.2.snoc q.2)) →
      mapAccumr f ((x_1 ::ᵥ w).snoc x) s =
        let q := f x s;
        let r := mapAccumr f (x_1 ::ᵥ w) q.1;
        (r.1, r.2.snoc q.2)
⊢ mapAccumr f (xs.snoc x) s =
    let q := f x s;
    let r := mapAccumr f xs q.1;
    (r.1, r.2.snoc q.2)

Tactic:
induction xs