Lemmas for new operations on Fin-indexed (heterogeneous) vectors

@[implicit_reducible]

instance Fin.instUniqueForallOfNatNat_starlib {α : Sort u} : Unique (Fin 0 → α)

@[implicit_reducible]

instance Fin.instUniqueForall_starlib {α : Fin 0 → Sort u} : Unique ((i : Fin 0) → α i)

@[simp]

theorem Fin.dcons_zero {n : ℕ} {motive : Fin (n + 1) → Sort u} (a : motive 0) (v : (i : Fin n) → motive i.succ) : (a ::ᵈ v) 0 = a

@[simp]

theorem Fin.vcons_zero {n : ℕ} {α : Sort u} (a : α) (v : Fin n → α) : (a ::ᵛ v) 0 = a

@[simp]

theorem Fin.dcons_succ {n : ℕ} {motive : Fin (n + 1) → Sort u} (a : motive 0) (v : (i : Fin n) → motive i.succ) (i : Fin n) : (a ::ᵈ v) i.succ = v i

@[simp]

theorem Fin.vcons_succ {n : ℕ} {α : Sort u} (a : α) (v : Fin n → α) (i : Fin n) : (a ::ᵛ v) i.succ = v i

@[csimp]

theorem Fin.dcons_eq_cons : @dcons = @cons

dcons is equal to cons. Marked as csimp to allow for switching to the cons implementation during execution.

theorem Fin.vcons_eq_cons {n : ℕ} {α : Sort u} (a : α) (v : Fin n → α) : a ::ᵛ v = cons a v

@[simp]

theorem Fin.dcons_one {n : ℕ} {motive : Fin (n + 2) → Sort u} (a : motive 0) (v : (i : Fin (n + 1)) → motive i.succ) : (a ::ᵈ v) 1 = v 0

@[simp]

theorem Fin.vcons_one {n : ℕ} {α : Sort u} (a : α) (v : Fin (n + 1) → α) : (a ::ᵛ v) 1 = v 0

@[simp]

theorem Fin.vcons_empty {α : Sort u} (a : α) : !v[a] = !v[a]

@[simp]

theorem Fin.vcons_of_one {α : Sort u} (a : α) {i : Fin 1} : !v[a] i = match i with | 0 => a

@[simp]

theorem Fin.tail_vcons {n : ℕ} {α : Sort u} (a : α) (v : Fin n → α) : tail (a ::ᵛ v) = v

@[simp]

theorem Fin.vcons_self_tail {n : ℕ} {α : Sort u} (v : Fin (n + 1) → α) : v 0 ::ᵛ tail v = v

theorem Fin.vcons_right_injective {n : ℕ} {α : Sort u} (a : α) : Function.Injective (vcons a)

theorem Fin.vcons_left_injective {n : ℕ} {α : Sort u} (v : Fin n → α) : Function.Injective fun (a : α) => a ::ᵛ v

theorem Fin.vcons_injective2 {n : ℕ} {α : Sort u} : Function.Injective2 vcons

theorem Fin.vcons_inj {n : ℕ} {α : Sort u} (a b : α) (v w : Fin n → α) : a ::ᵛ v = b ::ᵛ w ↔ a = b ∧ v = w

@[simp]

theorem Fin.vcons_fin_zero {α : Sort u} (a : α) (v : Fin 0 → α) : a ::ᵛ v = fun (i : Fin (0 + 1)) => match i with | 0 => a

theorem Fin.vcons_eq_const {n : ℕ} {α : Sort u} (a : α) : (a ::ᵛ fun (x : Fin n) => a) = fun (x : Fin (n + 1)) => a

theorem Fin.range_vcons {n : ℕ} {α : Type u_1} (a : α) (v : Fin n → α) : Set.range (a ::ᵛ v) = insert a (Set.range v)

@[simp]

theorem Fin.dconcat_zero {motive : Fin 1 → Sort u} (a : motive (last 0)) : !h[] :+ᵈ a = a ::ᵈ !h[]

@[simp]

theorem Fin.vconcat_zero {α : Sort u} (a : α) : !v[] :+ᵛ a = !v[a]

@[simp]

theorem Fin.dconcat_last {n : ℕ} {motive : Fin (n + 1) → Sort u} (v : (i : Fin n) → motive i.castSucc) (a : motive (last n)) : (v :+ᵈ a) (last n) = a

@[simp]

theorem Fin.vconcat_last {n : ℕ} {α : Sort u} (v : Fin n → α) (a : α) : (v :+ᵛ a) (last n) = a

@[simp]

theorem Fin.dconcat_castSucc {n : ℕ} {motive : Fin (n + 1) → Sort u} (v : (i : Fin n) → motive i.castSucc) (a : motive (last n)) (i : Fin n) : (v :+ᵈ a) i.castSucc = v i

@[simp]

theorem Fin.vconcat_castSucc {n : ℕ} {α : Sort u} (v : Fin n → α) (a : α) (i : Fin n) : (v :+ᵛ a) i.castSucc = v i

@[csimp]

theorem Fin.dconcat_eq_snoc : @dconcat = @snoc

dconcat is equal to snoc. Marked as csimp to allow for switching to the snoc implementation during execution.

theorem Fin.vconcat_eq_snoc {n : ℕ} {α : Sort u} (v : Fin n → α) (a : α) : v :+ᵛ a = snoc v a

theorem Fin.dconcat_dcons_eq_dcons_dconcat {n : ℕ} {motive : Fin (n + 2) → Sort u} (a : motive 0) (v : (i : Fin n) → motive i.castSucc.succ) (b : motive (last (n + 1))) : (fun (i : Fin (n + 1)) => (a ::ᵈ v) i) :+ᵈ b = a ::ᵈ fun (i : Fin (n + 1)) => (v :+ᵈ b) i

theorem Fin.vconcat_vcons_eq_vcons_vconcat {n : ℕ} {α : Sort u} (a : α) (v : Fin n → α) (b : α) : a ::ᵛ v :+ᵛ b = a ::ᵛ (v :+ᵛ b)

theorem Fin.init_dconcat {n : ℕ} {motive : Fin (n + 1) → Sort u} (v : (i : Fin n) → motive i.castSucc) (a : motive (last n)) : (fun (i : Fin n) => (v :+ᵈ a) i.castSucc) = v

theorem Fin.init_vconcat {n : ℕ} {α : Sort u} (v : Fin n → α) (a : α) : (fun (i : Fin n) => (v :+ᵛ a) i.castSucc) = v

theorem Fin.dconcat_init_self {n : ℕ} {motive : Fin (n + 1) → Sort u} (v : (i : Fin (n + 1)) → motive i) : (fun (i : Fin n) => v i.castSucc) :+ᵈ v (last n) = v

theorem Fin.vconcat_init_self {n : ℕ} {α : Sort u} (v : Fin (n + 1) → α) : (fun (i : Fin n) => v i.castSucc) :+ᵛ v (last n) = v

theorem Fin.range_vconcat {n : ℕ} {α : Type u_1} (v : Fin n → α) (a : α) : Set.range (v :+ᵛ a) = insert a (Set.range v)

theorem Fin.dconcat_injective2 {n : ℕ} {motive : Fin (n + 1) → Sort u} : Function.Injective2 dconcat

theorem Fin.vconcat_injective2 {n : ℕ} {α : Sort u} : Function.Injective2 vconcat

theorem Fin.dconcat_inj {n : ℕ} {motive : Fin (n + 1) → Sort u} (v w : (i : Fin n) → motive i.castSucc) (a b : motive (last n)) : v :+ᵈ a = w :+ᵈ b ↔ v = w ∧ a = b

theorem Fin.vconcat_inj {n : ℕ} {α : Sort u} (v w : Fin n → α) (a b : α) : v :+ᵛ a = w :+ᵛ b ↔ v = w ∧ a = b

theorem Fin.dconcat_right_injective {n : ℕ} {motive : Fin (n + 1) → Sort u} (v : (i : Fin n) → motive i.castSucc) : Function.Injective (dconcat v)

theorem Fin.vconcat_right_injective {n : ℕ} {α : Sort u} (v : Fin n → α) : Function.Injective (vconcat v)

theorem Fin.dconcat_left_injective {n : ℕ} {motive : Fin (n + 1) → Sort u} (a : motive (last n)) : Function.Injective fun (v : (i : Fin n) → motive i.castSucc) => v :+ᵈ a

theorem Fin.vconcat_left_injective {α : Sort u} {n : ℕ} (a : α) : Function.Injective fun (v : Fin n → α) => v :+ᵛ a

@[simp]

theorem Fin.zero_dappend {n : ℕ} {motive : Fin (0 + n) → Sort u} {u : (i : Fin 0) → motive (castAdd n i)} (v : (i : Fin n) → motive (natAdd 0 i)) : u ++ᵈ v = fun (i : Fin (0 + n)) => cast ⋯ (v (Fin.cast ⋯ i))

@[simp]

theorem Fin.zero_vappend {n : ℕ} {α : Sort u} {u : Fin 0 → α} (v : Fin n → α) : u ++ᵛ v = v ∘ Fin.cast ⋯

@[simp]

theorem Fin.dappend_zero {m : ℕ} {motive : Fin (m + 0) → Sort u} (u : (i : Fin m) → motive (castAdd 0 i)) : u ++ᵈ !h[] = u

@[simp]

theorem Fin.vappend_zero {m : ℕ} {α : Sort u} (u : Fin m → α) {v : Fin 0 → α} : u ++ᵛ v = u

theorem Fin.dappend_succ {m n : ℕ} {motive : Fin (m + (n + 1)) → Sort u} (u : (i : Fin m) → motive (castAdd (n + 1) i)) (v : (i : Fin (n + 1)) → motive (natAdd m i)) : u ++ᵈ v = (fun (i : Fin (m + n)) => (u ++ᵈ fun (i : Fin n) => v i.castSucc) i) :+ᵈ v (last n)

theorem Fin.vappend_succ {m n : ℕ} {α : Sort u} (u : Fin m → α) (v : Fin (n + 1) → α) : u ++ᵛ v = u ++ᵛ v ∘ castSucc :+ᵛ v (last n)

@[csimp]

theorem Fin.dappend_eq_addCases : @dappend = @addCases

dappend is equal to addCases. Marked as csimp to allow for switching to the addCases implementation during execution.

@[csimp]

theorem Fin.vappend_eq_append : @vappend = @append

vappend is equal to append. Marked as csimp to allow for switching to the append implementation during execution.

@[simp]

theorem Fin.dempty_dappend {n : ℕ} {motive : Fin (0 + n) → Sort u} (v : (i : Fin n) → motive (natAdd 0 i)) : !h[] ++ᵈ v = fun (i : Fin (0 + n)) => cast ⋯ (v (Fin.cast ⋯ i))

@[simp]

theorem Fin.vempty_vappend {n : ℕ} {α : Sort u} (v : Fin n → α) : !v[] ++ᵛ v = v ∘ Fin.cast ⋯

@[simp]

theorem Fin.dappend_dempty {m : ℕ} {motive : Fin (m + 0) → Sort u} (v : (i : Fin m) → motive (castAdd 0 i)) : v ++ᵈ !h[] = v

@[simp]

theorem Fin.vappend_vempty {m : ℕ} {α : Sort u} (v : Fin m → α) : v ++ᵛ !v[] = v

theorem Fin.dappend_assoc {m n p : ℕ} {motive : Fin (m + n + p) → Sort u} (_u : (i : Fin m) → motive (castAdd p (castAdd n i))) (_v : (i : Fin n) → motive (castAdd p (natAdd m i))) (_w : (i : Fin p) → motive (natAdd (m + n) i)) : True

theorem Fin.vappend_assoc {m n : ℕ} {α : Sort u} {p : ℕ} (u : Fin m → α) (v : Fin n → α) (w : Fin p → α) : u ++ᵛ v ++ᵛ w = (u ++ᵛ (v ++ᵛ w)) ∘ Fin.cast ⋯

@[simp]

theorem Fin.dappend_left {m n : ℕ} {motive : Fin (m + n) → Sort u} (u : (i : Fin m) → motive (castAdd n i)) (v : (i : Fin n) → motive (natAdd m i)) (i : Fin m) : (u ++ᵈ v) (castAdd n i) = u i

@[simp]

theorem Fin.vappend_left {m n : ℕ} {α : Sort u} (u : Fin m → α) (v : Fin n → α) (i : Fin m) : (u ++ᵛ v) (castAdd n i) = u i

@[simp]

theorem Fin.dappend_right {m n : ℕ} {motive : Fin (m + n) → Sort u} (u : (i : Fin m) → motive (castAdd n i)) (v : (i : Fin n) → motive (natAdd m i)) (i : Fin n) : (u ++ᵈ v) (natAdd m i) = v i

@[simp]

theorem Fin.vappend_right {m n : ℕ} {α : Sort u} (u : Fin m → α) (v : Fin n → α) (i : Fin n) : (u ++ᵛ v) (natAdd m i) = v i

theorem Fin.dappend_left_of_lt {m n : ℕ} {motive : Fin (m + n) → Sort u} (u : (i : Fin m) → motive (castAdd n i)) (v : (i : Fin n) → motive (natAdd m i)) (i : Fin (m + n)) (h : ↑i < m) : (u ++ᵈ v) i = cast ⋯ (u ⟨↑i, h⟩)

theorem Fin.vappend_left_of_lt {m n : ℕ} {α : Sort u} (u : Fin m → α) (v : Fin n → α) (i : Fin (m + n)) (h : ↑i < m) : (u ++ᵛ v) i = u ⟨↑i, h⟩

theorem Fin.dappend_right_of_not_lt {m n : ℕ} {motive : Fin (m + n) → Sort u} (u : (i : Fin m) → motive (castAdd n i)) (v : (i : Fin n) → motive (natAdd m i)) (i : Fin (m + n)) (h : ¬↑i < m) : (u ++ᵈ v) i = dcast ⋯ (v ⟨↑i - m, ⋯⟩)

theorem Fin.vappend_right_of_not_lt {m n : ℕ} {α : Sort u} (u : Fin m → α) (v : Fin n → α) (i : Fin (m + n)) (h : ¬↑i < m) : (u ++ᵛ v) i = v ⟨↑i - m, ⋯⟩

@[simp]

theorem Fin.vappend_vcons {m n : ℕ} {α : Sort u} (a : α) (u : Fin m → α) (v : Fin n → α) : a ::ᵛ u ++ᵛ v = (a ::ᵛ (u ++ᵛ v)) ∘ Fin.cast ⋯

theorem Fin.vappend_vconcat {m n : ℕ} {α : Sort u} (u : Fin m → α) (v : Fin n → α) (a : α) : u ++ᵛ (v :+ᵛ a) = u ++ᵛ v :+ᵛ a

theorem Fin.vappend_left_eq_cons {n : ℕ} {α : Sort u} (a : Fin 1 → α) (v : Fin n → α) : a ++ᵛ v = (a 0 ::ᵛ v) ∘ Fin.cast ⋯

theorem Fin.vappend_right_eq_snoc {m : ℕ} {α : Sort u} (u : Fin m → α) (a : Fin 1 → α) : u ++ᵛ a = u :+ᵛ a 0

theorem Fin.vappend_zero_of_succ_left {m n : ℕ} {α : Sort u} {u : Fin (m + 1) → α} {v : Fin n → α} : (u ++ᵛ v) 0 = u 0

@[simp]

theorem Fin.vappend_last_of_succ_right {m n : ℕ} {α : Sort u} {u : Fin m → α} {v : Fin (n + 1) → α} : (u ++ᵛ v) (last (m + n)) = v (last n)

theorem Fin.range_vappend {m n : ℕ} {α : Type u_1} (u : Fin m → α) (v : Fin n → α) : Set.range (u ++ᵛ v) = Set.range u ∪ Set.range v

theorem Fin.vappend_ext {m n : ℕ} {α : Sort u} (u₁ u₂ : Fin m → α) (v₁ v₂ : Fin n → α) : u₁ ++ᵛ v₁ = u₂ ++ᵛ v₂ ↔ u₁ = u₂ ∧ v₁ = v₂

theorem Fin.ext_vcons {n : ℕ} {α : Sort u} (a b : α) (v w : Fin n → α) : a ::ᵛ v = b ::ᵛ w ↔ a = b ∧ v = w

theorem Fin.vcons_eq_vcons_iff {n : ℕ} {α : Sort u} (a b : α) (v w : Fin n → α) : a ::ᵛ v = b ::ᵛ w ↔ a = b ∧ v = w

theorem Fin.vext_iff {n : ℕ} {α : Sort u} {v w : Fin n → α} : v = w ↔ ∀ (i : Fin n), v i = w i

theorem Fin.vcons_vappend_comm {m n : ℕ} {α : Sort u} (a : α) (u : Fin m → α) (v : Fin n → α) : a ::ᵛ (u ++ᵛ v) = (a ::ᵛ u ++ᵛ v) ∘ Fin.cast ⋯

theorem Fin.vappend_singleton {m : ℕ} {α : Sort u} (u : Fin m → α) (a : α) : u ++ᵛ !v[a] = u :+ᵛ a

theorem Fin.singleton_append {n : ℕ} {α : Sort u} (a : α) (v : Fin n → α) : !v[a] ++ᵛ v = (a ::ᵛ v) ∘ Fin.cast ⋯

theorem Fin.empty_unique {α : Sort u} (v : Fin 0 → α) : v = !v[]

Lemmas for functorial vectors (binary first, then unary)

@[simp]

theorem Fin.fcons₂_zero {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin n → A} {β₂ : Fin n → B} (a : F₂ α₁ α₂) (b : (i : Fin n) → F₂ (β₁ i) (β₂ i)) : fcons₂ a b 0 = cast ⋯ a

@[simp]

theorem Fin.fcons₂_succ {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin n → A} {β₂ : Fin n → B} (a : F₂ α₁ α₂) (b : (i : Fin n) → F₂ (β₁ i) (β₂ i)) (i : Fin n) : fcons₂ a b i.succ = cast ⋯ (b i)

@[simp]

theorem Fin.fcons₂_one {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin (n + 1) → A} {β₂ : Fin (n + 1) → B} (a : F₂ α₁ α₂) (b : (i : Fin (n + 1)) → F₂ (β₁ i) (β₂ i)) : fcons₂ a b 1 = b 0

theorem Fin.fcons₂_right_injective {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin n → A} {β₂ : Fin n → B} (a : F₂ α₁ α₂) : Function.Injective (fcons₂ a)

theorem Fin.fcons₂_left_injective {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin n → A} {β₂ : Fin n → B} (b : (i : Fin n) → F₂ (β₁ i) (β₂ i)) : Function.Injective fun (a : F₂ α₁ α₂) => fcons₂ a b

theorem Fin.fcons₂_injective2 {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin n → A} {β₂ : Fin n → B} : Function.Injective2 fcons₂

theorem Fin.fcons₂_inj {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : A} {α₂ : B} {β₁ : Fin n → A} {β₂ : Fin n → B} (a₁ a₂ : F₂ α₁ α₂) (b₁ b₂ : (i : Fin n) → F₂ (β₁ i) (β₂ i)) : fcons₂ a₁ b₁ = fcons₂ a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

@[simp]

theorem Fin.fconcat₂_castSucc {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B} (v : (i : Fin n) → F₂ (α₁ i) (α₂ i)) (a : F₂ β₁ β₂) (i : Fin n) : fconcat₂ v a i.castSucc = cast ⋯ (v i)

@[simp]

theorem Fin.fconcat₂_last {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B} (v : (i : Fin n) → F₂ (α₁ i) (α₂ i)) (a : F₂ β₁ β₂) : fconcat₂ v a (last n) = cast ⋯ a

theorem Fin.fconcat₂_injective2 {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B} : Function.Injective2 fconcat₂

theorem Fin.fconcat₂_inj {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B} (v₁ v₂ : (i : Fin n) → F₂ (α₁ i) (α₂ i)) (a₁ a₂ : F₂ β₁ β₂) : fconcat₂ v₁ a₁ = fconcat₂ v₂ a₂ ↔ v₁ = v₂ ∧ a₁ = a₂

theorem Fin.fconcat₂_right_injective {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B} (v : (i : Fin n) → F₂ (α₁ i) (α₂ i)) : Function.Injective (fconcat₂ v)

theorem Fin.fconcat₂_left_injective {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {n : ℕ} {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B} (a : F₂ β₁ β₂) : Function.Injective fun (v : (i : Fin n) → F₂ (α₁ i) (α₂ i)) => fconcat₂ v a

@[simp]

theorem Fin.fappend₂_zero {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {m : ℕ} {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin 0 → A} {β₂ : Fin 0 → B} (u : (i : Fin m) → F₂ (α₁ i) (α₂ i)) : fappend₂ u !h[] = u

@[simp]

theorem Fin.fappend₂_succ {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {m n : ℕ} {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin (n + 1) → A} {β₂ : Fin (n + 1) → B} (u : (i : Fin m) → F₂ (α₁ i) (α₂ i)) (v : (i : Fin (n + 1)) → F₂ (β₁ i) (β₂ i)) : fappend₂ u v = fconcat₂ (fappend₂ u fun (i : Fin n) => v i.castSucc) (v (last n))

@[simp]

theorem Fin.fappend₂_left {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {m n : ℕ} {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin n → A} {β₂ : Fin n → B} (u : (i : Fin m) → F₂ (α₁ i) (α₂ i)) (v : (i : Fin n) → F₂ (β₁ i) (β₂ i)) (i : Fin m) : fappend₂ u v (castAdd n i) = cast ⋯ (u i)

@[simp]

theorem Fin.fappend₂_right {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {m n : ℕ} {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin n → A} {β₂ : Fin n → B} (u : (i : Fin m) → F₂ (α₁ i) (α₂ i)) (v : (i : Fin n) → F₂ (β₁ i) (β₂ i)) (i : Fin n) : fappend₂ u v (natAdd m i) = cast ⋯ (v i)

theorem Fin.fappend₂_ext {A : Sort u} {B : Sort v} {F₂ : A → B → Sort w} {m n : ℕ} {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin n → A} {β₂ : Fin n → B} (u₁ u₂ : (i : Fin m) → F₂ (α₁ i) (α₂ i)) (v₁ v₂ : (i : Fin n) → F₂ (β₁ i) (β₂ i)) : fappend₂ u₁ v₁ = fappend₂ u₂ v₂ ↔ u₁ = u₂ ∧ v₁ = v₂

@[simp]

theorem Fin.fcons_zero {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} (a : F α) (b : (i : Fin n) → F (β i)) : fcons a b 0 = cast ⋯ a

@[simp]

theorem Fin.fcons_succ {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} (a : F α) (v : (i : Fin n) → F (β i)) (i : Fin n) : fcons a v i.succ = cast ⋯ (v i)

@[simp]

theorem Fin.fcons_one {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin (n + 1) → A} (a : F α) (v : (i : Fin (n + 1)) → F (β i)) : fcons a v 1 = v 0

theorem Fin.fcons_right_injective {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} (a : F α) : Function.Injective (fcons a)

theorem Fin.fcons_left_injective {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} (b : (i : Fin n) → F (β i)) : Function.Injective fun (a : F α) => fcons a b

theorem Fin.fcons_injective2 {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} : Function.Injective2 fcons

theorem Fin.fcons_inj {A : Sort u} {F : A → Sort v} {n : ℕ} {α : A} {β : Fin n → A} (a₁ a₂ : F α) (b₁ b₂ : (i : Fin n) → F (β i)) : fcons a₁ b₁ = fcons a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

@[simp]

theorem Fin.fconcat_zero {A : Sort u} {F : A → Sort v} {α : Fin 0 → A} {β : A} (a : F β) : !h[] :+ʰ a = fun (i : Fin (0 + 1)) => match i with | 0 => a

@[simp]

theorem Fin.fconcat_castSucc {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} (v : (i : Fin n) → F (α i)) (b : F β) (i : Fin n) : fconcat v b i.castSucc = cast ⋯ (v i)

@[simp]

theorem Fin.fconcat_last {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} (v : (i : Fin n) → F (α i)) (b : F β) : fconcat v b (last n) = cast ⋯ b

theorem Fin.fconcat_injective2 {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} : Function.Injective2 fconcat

theorem Fin.fconcat_inj {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} (v₁ v₂ : (i : Fin n) → F (α i)) (a₁ a₂ : F β) : fconcat v₁ a₁ = fconcat v₂ a₂ ↔ v₁ = v₂ ∧ a₁ = a₂

theorem Fin.fconcat_right_injective {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} (v : (i : Fin n) → F (α i)) : Function.Injective (fconcat v)

theorem Fin.fconcat_left_injective {A : Sort u} {F : A → Sort v} {n : ℕ} {α : Fin n → A} {β : A} (a : F β) : Function.Injective fun (v : (i : Fin n) → F (α i)) => fconcat v a

Functorial append (unary F) lemmas

@[simp]

theorem Fin.fappend_zero {A : Sort u} {F : A → Sort v} {m : ℕ} {β : Fin m → A} {α : Fin 0 → A} (u : (i : Fin m) → F (β i)) : fappend u !h[] = u

@[simp]

theorem Fin.fappend_succ {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin (n + 1) → A} (u : (i : Fin m) → F (α i)) (v : (i : Fin (n + 1)) → F (β i)) : fappend u v = fconcat (fappend u fun (i : Fin n) => v i.castSucc) (v (last n))

@[simp]

theorem Fin.fappend_left {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin n → A} (u : (i : Fin m) → F (α i)) (v : (i : Fin n) → F (β i)) (i : Fin m) : fappend u v (castAdd n i) = cast ⋯ (u i)

@[simp]

theorem Fin.fappend_right {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin n → A} (u : (i : Fin m) → F (α i)) (v : (i : Fin n) → F (β i)) (i : Fin n) : fappend u v (natAdd m i) = cast ⋯ (v i)

theorem Fin.fappend_ext {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin n → A} (u₁ u₂ : (i : Fin m) → F (α i)) (v₁ v₂ : (i : Fin n) → F (β i)) : fappend u₁ v₁ = fappend u₂ v₂ ↔ u₁ = u₂ ∧ v₁ = v₂

Lemmas for heterogeneous vectors

@[simp]

theorem Fin.hcons_zero {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a : α) (b : (i : Fin n) → β i) : (a ::ʰ b) 0 = cast ⋯ a

@[simp]

theorem Fin.hcons_succ {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a : α) (v : (i : Fin n) → β i) (i : Fin n) : (a ::ʰ v) i.succ = cast ⋯ (v i)

@[simp]

theorem Fin.hcons_one {n : ℕ} {α : Sort u} {β : Fin (n + 1) → Sort u} (a : α) (v : (i : Fin (n + 1)) → β i) : (a ::ʰ v) 1 = cast ⋯ (v 0)

theorem Fin.hcons_eq_cons {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a : α) (v : (i : Fin n) → β i) : a ::ʰ v = cons ((a ::ʰ v) 0) fun (i : Fin n) => (a ::ʰ v) i.succ

@[simp]

theorem Fin.hconcat_zero {α : Fin 0 → Sort u} {β : Sort u} (a : β) : !h[] :+ʰ a = fun (i : Fin (0 + 1)) => match i with | 0 => a

@[simp]

theorem Fin.hconcat_castSucc {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (v : (i : Fin n) → α i) (b : β) (i : Fin n) : (v :+ʰ b) i.castSucc = cast ⋯ (v i)

@[simp]

theorem Fin.hconcat_last {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (v : (i : Fin n) → α i) (b : β) : (v :+ʰ b) (last n) = cast ⋯ b

theorem Fin.hconcat_eq_snoc {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (v : (i : Fin n) → α i) (b : β) : v :+ʰ b = snoc (fun (i : Fin n) => cast ⋯ (v i)) (cast ⋯ b)

theorem Fin.hcons_right_injective {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a : α) : Function.Injective (hcons a)

theorem Fin.hcons_left_injective {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (b : (i : Fin n) → β i) : Function.Injective fun (a : α) => a ::ʰ b

theorem Fin.hcons_injective2 {n : ℕ} {α : Sort u} {β : Fin n → Sort u} : Function.Injective2 hcons

theorem Fin.hcons_inj {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a₁ a₂ : α) (b₁ b₂ : (i : Fin n) → β i) : a₁ ::ʰ b₁ = a₂ ::ʰ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

@[simp]

theorem Fin.hcons_fin_zero {α : Sort u} {β : Fin 0 → Sort u} (a : α) (v : (i : Fin 0) → β i) : a ::ʰ v = fun (i : Fin (0 + 1)) => match i with | 0 => a

theorem Fin.hconcat_hcons {n : ℕ} {α : Sort u} {β : Fin n → Sort u} {γ : Sort u} (_a : α) (_v : (i : Fin n) → β i) (_c : γ) : True

theorem Fin.dinit_hconcat {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (_v : (i : Fin n) → α i) (_b : β) : True

theorem Fin.hconcat_init_self {n : ℕ} {α : Fin n.succ → Sort u} (_v : (i : Fin (n + 1)) → α i) : True

theorem Fin.hconcat_injective2 {n : ℕ} {α : Fin n → Sort u} {β : Sort u} : Function.Injective2 hconcat

theorem Fin.hconcat_inj {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (v₁ v₂ : (i : Fin n) → α i) (a₁ a₂ : β) : v₁ :+ʰ a₁ = v₂ :+ʰ a₂ ↔ v₁ = v₂ ∧ a₁ = a₂

theorem Fin.hconcat_right_injective {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (v : (i : Fin n) → α i) : Function.Injective (hconcat v)

theorem Fin.hconcat_left_injective {n : ℕ} {α : Fin n → Sort u} {β : Sort u} (a : β) : Function.Injective fun (v : (i : Fin n) → α i) => v :+ʰ a

@[simp]

theorem Fin.happend_zero {m : ℕ} {β : Fin m → Sort u} {α : Fin 0 → Sort u} (u : (i : Fin m) → β i) : u ++ʰ !h[] = u

@[simp]

theorem Fin.happend_empty {m : ℕ} {α : Fin m → Sort u} {β : Fin 0 → Sort u} (v : (i : Fin m) → α i) : v ++ʰ !h[] = v

@[simp]

theorem Fin.happend_succ {m n : ℕ} {α : Fin m → Sort u} {β : Fin (n + 1) → Sort u} (u : (i : Fin m) → α i) (v : (i : Fin (n + 1)) → β i) : u ++ʰ v = (u ++ʰ fun (i : Fin n) => v i.castSucc) :+ʰ v (last n)

@[simp]

theorem Fin.dempty_happend {n : ℕ} {α : Fin 0 → Sort u} {β : Fin n → Sort u} (v : (i : Fin n) → β i) : !h[] ++ʰ v = fun (i : Fin (0 + n)) => cast ⋯ (v (Fin.cast ⋯ i))

@[simp]

theorem Fin.happend_left {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) (i : Fin m) : (u ++ʰ v) (castAdd n i) = cast ⋯ (u i)

@[simp]

theorem Fin.happend_right {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) (i : Fin n) : (u ++ʰ v) (natAdd m i) = cast ⋯ (v i)

theorem Fin.happend_eq_addCases {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) : u ++ʰ v = addCases (fun (i : Fin m) => cast ⋯ (u i)) fun (i : Fin n) => cast ⋯ (v i)

theorem Fin.happend_assoc {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} {p : ℕ} {γ : Fin p → Sort u} (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) (w : (i : Fin p) → γ i) : u ++ʰ v ++ʰ w = fun (i : Fin (m + n + p)) => cast ⋯ ((u ++ʰ (v ++ʰ w)) (Fin.cast ⋯ i))

theorem Fin.happend_hcons {m n : ℕ} {α : Sort u} {β : Fin m → Sort u} {γ : Fin n → Sort u} (_a : α) (_u : (i : Fin m) → β i) (_v : (i : Fin n) → γ i) : True

theorem Fin.happend_hconcat {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} {γ : Sort u} (_u : (i : Fin m) → α i) (_v : (i : Fin n) → β i) (_c : γ) : True

theorem Fin.happend_left_eq_hcons {n : ℕ} {α : Fin 1 → Sort u} {β : Fin n → Sort u} (_a : (i : Fin 1) → α i) (_v : (i : Fin n) → β i) : True

theorem Fin.happend_right_eq_hconcat {m : ℕ} {α : Fin m → Sort u} {β : Fin 1 → Sort u} (u : (i : Fin m) → α i) (a : (i : Fin 1) → β i) : u ++ʰ a = u :+ʰ a 0

theorem Fin.happend_ext {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (u₁ u₂ : (i : Fin m) → α i) (v₁ v₂ : (i : Fin n) → β i) : u₁ ++ʰ v₁ = u₂ ++ʰ v₂ ↔ u₁ = u₂ ∧ v₁ = v₂

theorem Fin.ext_hcons {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a₁ a₂ : α) (v₁ v₂ : (i : Fin n) → β i) : a₁ ::ʰ v₁ = a₂ ::ʰ v₂ ↔ a₁ = a₂ ∧ v₁ = v₂

theorem Fin.hcons_eq_hcons_iff {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (a₁ a₂ : α) (v₁ v₂ : (i : Fin n) → β i) : a₁ ::ʰ v₁ = a₂ ::ʰ v₂ ↔ a₁ = a₂ ∧ v₁ = v₂

theorem Fin.dext_iff {n : ℕ} {α : Fin n → Sort u} {v w : (i : Fin n) → α i} : v = w ↔ ∀ (i : Fin n), v i = w i

theorem Fin.hcons_happend_comm {m n : ℕ} {α : Sort u} {β : Fin m → Sort u} {γ : Fin n → Sort u} (_a : α) (_u : (i : Fin m) → β i) (_v : (i : Fin n) → γ i) : True

theorem Fin.happend_singleton {m : ℕ} {α : Fin m → Sort u} {β : Sort u} (_u : (i : Fin m) → α i) (_a : β) : True

theorem Fin.singleton_happend {n : ℕ} {α : Sort u} {β : Fin n → Sort u} (_a : α) (_v : (i : Fin n) → β i) : True

@[implicit_reducible]

instance Fin.instUniqueForall_starlib_1 {α : Fin 0 → Sort u} : Unique ((i : Fin 0) → α i)

@[simp]

theorem Fin.rightpad_apply_lt {m : ℕ} {α : Sort u} (n : ℕ) (a : α) (v : Fin m → α) (i : Fin n) (h : ↑i < m) : rightpad n a v i = v ⟨↑i, h⟩

@[simp]

theorem Fin.rightpad_apply_ge {m : ℕ} {α : Sort u} (n : ℕ) (a : α) (v : Fin m → α) (i : Fin n) (h : m ≤ ↑i) : rightpad n a v i = a

@[simp]

theorem Fin.leftpad_apply_lt {m : ℕ} {α : Sort u} (n : ℕ) (a : α) (v : Fin m → α) (i : Fin n) (h : ↑i < n - m) : leftpad n a v i = a

@[simp]

theorem Fin.leftpad_apply_ge {m : ℕ} {α : Sort u} (n : ℕ) (a : α) (v : Fin m → α) (i : Fin n) (h : n - m ≤ ↑i) : leftpad n a v i = v ⟨↑i - (n - m), ⋯⟩

theorem Fin.rightpad_eq_self {n : ℕ} {α : Sort u} (v : Fin n → α) (a : α) : rightpad n a v = v

theorem Fin.leftpad_eq_self {n : ℕ} {α : Sort u} (v : Fin n → α) (a : α) : leftpad n a v = v