awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
rw : (a ::ᵥ v).tail.get i = v.get i
⊢ (a ::ᵥ v).get i.succ = v.get i
have rw₁ : v.get i = v.get i
Tactic: rw [← get_tail_succ, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.head = v.last
have rw : v.reverse.toList.get (Fin.cast sorry 0) = v.toList.get (Fin.cast sorry (Fin.last n))
Tactic: rw [← get_zero, last_def, get_eq_get_toList, get_eq_get_toList]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
have simp_rw : v.toList.reverse.get (Fin.cast sorry 0) = v.toList.get (Fin.cast sorry (Fin.last n))
Tactic: simp_rw [toList_reverse]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (List.scanl f b v.toList).length = n + 1
have rw : v.toList.length + 1 = n + 1
Tactic: rw [List.length_scanl, toList_length]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
rw : v.toList.length + 1 = n + 1
⊢ (List.scanl f b v.toList).length = n + 1
have rw₁ : n + 1 = n + 1
Tactic: rw [List.length_scanl, toList_length]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
⊢ scanl f b nil = b ::ᵥ nil
have x : ∀ (m : Fin (HAdd.hAdd (α := ℕ) 0 1)), (scanl f b nil).get m = (b ::ᵥ nil).get m
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v
have a : (scanl f b (x ::ᵥ v)).toList = (b ::ᵥ scanl f (f b x) v).toList
Tactic: apply Vector.eq
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil
have rw : scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil
Tactic: rw [← cons_head_tail v]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (scanl f b v).head = b
have zero : ∀ (v : Vector α 0), (scanl f b v).head = b
Tactic: cases n
Cleared hypotheses: n, v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
zero : ∀ (v : Vector α 0), (scanl f b v).head = b
⊢ (scanl f b v).head = b
have succ : ∀ (n : ℕ) (v : Vector α (n + 1)), (scanl f b v).head = b
Tactic: cases n
Cleared hypotheses: n, v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b
have this : v = nil
Tactic: have : v = nil := by simp only [eq_iff_true_of_subsingleton]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
⊢ (scanl f b v).head = b
have succ : (scanl f b (v.head ::ᵥ v.tail)).head = b
Tactic: rw [← cons_head_tail v]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have zero : ∀ (v : Vector α 0) (i : Fin 0), (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Tactic: rcases n with - | n
Cleared hypotheses: n, v, i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
i : Fin n
zero : ∀ (v : Vector α 0) (i : Fin 0), (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have succ : ∀ (n : ℕ) (v : Vector α (n + 1)) (i : Fin (n + 1)),
  (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Tactic: rcases n with - | n
Cleared hypotheses: n, v, i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have i0 : i = 0
Tactic: have i0 : i = 0 := Fin.eq_zero _
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
i0 : i = 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have succ : (b ::ᵥ f b v.head ::ᵥ nil).get 1 = f b v.head
Tactic: simp [scanl_singleton, i0, get_zero]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have succ : (scanl f (f b v.head) v.tail).get i = f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)
Tactic: rw [← cons_head_tail v, scanl_cons, get_cons_succ]
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get i =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)
have succ : (scanl f (f b v.head) v.tail).get 0 =
  f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
succ :
  (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)
⊢ (scanl f (f b v.head) v.tail).get i =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)
have succ₁ : ∀ (i : Fin (n + 1)),
  (scanl f (f b v.head) v.tail).get i.succ =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have succ : ∀ (b : β) (v : Vector α (HAdd.hAdd (α := ℕ) 0 1)) (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
  (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Tactic: induction n generalizing b with
  | zero =>
    have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]
  | succ n hn =>
    rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp
    · intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]
Cleared hypotheses: b, n, v, i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
succ :
  ∀ (b : β) (v : Vector α (HAdd.hAdd (α := ℕ) 0 1)) (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
have succ₁ : ∀ (n : ℕ)
  (hn :
    ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
      (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i))
  (b : β) (v : Vector α (n + 1 + 1)) (i : Fin (n + 1 + 1)),
  (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Tactic: induction n generalizing b with
  | zero =>
    have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]
  | succ n hn =>
    rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp
    · intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]
Cleared hypotheses: b, n, v, i
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
m : Type u_6 → Type u_7
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ Eq.{u_7 + 1} (α := m (Vector α (n + 1))) (mOfFn fun (i : Fin (n + 1)) ↦ pure (f i)) (pure (ofFn f))
have rw : Eq.{u_7 + 1} (α := m (Vector α (n + 1)))
  (do
    let a ← pure (f 0)
    let v ← pure (ofFn fun (i : Fin n) ↦ f i.succ)
    pure (a ::ᵥ v))
  (pure (f 0 ::ᵥ ofFn fun (i : Fin n) ↦ f i.succ))
Tactic: rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
-- 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 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
v : Vector α 0
⊢ C v
have zero : C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry)
Tactic: rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
Cleared hypotheses: v
-- 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 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v : Vector α (n + 1)
⊢ C v
have succ : (v_property : List.length.{u_1} (α := α) [] = n + 1) →
  C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property)
Tactic: rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
Cleared hypotheses: v
-- 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 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v : Vector α (n + 1)
succ :
  (v_property : List.length.{u_1} (α := α) [] = n + 1) →
    C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property)
⊢ C v
have succ₁ : (a : α) →
  (v : List α) →
    (v_property : (a :: v).length = n + 1) →
      C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)
Tactic: rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
Cleared hypotheses: v
-- 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 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
n : ℕ
v : Vector α n
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C v
have zero : (v : Vector α 0) → C v
Tactic: induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)
Cleared hypotheses: n, v
-- 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 : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
n : ℕ
v : Vector α n
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
zero : (v : Vector α 0) → C v
⊢ C v
have succ : (n : ℕ) → (ih : (v : Vector α n) → C v) → (v : Vector α (n + 1)) → C v
Tactic: induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)
Cleared hypotheses: n, v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
v : Vector α 0
w : Vector β 0
⊢ C v w
have zero : C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry) w
Tactic: rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
w : Vector β 0
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) w
have zero : C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry)
  (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] sorry)
Tactic: rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
v : Vector α (n + 1)
w : Vector β (n + 1)
⊢ C v w
have succ : (v_property : List.length.{u_1} (α := α) [] = n + 1) →
  C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property) w
Tactic: rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
v : Vector α (n + 1)
w : Vector β (n + 1)
succ :
  (v_property : List.length.{u_1} (α := α) [] = n + 1) →
    C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property) w
⊢ C v w
have succ₁ : (a : α) →
  (v : List α) →
    (v_property : (a :: v).length = n + 1) →
      C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property) w
Tactic: rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (n + 1)
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property) w
have succ : (w_property : List.length.{u_6} (α := β) [] = n + 1) →
  C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) [] w_property)
Tactic: rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (n + 1)
a : α
v : List α
v_property : (a :: v).length = n + 1
succ :
  (w_property : List.length.{u_6} (α := β) [] = n + 1) →
    C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)
      (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) [] w_property)
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property) w
have succ₁ : (b : β) →
  (w : List β) →
    (w_property : (b :: w).length = n + 1) →
      C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)
        (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: w) w_property)
Tactic: rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : (a :: v).length = n + 1
b : β
w : List β
w_property : (b :: w).length = n + 1
⊢ C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: w) w_property)
have succ : C (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) v sorry)
  (Subtype.mk (p := fun (l : List β) ↦ l.length = n) w sorry)
Tactic: apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C v w
have zero : (v : Vector α 0) → (w : Vector β 0) → C v w
Tactic: induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
    cases w_property
    apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih
Cleared hypotheses: v, w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
zero : (v : Vector α 0) → (w : Vector β 0) → C v w
⊢ C v w
have succ : (n : ℕ) → (ih : (v : Vector α n) → (w : Vector β n) → C v w) → (v : Vector α (n + 1)) → (w : Vector β (n + 1)) → C v w
Tactic: induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
    cases w_property
    apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih
Cleared hypotheses: v, w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
u : Vector α 0
v : Vector β 0
w : Vector γ 0
⊢ C u v w
have zero : C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry) v w
Tactic: rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
v : Vector β 0
w : Vector γ 0
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) v w
have zero : C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry) (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] sorry) w
Tactic: rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
w : Vector γ 0
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯) w
have zero : C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] sorry)
  (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] sorry) (Subtype.mk (p := fun (l : List γ) ↦ l.length = 0) [] sorry)
Tactic: rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
u : Vector α (n + 1)
v : Vector β (n + 1)
w : Vector γ (n + 1)
⊢ C u v w
have succ : (u_property : List.length.{u_1} (α := α) [] = n + 1) →
  C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] u_property) v w
Tactic: rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Data.Vector.Basic (goal)
Goal:
α : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
σ : Type u_4
φ : Type u_5
m n_1 : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
u : Vector α (n + 1)
v : Vector β (n + 1)
w : Vector γ (n + 1)
succ :
  (u_property : List.length.{u_1} (α := α) [] = n + 1) →
    C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] u_property) v w
⊢ C u v w
have succ₁ : (a : α) →
  (u : List α) →
    (u_property : (a :: u).length = n + 1) →
      C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property) v w
Tactic: rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
Cleared hypotheses: u