awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ (l.insertIdx (↑i : ℕ) a).insertIdx ((↑j : ℕ) + 1) b = (l.insertIdx (↑j : ℕ) b).insertIdx (↑i : ℕ) a
have x : (↑i : ℕ) ≤ (↑j : ℕ)
Tactic: apply List.insertIdx_comm
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
x : (↑i : ℕ) ≤ (↑j : ℕ)
⊢ (l.insertIdx (↑i : ℕ) a).insertIdx ((↑j : ℕ) + 1) b = (l.insertIdx (↑j : ℕ) b).insertIdx (↑i : ℕ) a
have x₁ : (↑j : ℕ) ≤ l.length
Tactic: apply List.insertIdx_comm
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ (↑j : ℕ) ≤ l.length
have x : (↑j : ℕ) ≤ n
Tactic: rw [hl]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).get i = a
have mk : ∀ (val : List α) (property : val.length = n),
  (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) i a).get i = a
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
i : Fin n
a : α
val : List α
property : val.length = n
⊢ (set (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property) i a).get i = a
have 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
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ (v.set i a).get j = v.get j
have 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
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
i j : Fin n
h : i ≠ j
a : α
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
have 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
Tactic: cases i
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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
⊢ (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
have 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)
Tactic: cases j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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⟩
⊢ (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)
have mk : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (val.set val_1 a) val_2 sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) val val_2 sorry
Tactic: simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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⟩
⊢ 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 ⋯
have mk : val_1 ≠ val_2
Tactic: rw [List.getElem_set_of_ne]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
⊢ (v.set i a).get j = if i = j then a else v.get j
have pos : i = j → (v.set i a).get j = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
pos : i = j → (v.set i a).get j = a
⊢ (v.set i a).get j = if i = j then a else v.get j
have neg : ¬i = j → (v.set i a).get j = v.get j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h : ¬i = j
⊢ (v.set i a).get j = v.get j
have neg : v.get j = v.get j
Tactic: rwa [get_set_of_ne]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h : ¬i = j
neg : v.get j = v.get j
⊢ (v.set i a).get j = v.get j
have neg₁ : i ≠ j
Tactic: rwa [get_set_of_ne]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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
have 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
Tactic: refine (List.prod_set v.toList i a).trans ?_
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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
have 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
Tactic: refine (List.prod_set' v.toList i a).trans ?_
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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
⊢ F (Vector β v.length) = F (Vector β n)
have rw : F (Vector β n) = F (Vector β n)
Tactic: rw [Hv]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u
x : List α
⊢ 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 ⋯))
have dsimp : Eq (α := Id (Vector α x.length)) (traverseAux pure x)
  (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x sorry))
Tactic: dsimp [Vector.traverse, cast]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u
x : List α
⊢ Eq (α := Id (Vector α x.length)) (traverseAux pure x)
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))
have nil : Eq.{u + 1} (α := Id (Vector α (List.length.{u} (α := α) []))) (traverseAux pure [])
  (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = List.length.{u} (α := α) []) [] sorry))
Tactic: induction x with | nil => rfl | cons x xs IH => simp! [IH]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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} (α := α) []) [] ⋯))
⊢ Eq (α := Id (Vector α x.length)) (traverseAux pure x)
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))
have 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 sorry))),
  Eq (α := Id (Vector α (x :: xs).length)) (traverseAux pure (x :: xs))
    (pure (Subtype.mk (p := fun (l : List α) ↦ l.length = (x :: xs).length) (x :: xs) sorry))
Tactic: induction x with | nil => rfl | cons x xs IH => simp! [IH]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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 β
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) nil = Comp.mk (Vector.traverse f <$> Vector.traverse g nil)
have nil : Eq.{u + 1} (α := Comp G F (Vector γ 0)) (pure nil) (Comp.mk (pure (pure nil)))
Tactic: simp! [cast, *, functor_norm]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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 β
n_1 : ℕ
x : α
w : Vector α n_1
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w = Comp.mk (Vector.traverse f <$> Vector.traverse g w)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ w) = Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))
have cons : cons <$> (Comp.mk ∘ Functor.map f ∘ g) x <*> Comp.mk (Vector.traverse f <$> Vector.traverse g w) =
  Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))
Tactic: rw [Vector.traverse_def, ih]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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 β
x : Vector α n
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)
have nil : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) nil = Comp.mk (Vector.traverse f <$> Vector.traverse g nil)
Tactic: induction x with
  | nil =>
    simp! [cast, *, functor_norm]
    rfl
  | cons ih =>
    rw [Vector.traverse_def, ih]
    simp [functor_norm, Function.comp_def]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
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 β
x : Vector α n
nil :
  Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) Vector.nil =
    Comp.mk (Vector.traverse f <$> Vector.traverse g Vector.nil)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)
have cons : ∀ {n : ℕ} {x : α} {w : Vector α n}
  (ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) w = Comp.mk (Vector.traverse f <$> Vector.traverse g w)),
  Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ w) = Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ w))
Tactic: induction x with
  | nil =>
    simp! [cast, *, functor_norm]
    rfl
  | cons ih =>
    rw [Vector.traverse_def, ih]
    simp [functor_norm, Function.comp_def]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α β : Type u_6
f : α → β
x : List α
⊢ Eq (α := Id (Vector β x.length))
    (Vector.traverse (pure ∘ f) (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯))
    (pure (map f (Subtype.mk (p := fun (l : List α) ↦ l.length = x.length) x ⋯)))
have simp! : Eq (α := Id (Vector β x.length)) (traverseAux (pure ∘ f) x)
  (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = x.length) (List.map f x) sorry))
Tactic: simp!
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α β : Type u_6
f : α → β
x : List α
⊢ Eq (α := Id (Vector β x.length)) (traverseAux (pure ∘ f) x)
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = x.length) (List.map f x) ⋯))
have nil : Eq (α := Id (Vector β (List.length.{u_6} (α := α) []))) (traverseAux (pure ∘ f) [])
  (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = List.length.{u_6} (α := α) []) (List.map f []) sorry))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α β : Type u_6
f : α → β
x : List α
nil :
  Eq (α := Id (Vector β (List.length.{u_6} (α := α) []))) (traverseAux (pure ∘ f) [])
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = List.length.{u_6} (α := α) []) (List.map f []) ⋯))
⊢ Eq (α := Id (Vector β x.length)) (traverseAux (pure ∘ f) x)
    (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = x.length) (List.map f x) ⋯))
have cons : ∀ (head : α) (tail : List α),
  Eq (α := Id (Vector β tail.length)) (traverseAux (pure ∘ f) tail)
      (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = tail.length) (List.map f tail) sorry)) →
    Eq (α := Id (Vector β (head :: tail).length)) (traverseAux (pure ∘ f) (head :: tail))
      (pure (Subtype.mk (p := fun (l : List β) ↦ l.length = (head :: tail).length) (List.map f (head :: tail)) sorry))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n_1 : ℕ
x : α
w : Vector α n_1
ih :
  Eq (α := G (Vector β n_1)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) w)
⊢ Eq (α := G (Vector β n_1.succ)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f (x ::ᵥ w)))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (x ::ᵥ w))
have cons : Eq (α := G (Vector β n_1.succ))
  (cons <$> (fun {α : Type u} ↦ η.app α) (f x) <*> (fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
  (cons <$> ((fun {α : Type u} ↦ η.app α) ∘ f) x <*> (fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
Tactic: rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ Eq (α := G (Vector β n)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f x))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have nil : Eq (α := G (Vector β 0)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f nil))
  (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) nil)
Tactic: induction x with
  | nil => simp! [functor_norm, cast, η.preserves_pure]
  | cons ih =>
    rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
    rfl
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
n : ℕ
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
nil :
  Eq (α := G (Vector β 0)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f Vector.nil))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) Vector.nil)
⊢ Eq (α := G (Vector β n)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f x))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have cons : ∀ {n : ℕ} {x : α} {w : Vector α n}
  (ih :
    Eq (α := G (Vector β n)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f w))
      (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) w)),
  Eq (α := G (Vector β n.succ)) ((fun {α : Type u} ↦ η.app α) (Vector.traverse f (x ::ᵥ w)))
    (Vector.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (x ::ᵥ w))
Tactic: induction x with
  | nil => simp! [functor_norm, cast, η.preserves_pure]
  | cons ih =>
    rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
    rfl
Cleared hypotheses: x
-- 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 : ℕ
α_1 : Type u
x : flip Vector n α_1
⊢ id <$> x = x
have mk : ∀ (val : List α_1) (property : val.length = n),
  Eq.{u + 1} (α := flip Vector n α_1) (id <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
    (Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
Tactic: cases x
Cleared hypotheses: x
-- 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 : ℕ
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : flip Vector n α_1
⊢ (h ∘ g) <$> x = h <$> g <$> x
have mk : ∀ (val : List α_1) (property : val.length = n),
  Eq (α := flip Vector n γ_1) ((h ∘ g) <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
    (h <$> g <$> Subtype.mk (p := fun (l : List α_1) ↦ l.length = n) val property)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
xs : Vector α n
⊢ HAppend.hAppend (β := Vector α 0) xs nil = xs
have mk : ∀ (val : List α) (property : val.length = n),
  Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property ++ nil =
    Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property
Tactic: cases xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
i : Fin n_1.succ
⊢ (map₂ f (a ::ᵥ x) (b ::ᵥ y)).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
have cons : (f a b ::ᵥ map₂ f x y).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
Tactic: rw [map₂_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
i : Fin n_1.succ
⊢ (f a b ::ᵥ map₂ f x y).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
have cons : (f a b ::ᵥ map₂ f x y).get 0 = f ((a ::ᵥ x).get 0) ((b ::ᵥ y).get 0)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n_1 : ℕ
a : α
b : β
x : Vector α n_1
y : Vector β n_1
ih : ∀ (i : Fin n_1), (map₂ f x y).get i = f (x.get i) (y.get i)
i : Fin n_1.succ
cons : (f a b ::ᵥ map₂ f x y).get 0 = f ((a ::ᵥ x).get 0) ((b ::ᵥ y).get 0)
⊢ (f a b ::ᵥ map₂ f x y).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
have cons₁ : ∀ (i : Fin n_1), (f a b ::ᵥ map₂ f x y).get i.succ = f ((a ::ᵥ x).get i.succ) ((b ::ᵥ y).get i.succ)
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)
have nil : ∀ (i : Fin 0), (map₂ f nil nil).get i = f (get nil i) (get nil i)
Tactic: induction v₁, v₂ using inductionOn₂ with
  | nil =>
    exact Fin.elim0 i
  | cons ih =>
    rw [map₂_cons]
    cases i using Fin.cases
    · simp only [get_zero, head_cons]
    · simp only [get_cons_succ, ih]
Cleared hypotheses: v₁, v₂, i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
nil : ∀ (i : Fin 0), (map₂ f Vector.nil Vector.nil).get i = f (get Vector.nil i) (get Vector.nil i)
⊢ (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)
have cons : ∀ {n : ℕ} {a : α} {b : β} {x : Vector α n} {y : Vector β n}
  (ih : ∀ (i : Fin n), (map₂ f x y).get i = f (x.get i) (y.get i)) (i : Fin n.succ),
  (map₂ f (a ::ᵥ x) (b ::ᵥ y)).get i = f ((a ::ᵥ x).get i) ((b ::ᵥ y).get i)
Tactic: induction v₁, v₂ using inductionOn₂ with
  | nil =>
    exact Fin.elim0 i
  | cons ih =>
    rw [map₂_cons]
    cases i using Fin.cases
    · simp only [get_zero, head_cons]
    · simp only [get_cons_succ, ih]
Cleared hypotheses: v₁, v₂, i
-- Lean 4 proof step from Mathlib.Data.Vector.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (l.eraseIdx (↑i : ℕ)).length = n - 1
have rw : l.length - 1 = n - 1
Tactic: rw [l.length_eraseIdx_of_lt]
-- Lean 4 proof step from Mathlib.Data.Vector.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
rw : l.length - 1 = n - 1
⊢ (l.eraseIdx (↑i : ℕ)).length = n - 1
have rw₁ : (↑i : ℕ) < l.length
Tactic: rw [l.length_eraseIdx_of_lt]
-- Lean 4 proof step from Mathlib.Data.Vector.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ l.length - 1 = n - 1
have rw : n - 1 = n - 1
Tactic: rw [p]
-- Lean 4 proof step from Mathlib.Data.Vector.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p_1 : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (↑i : ℕ) < l.length
have rw : (↑i : ℕ) < n
Tactic: rw [p]
-- Lean 4 proof step from Mathlib.Data.Vector.Defs (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (cons a v).toList = a :: v.toList
have mk : ∀ (val : List α) (property : val.length = n),
  toList (n := n.succ) (cons a (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) =
    a :: 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.Defs (goal)
Goal:
α : Type u_1
n m : ℕ
v : Vector α m
⊢ (drop n v).toList = List.drop n v.toList
have mk : ∀ (val : List α) (property : val.length = m),
  toList (n := m - n) (drop n (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property)) =
    List.drop n (toList (n := m) (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property))
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Defs (goal)
Goal:
α : Type u_1
n m : ℕ
v : Vector α m
⊢ (take n v).toList = List.take n v.toList
have mk : ∀ (val : List α) (property : val.length = m),
  toList (n := min n m) (take n (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property)) =
    List.take n (toList (n := m) (Subtype.mk (p := fun (l : List α) ↦ l.length = m) val property))
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
⊢ mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector γ n :=
      mapAccumr
        (fun (x : α) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs (s₁, s₂);
    (m.1.1, m.2)
have nil : ∀ {s₁ : σ₁} {s₂ : σ₂},
  mapAccumr f₁ (mapAccumr f₂ nil s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector γ 0 :=
      mapAccumr
        (fun (x : α) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        nil (s₁, s₂);
    (m.1.1, m.2)
Tactic: induction xs using Vector.revInductionOn generalizing s₁ s₂
Cleared hypotheses: s₁, s₂, xs