awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.Basic
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
succ : (n : ℕ) → (ih : (v : Vector α n) → C v) → (v : Vector α (n + 1)) → C v
⊢ 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⟩)
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ (inductionOn (C := fun (x : ℕ) (x_1 : Vector α x) ↦ C x_1) Vector.nil nil fun {n : ℕ} {x : α} {w : Vector α n} ↦
      cons) =
    nil

Tactic:
rfl

Premises used: List.Vector.inductionOn, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_6
n : ℕ
x : α
v : Vector α n
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ ((x ::ᵥ v).inductionOn (C := fun (x : ℕ) (x_1 : Vector α x) ↦ C x_1) nil fun {n : ℕ} {x : α} {w : Vector α n} ↦
      cons) =
    cons (v.inductionOn (C := fun (x : ℕ) (x_1 : Vector α x) ↦ C x_1) nil fun {n : ℕ} {x : α} {w : Vector α n} ↦ cons)

Tactic:
rfl

Premises used: List.Vector, List.Vector.inductionOn, rfl
-- Module: Mathlib.Data.Vector.Basic
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
zero : C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) w
⊢ C v w

Tactic:
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
-- Module: Mathlib.Data.Vector.Basic
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
zero :
  C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯)
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) w

Tactic:
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
-- Module: Mathlib.Data.Vector.Basic
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)
⊢ C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯)

Tactic:
exact nil
-- Module: Mathlib.Data.Vector.Basic
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
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
⊢ C v w

Tactic:
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
-- Module: Mathlib.Data.Vector.Basic
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)
v_property : List.length.{u_1} (α := α) [] = n + 1
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] v_property) w

Tactic:
cases v_property
-- Module: Mathlib.Data.Vector.Basic
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)
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)
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: v) v_property) w

Tactic:
rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
-- Module: Mathlib.Data.Vector.Basic
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
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:
cases w_property
-- Module: Mathlib.Data.Vector.Basic
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
succ :
  C (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) v ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n) w ⋯)
⊢ 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:
apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
-- Module: Mathlib.Data.Vector.Basic
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) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) v ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n) w ⋯)

Tactic:
apply ih
-- Module: Mathlib.Data.Vector.Basic
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
succ :
  (n : ℕ) → (ih : (v : Vector α n) → (w : Vector β n) → C v w) → (v : Vector α (n + 1)) → (w : Vector β (n + 1)) → C v w
⊢ 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
-- Module: Mathlib.Data.Vector.Basic
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
zero : C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) v w
⊢ C u v w

Tactic:
rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
-- Module: Mathlib.Data.Vector.Basic
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
zero :
  C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯) w
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) v w

Tactic:
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
-- Module: Mathlib.Data.Vector.Basic
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
zero :
  C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯) (Subtype.mk (p := fun (l : List γ) ↦ l.length = 0) [] ⋯)
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯) (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯) w

Tactic:
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
-- Module: Mathlib.Data.Vector.Basic
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)
⊢ C (n := 0) (Subtype.mk (p := fun (l : List α) ↦ l.length = 0) [] ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = 0) [] ⋯) (Subtype.mk (p := fun (l : List γ) ↦ l.length = 0) [] ⋯)

Tactic:
exact nil
-- Module: Mathlib.Data.Vector.Basic
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
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
⊢ C u v w

Tactic:
rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
-- Module: Mathlib.Data.Vector.Basic
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
v : Vector β (n + 1)
w : Vector γ (n + 1)
u_property : List.length.{u_1} (α := α) [] = n + 1
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) [] u_property) v w

Tactic:
cases u_property
-- Module: Mathlib.Data.Vector.Basic
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
v : Vector β (n + 1)
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
succ :
  (v_property : List.length.{u_6} (α := β) [] = n + 1) →
    C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
      (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) [] v_property) w
succ₁ :
  (b : β) →
    (v : List β) →
      (v_property : (b :: v).length = n + 1) →
        C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
          (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property) w
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property) v w

Tactic:
rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
-- Module: Mathlib.Data.Vector.Basic
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
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
v_property : List.length.{u_6} (α := β) [] = n + 1
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) [] v_property) w

Tactic:
cases v_property
-- Module: Mathlib.Data.Vector.Basic
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
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
succ :
  (w_property : List.length.{u_7} (α := γ) [] = n + 1) →
    C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
      (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
      (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) [] w_property)
succ₁ :
  (c : γ) →
    (w : List γ) →
      (w_property : (c :: w).length = n + 1) →
        C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
          (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
          (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) (c :: w) w_property)
⊢ C (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property) w

Tactic:
rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
-- Module: Mathlib.Data.Vector.Basic
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
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
w_property : List.length.{u_7} (α := γ) [] = n + 1
⊢ C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
    (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) [] w_property)

Tactic:
cases w_property
-- Module: Mathlib.Data.Vector.Basic
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
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
c : γ
w : List γ
w_property : (c :: w).length = n + 1
succ :
  C (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) u ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n) v ⋯) (Subtype.mk (p := fun (l : List γ) ↦ l.length = n) w ⋯)
⊢ C (n := n + 1) (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1) (a :: u) u_property)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n + 1) (b :: v) v_property)
    (Subtype.mk (p := fun (l : List γ) ↦ l.length = n + 1) (c :: w) w_property)

Tactic:
apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
-- Module: Mathlib.Data.Vector.Basic
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
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
c : γ
w : List γ
w_property : (c :: w).length = n + 1
⊢ C (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) u ⋯)
    (Subtype.mk (p := fun (l : List β) ↦ l.length = n) v ⋯) (Subtype.mk (p := fun (l : List γ) ↦ l.length = n) w ⋯)

Tactic:
apply ih
-- Module: Mathlib.Data.Vector.Basic
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
u : Vector α n
v : Vector β n
w : Vector γ n
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)
zero : (u : Vector α 0) → (v : Vector β 0) → (w : Vector γ 0) → C u v w
succ :
  (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
⊢ C u v w

Tactic:
induction n with
  | zero =>
    rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
    cases u_property
    rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
    cases w_property
    apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih
-- Module: Mathlib.Data.Vector.Basic
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
xs : List α
property : xs.length = n
⊢ Array α = Array α

Tactic:
rfl
-- Module: Mathlib.Data.Vector.Basic
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
a_1 a : α
i : Fin (n + 1)
v : Vector α n
rw : (if (↑i : ℕ) ≤ n then n + 1 else n) = n + 1
⊢ ((↑v : List α).insertIdx (↑i : ℕ) a).length = n + 1

Tactic:
rw [List.length_insertIdx, v.2]

Premises used: List.length_insertIdx, Subtype.property
-- Module: Mathlib.Data.Vector.Basic
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
a_1 a : α
i : Fin (n + 1)
v : Vector α n
isTrue : (↑i : ℕ) ≤ n → n + 1 = n + 1
isFalse : ¬(↑i : ℕ) ≤ n → n = n + 1
⊢ (if (↑i : ℕ) ≤ n then n + 1 else n) = n + 1

Tactic:
split
-- Module: Mathlib.Data.Vector.Basic
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
a_1 a : α
i : Fin (n + 1)
v : Vector α n
h : (↑i : ℕ) ≤ n
⊢ n + 1 = n + 1

Tactic:
lia
-- Module: Mathlib.Data.Vector.Basic
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
a_1 a : α
i : Fin (n + 1)
v : Vector α n
h : ¬(↑i : ℕ) ≤ n
⊢ n = n + 1

Tactic:
lia
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
i : Fin (n + 1)
v : Vector α n
⊢ (↑(insertIdx a i v) : List α) = (↑v : List α).insertIdx (↑i : ℕ) a

Tactic:
rfl

Premises used: List.insertIdx, List.modifyTailIdx, rfl
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin (n + 1)
⊢ eraseIdx i (insertIdx a i v) = v

Tactic:
Subtype.ext (List.eraseIdx_insertIdx_self ..)

Premises used: List.Vector, List.eraseIdx_insertIdx_self, Subtype.ext
-- Module: Mathlib.Data.Vector.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
dsimp :
  Eq (α := Vector α (n + 1))
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (((↑v : List α).insertIdx j a).eraseIdx
        (↑(if (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < (⟨j, hj⟩ : Fin (n + 2)) then (⟨i, ⋯⟩ : Fin (n + 1 + 1))
            else (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1))) :
          ℕ))
      ⋯)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = n + 1)
      (List.insertIdx
        (↑(match (motive := Vector α (n + 1) → Vector α n) v with
            | ⟨l, p⟩ => Subtype.mk (p := fun (l : List α) ↦ l.length = n) (l.eraseIdx i) ⋯) :
          List α)
        (↑(if h : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯) : ℕ) a)
      ⋯)
⊢ eraseIdx ((⟨j, hj⟩ : Fin (n + 2)).succAbove (⟨i, hi⟩ : Fin (n + 1))) (insertIdx a (⟨j, hj⟩ : Fin (n + 2)) v) =
    insertIdx a (⟨i, hi⟩.predAbove ⟨j, hj⟩) (eraseIdx ⟨i, hi⟩ v)

Tactic:
dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]

Premises used: Fin.succAbove, Fin.predAbove, List.Vector.insertIdx, List.Vector.eraseIdx