awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ (mapAccumr₂ f xs ys s₀).2 = map₂ (fun (x1 : α) (x2 : β) ↦ (f x1 x2 s₀).2) xs ys
have rw : (mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), (f x y s₀).2)) xs ys ()).2
Tactic: rw [Vector.map₂_eq_mapAccumr₂]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ (mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), (f x y s₀).2)) xs ys ()).2
have h : ∃ (R : σ → Unit → Prop),
  R s₀ () ∧
    ∀ {s : σ} {q : Unit} (a : α) (b : β),
      R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2
Tactic: apply mapAccumr₂_bisim_tail
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∃ (R : σ → Unit → Prop),
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2
have right : ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2
Tactic: use fun s _ => s ∈ S, h₀
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f xs s = (s, map (fun (x : α) ↦ (f x s).2) xs)
have nil : mapAccumr f nil s = (s, map (fun (x : α) ↦ (f x s).2) nil)
Tactic: induction xs using revInductionOn
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
nil : mapAccumr f Vector.nil s = (s, map (fun (x : α) ↦ (f x s).2) Vector.nil)
⊢ mapAccumr f xs s = (s, map (fun (x : α) ↦ (f x s).2) xs)
have snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α),
  mapAccumr f xs s = (s, map (fun (x : α) ↦ (f x s).2) xs) →
    mapAccumr f (xs.snoc x) s = (s, map (fun (x : α) ↦ (f x s).2) (xs.snoc x))
Tactic: induction xs using revInductionOn
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = s
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) xs ys)
have nil : mapAccumr₂ f nil nil s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) nil nil)
Tactic: induction xs, ys using revInductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = s
nil : mapAccumr₂ f Vector.nil Vector.nil s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) Vector.nil Vector.nil)
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) xs ys)
have snoc : ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
  mapAccumr₂ f xs ys s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) xs ys) →
    mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) (xs.snoc x) (ys.snoc y))
Tactic: induction xs, ys using revInductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s_1 : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
a : α
s s' : σ
h_1 : Membership.mem (γ := Set σ) Set.univ s
h_2 : Membership.mem (γ := Set σ) Set.univ s'
⊢ (f a s).2 = (f a s').2
have rw : f' a = (f a s').2
Tactic: rw [h, h]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s_1 : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
a : α
s s' : σ
h_1 : Membership.mem (γ := Set σ) Set.univ s
h_2 : Membership.mem (γ := Set σ) Set.univ s'
rw : f' a = (f a s').2
⊢ (f a s).2 = (f a s').2
have rw₁ : f' a = f' a
Tactic: rw [h, h]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
⊢ (mapAccumr f xs s).2 = map f' xs
have rw : map (fun (x : α) ↦ (f x s).2) xs = map f' xs
Tactic: rw [mapAccumr_eq_map Set.univ (Set.mem_univ _) (fun _ _ _ => Set.mem_univ _)
    (fun a s s' _ _ => by rw [h, h])]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → β → γ
s_1 : σ
h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b
a : α
b : β
s s' : σ
h_1 : Membership.mem (γ := Set σ) Set.univ s
h_2 : Membership.mem (γ := Set σ) Set.univ s'
⊢ (f a b s).2 = (f a b s').2
have rw : f' a b = (f a b s').2
Tactic: rw [h, h]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → β → γ
s_1 : σ
h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b
a : α
b : β
s s' : σ
h_1 : Membership.mem (γ := Set σ) Set.univ s
h_2 : Membership.mem (γ := Set σ) Set.univ s'
rw : f' a b = (f a b s').2
⊢ (f a b s).2 = (f a b s').2
have rw₁ : f' a b = f' a b
Tactic: rw [h, h]
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → Prod.{u_5, u_2} (σ × σ) β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
⊢ ∃ (R : σ × σ → σ → Prop),
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α),
        R s q → R (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧ (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2
have h₁ : (fun (x : σ × σ) (s : σ) ↦
      (match (motive := σ × σ → Prop) x with
        | (s₁, s₂) => s₂ = s ∧ s₁ = s :
        Prop))
    (s, s) s ∧
  ∀ {s : σ × σ} {q : σ} (a : α),
    (fun (x : σ × σ) (s : σ) ↦
          (match (motive := σ × σ → Prop) x with
            | (s₁, s₂) => s₂ = s ∧ s₁ = s :
            Prop))
        s q →
      (fun (x : σ × σ) (s : σ) ↦
            (match (motive := σ × σ → Prop) x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s :
              Prop))
          (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧
        (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2
Tactic: use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → Prod.{u_5, u_3} (σ × σ) γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
⊢ ∃ (R : σ × σ → σ → Prop),
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
        R s q →
          R (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
            (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2
have h₁ : (fun (x : σ × σ) (s : σ) ↦
      (match (motive := σ × σ → Prop) x with
        | (s₁, s₂) => s₂ = s ∧ s₁ = s :
        Prop))
    (s, s) s ∧
  ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
    (fun (x : σ × σ) (s : σ) ↦
          (match (motive := σ × σ → Prop) x with
            | (s₁, s₂) => s₂ = s ∧ s₁ = s :
            Prop))
        s q →
      (fun (x : σ × σ) (s : σ) ↦
            (match (motive := σ × σ → Prop) x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s :
              Prop))
          (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
        (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2
Tactic: use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr f' ys s
have nil : ∀ {s : σ}, mapAccumr₂ f nil nil s = mapAccumr f' nil 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]
Cleared hypotheses: s, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr f' ys s
have 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
Tactic: induction xs, ys using Vector.revInductionOn₂ generalizing s with
  | nil => rfl
  | snoc xs ys x y ih => simp [h x y s, ih]
Cleared hypotheses: s, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr f' xs s
have nil : ∀ {s : σ}, mapAccumr₂ f nil nil s = mapAccumr f' nil 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]
Cleared hypotheses: s, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr f' xs s
have 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
Tactic: induction xs, ys using Vector.revInductionOn₂ generalizing s with
  | nil => rfl
  | snoc xs ys x y ih => simp [h x y s, ih]
Cleared hypotheses: s, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f xs ys = map₂ f ys xs
have nil : map₂ f nil nil = map₂ f nil nil
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ map₂ f xs ys = map₂ f ys xs
have 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)
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s
have nil : ∀ {s : σ}, mapAccumr₂ f nil nil s = mapAccumr₂ f nil nil s
Tactic: induction xs, ys using Vector.inductionOn₂ generalizing s
Cleared hypotheses: s, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s
have 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
Tactic: induction xs, ys using Vector.inductionOn₂ generalizing s
Cleared hypotheses: s, xs, ys
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f xs ys = map₂ (flip f) ys xs
have nil : map₂ f nil nil = map₂ (flip f) nil nil
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ map₂ f xs ys = map₂ (flip f) ys xs
have 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)
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s
have nil : mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.MapLemmas (goal)
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
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s
have 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
Tactic: induction xs, ys using Vector.inductionOn₂
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ a ∈ v.toList ↔ ∃ (i : Fin n), v.get i = a
have 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 sorry (⟨i, h⟩ : Fin n)) = a
Tactic: simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get_toList]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ i < n
have rwa : ∀ (hi_1 : i < n) (h : v.toList.get (⟨i, hi⟩ : Fin v.toList.length) = a), i < n
Tactic: rwa [toList_length] at hi
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
n : ℕ
a a' : α
v : Vector α n
⊢ a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList
have rw : a' ∈ a :: v.toList ↔ a' = a ∨ a' ∈ v.toList
Tactic: rw [Vector.toList_cons, List.mem_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
n : ℕ
a a' : α
v : Vector α n
rw : a' ∈ a :: v.toList ↔ a' = a ∨ a' ∈ v.toList
⊢ a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList
have rw₁ : a' = a ∨ a' ∈ v.toList ↔ a' = a ∨ a' ∈ v.toList
Tactic: rw [Vector.toList_cons, List.mem_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
have obtain : ∀ (a' : α) (v' : Vector α n) (h : v = a' ::ᵥ v'), a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
Tactic: obtain ⟨a', v', h⟩ := exists_eq_cons v
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
have simp_rw : a ∈ (a' ::ᵥ v').toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList
Tactic: simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
have simp_rw₁ : a = a' ∨ a ∈ v'.toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList
Tactic: simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
have simp_rw₂ : a = a' ∨ a ∈ v'.toList ↔ a = a' ∨ a ∈ (a' ::ᵥ v').tail.toList
Tactic: simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList
have zero : ∀ (v : Vector α 0) (ha : a ∈ v.tail.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)
Cleared hypotheses: v, ha
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ a ∈ v.toList
have 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
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)
Cleared hypotheses: v, ha
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α n
f : α → β
⊢ b ∈ (map f v).toList ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b
have rw : b ∈ List.map f v.toList ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b
Tactic: rw [Vector.toList_map, List.mem_map]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ b ∈ (map f v).toList ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b
have rw₁ : (∃ (a : α), a ∈ v.toList ∧ f a = b) ↔ ∃ (a : α), a ∈ v.toList ∧ f a = b
Tactic: rw [Vector.toList_map, List.mem_map]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
have rw : b = (map f v).head ∨ b ∈ (map f v).tail.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]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
have rw₁ : b = f v.head ∨ b ∈ (map f v).tail.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]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
have rw₂ : b = f v.head ∨ b ∈ (map f v.tail).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]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
have 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
Tactic: rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]
-- Lean 4 proof step from Mathlib.Data.Vector.Mem (goal)
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
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ (a : α), a ∈ v.tail.toList ∧ f a = b
have 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
Tactic: rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (x ::ᵥ xs).reverse = xs.reverse.snoc x
have 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)
Tactic: cases xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
x : α
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)
have mk : Subtype.mk (p := fun (l : List α) ↦ l.length = n.succ) (val.reverse ++ [x]) sorry =
  HAppend.hAppend (α := Vector α n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val.reverse sorry)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = Nat.succ 0) [x] sorry)
Tactic: simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]
-- Lean 4 proof step from Mathlib.Data.Vector.Snoc (goal)
Goal:
α : Type u_1
n : ℕ
x : α
xs : Vector α n
⊢ (xs.snoc x).reverse = x ::ᵥ xs.reverse
have 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))
Tactic: cases xs
Cleared hypotheses: xs