Supporting results for pointwise provable equality.

theorem PointwiseComposition.eq_finZeroElim {α : Sort u} (x : Fin 0 → α) : x = finZeroElim

theorem PointwiseComposition.Nat.sub_one_lt' {n : ℕ} [NeZero n] : n - 1 < n

theorem PointwiseComposition.Fin.isEmpty_embedding_lt {n m : ℕ} (hn : n > m) : IsEmpty (Fin n ↪ Fin m)

theorem PointwiseComposition.Fin.lt_last {n : ℕ} : n < ↑(Fin.last (n + 1))

theorem PointwiseComposition.Fin.lt_sub_one_of_pos {n : ℕ} {a : Fin n} (hn : 0 < n) : a ≤ ⟨n - 1, ⋯⟩

def PointwiseComposition.Fin.last' {n : ℕ} [NeZero n] : Fin n

The last element of Fin n when n is NeZero.

Equations

• PointwiseComposition.Fin.last' = ⟨n - 1, ⋯⟩

@[simp]

theorem PointwiseComposition.Fin.lt_last' {n : ℕ} {i : Fin n} [NeZero n] : i ≤ last'

theorem PointwiseComposition.Fin.pos_of_coe_ne_zero {n : ℕ} {i : Fin (n + 1)} (h : ↑i ≠ 0) : 0 < i

theorem PointwiseComposition.Fin.one_pos'' {n : ℕ} : 0 < 1

@[simp]

theorem PointwiseComposition.Fin.two_pos {n : ℕ} : 0 < 2

@[simp]

theorem PointwiseComposition.Fin.three_pos {n : ℕ} : 0 < 3

@[simp]

theorem PointwiseComposition.Fin.four_pos {n : ℕ} : 0 < 4

@[simp]

theorem PointwiseComposition.Fin.five_pos {n : ℕ} : 0 < 5

theorem PointwiseComposition.Fin.forall_fin_iff_zero_and_forall_succ {k : ℕ} {P : Fin (k + 1) → Prop} : (∀ (i : Fin (k + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin k), P i.succ

theorem PointwiseComposition.Fin.exists_fin_iff_zero_or_exists_succ {k : ℕ} {P : Fin (k + 1) → Prop} : (∃ (i : Fin (k + 1)), P i) ↔ P 0 ∨ ∃ (i : Fin k), P i.succ

theorem PointwiseComposition.Fin.funext_two {k : ℕ} {α : Type u_1} {f g : Fin (k + 2) → α} (h0 : f 0 = g 0) (h1 : f (Fin.succ 0) = g (Fin.succ 0)) (hs : ∀ (i : Fin k), f i.succ.succ = g i.succ.succ) : f = g

@[inline]

def PointwiseComposition.Fin.addCast {n : ℕ} (m : ℕ) : Fin n → Fin (m + n)

The add Cast construction in Fin.

Equations

• PointwiseComposition.Fin.addCast m = Fin.castLE ⋯

@[simp]

theorem PointwiseComposition.Fin.addCast_val {n m : ℕ} (i : Fin n) : ↑(addCast m i) = ↑i

theorem PointwiseComposition.Fin.Fin1.eq_one {n : Fin 1} : n = 0

@[simp]

theorem PointwiseComposition.Fin.Fin1.not_lt_zero {n : Fin 1} : ¬0 < n