Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2022 Eric Rodriguez. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Rodriguez

! This file was ported from Lean 3 source module data.fin.succ_pred
! leanprover-community/mathlib commit 7c523cb78f4153682c2929e3006c863bfef463d0
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fin.Basic
import Mathlib.Order.SuccPred.Basic

/-!
# Successors and predecessors of `Fin n`

In this file, we show that `Fin n` is both a `SuccOrder` and a `PredOrder`. Note that they are
also archimedean, but this is derived from the general instance for well-orderings as opposed
to a specific `Fin` instance.

-/


namespace Fin

instance: {n : ℕ} → SuccOrder (Fin n)
instance
: ∀ {n :
ℕ: Type
ℕ
},
SuccOrder: (α : Type ?u.5) → [inst : Preorder α] → Type ?u.5
SuccOrder
(
Fin: ℕ → Type
Fin
n) | 0 =>

Goals accomplished! 🐙

le_succ
∀ (a : Fin 0), a ≤ ?succ a

max_of_succ_le
∀ {a : Fin 0}, ?succ a ≤ a → IsMax a

succ_le_of_lt
∀ {a b : Fin 0}, a < b → ?succ a ≤ b

le_of_lt_succ
∀ {a b : Fin 0}, a < ?succ b → a ≤ b

succ
Fin 0 → Fin 0

le_succ
∀ (a : Fin 0), a ≤ ?succ a

max_of_succ_le
∀ {a : Fin 0}, ?succ a ≤ a → IsMax a

succ_le_of_lt
∀ {a b : Fin 0}, a < b → ?succ a ≤ b

le_of_lt_succ
∀ {a b : Fin 0}, a < ?succ b → a ≤ b

succ
Fin 0 → Fin 0

succ
Fin 0 → Fin 0

le_succ
∀ (a : Fin 0), a ≤ ?succ a

succ
Fin 0 → Fin 0
a: Fin 0


succ_le_of_lt
∀ {b : Fin 0}, a < b → ?succ a ≤ b
a: Fin 0


le_of_lt_succ
∀ {b : Fin 0}, a < ?succ b → a ≤ b

succ_le_of_lt
∀ {a b : Fin 0}, a < b → ?succ a ≤ b

Goals accomplished! 🐙
| n + 1 =>
SuccOrder.ofCore: {α : Type ?u.131} → [inst : LinearOrder α] → (succ : α → α) → (∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b) → (∀ (a : α), IsMax a → succ a = a) → SuccOrder α
SuccOrder.ofCore
(fun
i: ?m.180
i
=> if
i: ?m.180
i
<
Fin.last: (n : ℕ) → Fin (n + 1)
Fin.last
n then
i: ?m.180
i
+
1: ?m.212
1
else
i: ?m.180
i
) (

Goals accomplished! 🐙

∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha: ¬IsMax a

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b

∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha: ¬IsMax a

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: ¬a = ⊤

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha: ¬IsMax a

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: ¬⊤ ≤ a

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha: ¬IsMax a

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < ⊤

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha: ¬IsMax a

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b

∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (if a < last n then a + 1 else a) ≤ b

∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (if a < last n then a + 1 else a) ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ a + 1 ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (if a < last n then a + 1 else a) ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


↑a < ↑b ↔ a + 1 ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (if a < last n then a + 1 else a) ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


↑a < ↑b ↔ ↑(a + 1) ≤ ↑b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


a < b ↔ (if a < last n then a + 1 else a) ≤ b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


↑a < ↑b ↔ ↑a + 1 ≤ ↑b
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMax a

ha: a < last n

b: Fin (n + 1)


↑a < ↑b ↔ ↑a + 1 ≤ ↑b

∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b

Goals accomplished! 🐙
) (

Goals accomplished! 🐙

∀ (a : Fin (n + 1)), IsMax a → (fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha: IsMax a


(fun i => if i < last n then i + 1 else i) a = a

∀ (a : Fin (n + 1)), IsMax a → (fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha: IsMax a


(fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = ⊤


(fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha: IsMax a


(fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = last n


(fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = last n


(fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = last n


(fun i => if i < last n then i + 1 else i) a = a

∀ (a : Fin (n + 1)), IsMax a → (fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = last n


(if a < last n then a + 1 else a) = a

∀ (a : Fin (n + 1)), IsMax a → (fun i => if i < last n then i + 1 else i) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = last n


(if a < last n then a + 1 else a) = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMax a

ha: a = last n


a = a

Goals accomplished! 🐙
) @[simp] theorem
succ_eq: ∀ {n : ℕ}, SuccOrder.succ = fun a => if a < last n then a + 1 else a
succ_eq
{n :
ℕ: Type
ℕ
} :
SuccOrder.succ: {α : Type ?u.1739} → [inst : Preorder α] → [self : SuccOrder α] → α → α
SuccOrder.succ
= fun
a: ?m.1804
a
=> if
a: ?m.1804
a
<
Fin.last: (n : ℕ) → Fin (n + 1)
Fin.last
n then
a: ?m.1804
a
+
1: ?m.1823
1
else
a: ?m.1804
a
:=
rfl: ∀ {α : Sort ?u.2074} {a : α}, a = a
rfl
#align fin.succ_eq
Fin.succ_eq: ∀ {n : ℕ}, SuccOrder.succ = fun a => if a < last n then a + 1 else a
Fin.succ_eq
@[simp] theorem
succ_apply: ∀ {n : ℕ} (a : Fin (n + 1)), SuccOrder.succ a = if a < last n then a + 1 else a
succ_apply
{n :
ℕ: Type
ℕ
} (
a: ?m.2137
a
) :
SuccOrder.succ: {α : Type ?u.2141} → [inst : Preorder α] → [self : SuccOrder α] → α → α
SuccOrder.succ
a: ?m.2137
a
= if
a: ?m.2137
a
<
Fin.last: (n : ℕ) → Fin (n + 1)
Fin.last
n then
a: ?m.2137
a
+
1: ?m.2221
1
else
a: ?m.2137
a
:=
rfl: ∀ {α : Sort ?u.2355} {a : α}, a = a
rfl
#align fin.succ_apply
Fin.succ_apply: ∀ {n : ℕ} (a : Fin (n + 1)), SuccOrder.succ a = if a < last n then a + 1 else a
Fin.succ_apply
instance: {n : ℕ} → PredOrder (Fin n)
instance
: ∀ {n :
ℕ: Type
ℕ
},
PredOrder: (α : Type ?u.2418) → [inst : Preorder α] → Type ?u.2418
PredOrder
(
Fin: ℕ → Type
Fin
n) | 0 =>

Goals accomplished! 🐙

pred_le
∀ (a : Fin 0), ?pred a ≤ a

min_of_le_pred
∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

le_pred_of_lt
∀ {a b : Fin 0}, a < b → a ≤ ?pred b

le_of_pred_lt
∀ {a b : Fin 0}, ?pred a < b → a ≤ b

pred
Fin 0 → Fin 0

pred_le
∀ (a : Fin 0), ?pred a ≤ a

min_of_le_pred
∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

le_pred_of_lt
∀ {a b : Fin 0}, a < b → a ≤ ?pred b

le_of_pred_lt
∀ {a b : Fin 0}, ?pred a < b → a ≤ b

pred
Fin 0 → Fin 0

le_of_pred_lt
∀ {a b : Fin 0}, ?pred a < b → a ≤ b

pred
Fin 0 → Fin 0

le_of_pred_lt
∀ {a b : Fin 0}, ?pred a < b → a ≤ b
a: Fin 0


pred
Fin 0
a: Fin 0


le_pred_of_lt
∀ {b : Fin 0}, a < b → a ≤ ?pred b

min_of_le_pred
∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

Goals accomplished! 🐙
| n + 1 =>
PredOrder.ofCore: {α : Type ?u.2544} → [inst : LinearOrder α] → (pred : α → α) → (∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a) → (∀ (a : α), IsMin a → pred a = a) → PredOrder α
PredOrder.ofCore
(fun
x: ?m.2593
x
=> if
x: ?m.2593
x
=
0: ?m.2597
0
then
0: ?m.2651
0
else
x: ?m.2593
x
-
1: ?m.2657
1
) (

Goals accomplished! 🐙

∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha: ¬IsMin a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a

∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha: ¬IsMin a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: ¬a = ⊥

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha: ¬IsMin a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: ¬a ≤ ⊥

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha: ¬IsMin a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: ⊥ < a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha: ¬IsMin a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a

∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a

∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


b ≤ a - 1 ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


b ≤ a - 1 ↔ ↑b < ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


↑b ≤ ↑(a - 1) ↔ ↑b < ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(↑b ≤ if a = 0 then n else ↑a - 1) ↔ ↑b < ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


↑b ≤ ↑a - 1 ↔ ↑b < ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


↑b + 1 ≤ ↑a ↔ ↑b < ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


1 ≤ ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


(b ≤ if a = 0 then 0 else a - 1) ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


↑b < ↑a ↔ ↑b + 1 ≤ ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


1 ≤ ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


↑b < ↑a ↔ ↑b + 1 ≤ ↑a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


1 ≤ ↑a

∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
n: ℕ

a: Fin (n + 1)

ha✝: ¬IsMin a

ha: 0 < a

b: Fin (n + 1)


1 ≤ ↑a

∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a

Goals accomplished! 🐙
) (

Goals accomplished! 🐙

∀ (a : Fin (n + 1)), IsMin a → (fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha: IsMin a


(fun x => if x = 0 then 0 else x - 1) a = a

∀ (a : Fin (n + 1)), IsMin a → (fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha: IsMin a


(fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = ⊥


(fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha: IsMin a


(fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


(fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


(fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


(fun x => if x = 0 then 0 else x - 1) a = a

∀ (a : Fin (n + 1)), IsMin a → (fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


(if a = 0 then 0 else a - 1) = a

∀ (a : Fin (n + 1)), IsMin a → (fun x => if x = 0 then 0 else x - 1) a = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


(if a = 0 then 0 else a - 1) = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


0 = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


(if a = 0 then 0 else a - 1) = a
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


a = 0
n: ℕ

a: Fin (n + 1)

ha✝: IsMin a

ha: a = 0


a = 0
) @[simp] theorem
pred_eq: ∀ {n : ℕ}, PredOrder.pred = fun a => if a = 0 then 0 else a - 1
pred_eq
{
n: ?m.4802
n
} :
PredOrder.pred: {α : Type ?u.4806} → [inst : Preorder α] → [self : PredOrder α] → α → α
PredOrder.pred
= fun
a: Fin (n + 1)
a
:
Fin: ℕ → Type
Fin
(
n: ?m.4802
n
+
1: ?m.4875
1
) => if
a: Fin (n + 1)
a
=
0: ?m.4958
0
then
0: ?m.5028
0
else
a: Fin (n + 1)
a
-
1: ?m.5042
1
:=
rfl: ∀ {α : Sort ?u.5331} {a : α}, a = a
rfl
#align fin.pred_eq
Fin.pred_eq: ∀ {n : ℕ}, PredOrder.pred = fun a => if a = 0 then 0 else a - 1
Fin.pred_eq
@[simp] theorem
pred_apply: ∀ {n : ℕ} (a : Fin (n + 1)), PredOrder.pred a = if a = 0 then 0 else a - 1
pred_apply
{n :
ℕ: Type
ℕ
} (
a: Fin (n + 1)
a
:
Fin: ℕ → Type
Fin
(n +
1: ?m.5387
1
)) :
PredOrder.pred: {α : Type ?u.5442} → [inst : Preorder α] → [self : PredOrder α] → α → α
PredOrder.pred
a: Fin (n + 1)
a
= if
a: Fin (n + 1)
a
=
0: ?m.5488
0
then
0: ?m.5556
0
else
a: Fin (n + 1)
a
-
1: ?m.5570
1
:=
rfl: ∀ {α : Sort ?u.5663} {a : α}, a = a
rfl
#align fin.pred_apply
Fin.pred_apply: ∀ {n : ℕ} (a : Fin (n + 1)), PredOrder.pred a = if a = 0 then 0 else a - 1
Fin.pred_apply
end Fin