ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Nat<GOAL>n = 0 ∨ n = n.pred.succ
<VAR>a b : Nat<GOAL>a.succ = b.succ ↔ a = b
<VAR>a b : Nat<GOAL>a.succ ≤ b.succ ↔ a ≤ b
<VAR>a b : Nat<GOAL>a.succ < b.succ ↔ a < b
<VAR>a b : Nat<GOAL>a + 1 = b + 1 ↔ a = b
<VAR>a b : Nat<GOAL>a + 1 ≤ b + 1 ↔ a ≤ b
<VAR>a b : Nat<GOAL>a + 1 < b + 1 ↔ a < b
<VAR>a b : Nat<GOAL>0 < a → 0 < b → a.pred = b.pred → a = b
<VAR>a : Nat<GOAL>a ≠ 0 → a.pred ≠ a
<VAR>a : Nat<GOAL>a ≠ 0 → a - 1 ≠ a
<VAR>a : Nat<GOAL>0 < a → a.pred < a
<VAR>n m : Nat<GOAL>n ≠ 0 → n < m → n.pred < m.pred
<VAR>n : Nat<VAR>m : Nat<GOAL>n.pred ≤ m ↔ n ≤ m.succ
<VAR>n : Nat<VAR>m : Nat<GOAL>n.pred ≤ m → n ≤ m.succ
<VAR>n m : Nat<GOAL>n ≤ m.succ → n.pred ≤ m
<VAR>n : Nat<VAR>m : Nat<GOAL>n < m.pred ↔ n.succ < m
<VAR>n : Nat<VAR>m : Nat<GOAL>n < m.pred → n.succ < m
<VAR>n m : Nat<GOAL>n.succ < m → n < m.pred
<VAR>n : Nat<VAR>m : Nat<GOAL>0 < m → (n ≤ m.pred ↔ n < m)
<VAR>n m : Nat<VAR>h : n < m<GOAL>n ≤ m.pred
<VAR>a b : Nat<GOAL>a < b → a ≤ b - 1
<VAR>m : Nat<VAR>n : Nat<VAR>h : 0 < m<GOAL>n ≤ m.pred → n < m
<VAR>m n : Nat<VAR>h : 0 < m<GOAL>n ≤ m - 1 → n < m
<VAR>m n : Nat<VAR>h : 0 < m<GOAL>n ≤ m - 1 ↔ n < m
<VAR>n : Nat<GOAL>n ≠ 0 → Exists fun k => n = k.succ
<VAR>n : Nat<GOAL>n ≠ 0 → Exists fun k => n = k + 1
<VAR>n : Nat<GOAL>n.succ ≠ 0
<VAR>n m : Nat<VAR>k : Nat<VAR>h : n ≤ m<GOAL>k * n ≤ k * m
<VAR>n m : Nat<VAR>k : Nat<VAR>h : n ≤ m<GOAL>n * k ≤ m * k
<VAR>n₁ m₁ n₂ m₂ : Nat<VAR>h₁ : n₁ ≤ n₂<VAR>h₂ : m₁ ≤ m₂<GOAL>n₁ * m₁ ≤ n₂ * m₂
<VAR>n m k : Nat<VAR>h : n < m<VAR>hk : k > 0<GOAL>k * n < k * m
<VAR>n m k : Nat<VAR>h : n < m<VAR>hk : k > 0<GOAL>n * k < m * k
<VAR>n m : Nat<VAR>ha : n > 0<VAR>hb : m > 0<GOAL>n * m > 0
<VAR>a b c : Nat<VAR>h : c * a ≤ c * b<VAR>hc : 0 < c<GOAL>a ≤ b
<VAR>m k n : Nat<VAR>hn : 0 < n<VAR>h : n * m = n * k<GOAL>m = k
<VAR>n m k : Nat<VAR>hm : 0 < m<VAR>h : n * m = k * m<GOAL>n = k
<VAR>n m : Nat<GOAL>n ^ m.succ = n ^ m * n
<VAR>n m : Nat<GOAL>n ^ (m + 1) = n ^ m * n
<VAR>n m : Nat<GOAL>min n m = ite (n ≤ m) n m
<VAR>n m : Nat<GOAL>max n m = ite (n ≤ m) m n
<VAR>b a : Nat<VAR>h : b < a<GOAL>a ≠ 0
<VAR>n m : Nat<VAR>h : m < n<GOAL>n.pred < n
<VAR>n m : Nat<VAR>h : m < n<GOAL>n - 1 < n
<VAR>a : Nat<VAR>h : a ≠ 0<GOAL>a.pred.succ = a
<VAR>a : Nat<VAR>h : a ≠ 0<GOAL>a - 1 + 1 = a
<VAR>n : Nat<GOAL>0 < n → n.pred.succ = n
<VAR>n : Nat<GOAL>0 < n → n - 1 + 1 = n
<VAR>n : Nat<GOAL>n = 0 ∨ n = n - 1 + 1
<VAR>a i : Nat<GOAL>a - i ≤ a.succ - i
<VAR>i a : Nat<VAR>h : i < a<GOAL>0 < a - i
<VAR>a i : Nat<VAR>h : i < a<GOAL>a - (i + 1) < a - i
<VAR>a b : Nat<GOAL>a < b → b - a ≠ 0
<VAR>a b : Nat<VAR>h : a ≤ b<GOAL>a + (b - a) = b
<VAR>a b : Nat<GOAL>0 < a → 0 < b → a - 1 = b - 1 → a = b
<VAR>n m : Nat<VAR>h : m ≤ n<GOAL>n - m + m = n
<VAR>n k m : Nat<GOAL>n + k - (m + k) = n - m
<VAR>k n m : Nat<GOAL>k + n - (k + m) = n - m
<VAR>m k : Nat<VAR>h : k ≤ m<VAR>n : Nat<GOAL>n + m - k = n + (m - k)
<VAR>a b c : Nat<VAR>hle : b ≤ a<VAR>h : a - b = c<GOAL>a = c + b
<VAR>a b c : Nat<VAR>h : a = c + b<GOAL>a - b = c
<VAR>a b c : Nat<VAR>h : a - b ≤ c<GOAL>a ≤ c + b
<VAR>k m n : Nat<GOAL>k < m → k < n → m - n < m - k
<VAR>a b c : Nat<GOAL>c ≤ a → a < b → a - c < b - c
<VAR>n m : Nat<GOAL>n - (n + m) = 0
<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>n - m = 0
<VAR>a b c : Nat<VAR>h : a ≤ c + b<GOAL>a - b ≤ c
<VAR>a b c : Nat<VAR>hle : b ≤ c<VAR>h : a ≤ c - b<GOAL>a + b ≤ c
<VAR>a b c : Nat<VAR>h : a + b ≤ c<GOAL>a ≤ c - b
<VAR>a b c : Nat<VAR>h : a < c - b<GOAL>a + b < c
<VAR>a b c : Nat<VAR>h : a + b < c<GOAL>a < c - b
<VAR>motive : Nat → Prop<VAR>x y : Nat<VAR>h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k<VAR>h₂ : x < y → motive 0<GOAL>motive (x - y)
<VAR>m n : Nat<VAR>h : n ≤ m<GOAL>m.succ - n = (m - n).succ
<VAR>m n : Nat<VAR>h : m < n<GOAL>0 < n - m
<VAR>n m k : Nat<GOAL>n - m - k = n - (m + k)
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>k : Nat<GOAL>k - m ≤ k - n
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>k : Nat<GOAL>n - k ≤ m - k
<VAR>a i j : Nat<GOAL>a - i ≤ a + j - i
<VAR>n m : Nat<VAR>h : n - m ≠ 0<GOAL>m < n
<VAR>n m : Nat<GOAL>n - m ≠ 0 ↔ m < n
<VAR>n m : Nat<VAR>h : 0 < n - m<GOAL>m < n
<VAR>m n l : Nat<VAR>h : m - n = l.succ<GOAL>n < m
<VAR>m n l : Nat<VAR>h : m - n = l + 1<GOAL>n < m
<VAR>n k m : Nat<VAR>H : n ≤ k<VAR>h : k < n + m<GOAL>k - n < m
<VAR>n k m : Nat<VAR>H : n ≤ k<VAR>h : k < m + n<GOAL>k - n < m
<VAR>n m : Nat<GOAL>n - m = 0 → n ≤ m
<VAR>n m k : Nat<GOAL>k ≤ m → n - k ≤ m - k → n ≤ m
<VAR>k m n : Nat<VAR>h : k ≤ m<GOAL>n - k ≤ m - k ↔ n ≤ m
<VAR>b a c : Nat<VAR>h : b ≤ a<GOAL>a - b = c ↔ a = c + b
<VAR>b a c : Nat<VAR>h : b ≤ a<GOAL>a - b = c ↔ a = b + c
<VAR>n m : Nat<GOAL>n.pred * m = n * m - m
<VAR>n m : Nat<GOAL>(n - 1) * m = n * m - m
<VAR>n m : Nat<GOAL>n * m.pred = n * m - n
<VAR>n m : Nat<GOAL>n * (m - 1) = n * m - n
<VAR>n m k : Nat<GOAL>(n - m) * k = n * k - m * k
<VAR>n m k : Nat<GOAL>n * (m - k) = n * m - n * k
<VAR>a b : Nat<GOAL>(¬a ≤ b) = (b + 1 ≤ a)
<VAR>a b : Nat<GOAL>(¬a ≥ b) = (a + 1 ≤ b)
<VAR>a b : Nat<GOAL>(¬a < b) = (b ≤ a)
<VAR>a b : Nat<GOAL>(¬a > b) = (a ≤ b)
<VAR>α : Type u_1<VAR>f : Nat → α → α<VAR>init : α<VAR>m n : Nat<GOAL>Nat.foldTR.loop f (m + n) m (Nat.fold f n init) = Nat.fold f (m + n) init
<VAR>f : Nat → Bool<VAR>m n : Nat<GOAL>(Nat.any f n || Nat.anyTR.loop f (m + n) m) = Nat.any f (m + n)
<VAR>f : Nat → Bool<VAR>m n : Nat<GOAL>(Nat.all f n && Nat.allTR.loop f (m + n) m) = Nat.all f (m + n)
<VAR>α : Type u_1<VAR>f : α → α<VAR>init : α<VAR>m n : Nat<GOAL>Nat.repeatTR.loop f m (Nat.repeat f n init) = Nat.repeat f (m + n) init
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.SOM.Mon<GOAL>Nat.SOM.Mon.denote ctx (m₁ ++ m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>m₁ m₂ : Nat.SOM.Mon<GOAL>Nat.SOM.Mon.denote ctx (Nat.SOM.Mon.mul.go fuel m₁ m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.SOM.Mon<GOAL>Nat.SOM.Mon.denote ctx (m₁.mul m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂
<VAR>ctx : Nat.Linear.Context<VAR>p₁ p₂ : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (p₁ ++ p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>p₁ p₂ : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.add.go fuel p₁ p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>p₁ p₂ : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (p₁.add p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>m : Nat.SOM.Mon<VAR>p : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.insertSorted k m p) = Nat.SOM.Poly.denote ctx p + k * Nat.SOM.Mon.denote ctx m
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>m : Nat.SOM.Mon<VAR>p acc : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.mulMon.go k m p acc) = Nat.SOM.Poly.denote ctx acc + Nat.SOM.Poly.denote ctx p * k * Nat.SOM.Mon.denote ctx m
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.SOM.Poly<VAR>k : Nat<VAR>m : Nat.SOM.Mon<GOAL>Nat.SOM.Poly.denote ctx (p.mulMon k m) = Nat.SOM.Poly.denote ctx p * k * Nat.SOM.Mon.denote ctx m
<VAR>ctx : Nat.Linear.Context<VAR>p₂ p₁ acc : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.mul.go p₂ p₁ acc) = Nat.SOM.Poly.denote ctx acc + Nat.SOM.Poly.denote ctx p₁ * Nat.SOM.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>p₁ p₂ : Nat.SOM.Poly<GOAL>Nat.SOM.Poly.denote ctx (p₁.mul p₂) = Nat.SOM.Poly.denote ctx p₁ * Nat.SOM.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>e : Nat.SOM.Expr<GOAL>Nat.SOM.Poly.denote ctx e.toPoly = Nat.SOM.Expr.denote ctx e
<VAR>ctx : Nat.Linear.Context<VAR>a b : Nat.SOM.Expr<VAR>h : (a.toPoly == b.toPoly) = true<GOAL>Nat.SOM.Expr.denote ctx a = Nat.SOM.Expr.denote ctx b
<VAR>α : Type u<VAR>self : Subarray α<GOAL>self.stop ≤ self.array.size
<VAR>α : Type u<VAR>self : Subarray α<GOAL>self.start ≤ self.stop
<VAR>α : Type u_1<VAR>s : Subarray α<GOAL>s.start ≤ s.stop
<VAR>α : Type u_1<VAR>s : Subarray α<GOAL>s.stop ≤ s.array.size
<VAR>α : Type u_1<VAR>s : Subarray α<GOAL>s.size ≤ s.array.size
<VAR>n : Nat<VAR>h : Char.isValidCharNat n<GOAL>n < UInt32.size
<VAR>n : Nat<VAR>h : Char.isValidCharNat n<GOAL>isValidChar (UInt32.ofNat' n ⋯)
<VAR>α : Type u_1<VAR>a : α<VAR>as : Array α<VAR>self : Array.Mem a as<GOAL>a ∈ as.data
<VAR>α : Type u_1<VAR>a : α<VAR>SizeOf α<VAR>as : Array α<VAR>h : a ∈ as<GOAL>sizeOf a < sizeOf as
<VAR>α : Type u_1<VAR>SizeOf α<VAR>as : Array α<VAR>i : Fin as.size<GOAL>sizeOf (as.get i) < sizeOf as
<VAR>α : Type u_1<VAR>SizeOf α<VAR>as : Array α<VAR>i : Nat<VAR>h : i < as.size<GOAL>sizeOf as[i] < sizeOf as
<VAR>n : Nat<VAR>a m : Fin n<GOAL>a % m = ⟨↑a % ↑m, ⋯⟩
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a * b = ⟨↑a * ↑b % n, ⋯⟩
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a - b = ⟨(n - ↑b + ↑a) % n, ⋯⟩
<VAR>n : Nat<VAR>Nonempty (Fin n)<GOAL>0 < n
<VAR>n : Nat<VAR>a : Fin n<GOAL>↑a < n
<VAR>n : Nat<GOAL>0 < n ↔ Nonempty (Fin n)
<VAR>n : Nat<VAR>a : Fin n<VAR>h : ↑a < n<GOAL>⟨↑a, h⟩ = a
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : ↑a = ↑b<GOAL>a = b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a = b ↔ ↑a = ↑b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑a ≠ ↑b ↔ a ≠ b
<VAR>n : Nat<VAR>p : Fin n → Prop<GOAL>(∀ (i : Fin n), p i) ↔ ∀ (i : Nat) (h : i < n), p ⟨i, h⟩
<VAR>n a b : Nat<VAR>ha : a < n<VAR>hb : b < n<GOAL>⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b
<VAR>m n : Nat<VAR>h : m < n<GOAL>↑⟨m, h⟩ = m
<VAR>n : Nat<VAR>a : Fin n<VAR>k : Nat<VAR>hk : k < n<GOAL>a = ⟨k, hk⟩ ↔ ↑a = k
<VAR>n : Nat<VAR>i : Fin n<GOAL>⟨↑i, ⋯⟩ = i
<VAR>n : Nat<VAR>a : Nat<VAR>is_pos : n > 0<GOAL>↑(Fin.ofNat' a is_pos) = a % n
<GOAL>∀ {a : Nat} {h : a > 0}, ↑(Fin.ofNat' 0 h) = 0
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a % b) = ↑a % ↑b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a / b) = ↑a / ↑b
<VAR>n : Nat<VAR>a : Fin n<VAR>b : Nat<GOAL>↑(a.modn b) = ↑a % b
<VAR>n : Nat<VAR>c : Prop<VAR>Decidable c<VAR>x : c → Fin n<VAR>y : ¬c → Fin n<GOAL>↑(if h : c then x h else y h) = if h : c then ↑(x h) else ↑(y h)
<VAR>n : Nat<VAR>c : Prop<VAR>Decidable c<VAR>x y : Fin n<GOAL>↑(if c then x else y) = if c then ↑x else ↑y
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a ≤ b ↔ ↑a ≤ ↑b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a < b ↔ ↑a < ↑b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>¬a ≤ b ↔ b < a
<VAR>n : Nat<VAR>a b : Fin n<GOAL>¬a < b ↔ b ≤ a
<VAR>n : Nat<VAR>a : Fin n<GOAL>a ≤ a
<VAR>n : Nat<VAR>a : Fin n<GOAL>¬a < a
<VAR>n : Nat<VAR>a b c : Fin n<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>n : Nat<VAR>a b c : Fin n<GOAL>a < b → b < c → a < c
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a ≤ b ∨ b ≤ a
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a < b<GOAL>¬b < a
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a < b<GOAL>a ≠ b
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a < b<GOAL>b ≠ a
<VAR>n : Nat<VAR>a b : Fin n<VAR>h : a < b<GOAL>a ≤ b
<VAR>n : Nat<VAR>i : Fin (n + 1)<GOAL>↑i ≤ n
<VAR>n : Nat<VAR>a : Fin n<GOAL>↑a ≤ n
<VAR>n : Nat<VAR>b : Fin n<VAR>a : Nat<VAR>h : a < ↑b<GOAL>⟨a, ⋯⟩ < b
<VAR>n : Nat<VAR>b : Fin n<VAR>a : Nat<VAR>h : a ≤ ↑b<GOAL>⟨a, ⋯⟩ ≤ b
<VAR>n x y : Nat<VAR>hx : x < n<VAR>hy : y < n<GOAL>⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y
<VAR>n x y : Nat<VAR>hx : x < n<VAR>hy : y < n<GOAL>⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y
<VAR>n : Nat<VAR>a : Fin (n + 1)<GOAL>0 ≤ a
<VAR>n : Nat<VAR>a : Fin (n + 1)<GOAL>¬a < 0
<VAR>n : Nat<VAR>a : Fin (n + 1)<GOAL>0 < a ↔ a ≠ 0
<VAR>n : Nat<VAR>i : Fin (n + 1)<GOAL>i = 0 ∨ ∃ j, i = j.succ
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>∃ j, i = j.succ
<VAR>n : Nat<VAR>i : Fin n<GOAL>↑i.rev = n - (↑i + 1)
<VAR>n : Nat<VAR>i : Fin n<GOAL>i.rev.rev = i
<VAR>n : Nat<VAR>i j : Fin n<GOAL>i.rev ≤ j.rev ↔ j ≤ i
<VAR>n : Nat<VAR>i j : Fin n<GOAL>i.rev = j.rev ↔ i = j
<VAR>n a : Nat<VAR>i : Fin (n + 1)<VAR>h : n = a + ↑i<GOAL>i.rev = ⟨a, ⋯⟩
<VAR>n : Nat<VAR>i j : Fin n<GOAL>i.rev < j.rev ↔ j < i
<VAR>n : Nat<GOAL>↑(Fin.last n) = n
<VAR>n : Nat<VAR>i : Fin (n + 1)<GOAL>i ≤ Fin.last n
<VAR>n : Nat<GOAL>0 < Fin.last (n + 1)
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>h : ¬↑i < n<GOAL>i = Fin.last n
<VAR>n : Nat<VAR>i : Fin (n + 1)<GOAL>i ≠ Fin.last n → ↑i < n
<VAR>n : Nat<GOAL>(Fin.last n).rev = 0
<VAR>n : Nat<GOAL>Fin.rev 0 = Fin.last n
<VAR>n : Nat<GOAL>⟨1, ⋯⟩ = 1
<VAR>n : Nat<GOAL>Subsingleton (Fin n) ↔ n ≤ 1
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a + b = ⟨(↑a + ↑b) % n, ⋯⟩
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a + b) = (↑a + ↑b) % n
<VAR>n : Nat<VAR>i : Fin n.succ<VAR>h : i < Fin.last n<GOAL>↑(i + 1) = ↑i + 1
<VAR>n : Nat<GOAL>Fin.last n + 1 = 0
<VAR>n : Nat<VAR>i : Fin (n + 1)<GOAL>↑(i + 1) = if i = Fin.last n then 0 else ↑i + 1
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>h : i < Fin.last n<GOAL>0 < i + 1
<VAR>n : Nat<VAR>j : Fin n<GOAL>↑j.succ = ↑j + 1
<VAR>n : Nat<VAR>a : Fin n<GOAL>0 < a.succ
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a.succ ≤ b.succ ↔ a ≤ b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a.succ < b.succ ↔ a < b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a.succ = b.succ ↔ a = b
<VAR>n : Nat<VAR>k : Fin n<GOAL>k.succ ≠ 0
<VAR>n : Nat<GOAL>Fin.succ 0 = 1
<VAR>n : Nat<GOAL>Fin.succ 1 = 2
<VAR>n i : Nat<VAR>h : i < n<GOAL>⟨i, h⟩.succ = ⟨i + 1, ⋯⟩
<VAR>n : Nat<VAR>i : Nat<VAR>h : i < n<GOAL>0 < ⟨i.succ, ⋯⟩
<VAR>n : Nat<VAR>a : Fin n<GOAL>1 < a.succ.succ
<VAR>n : Nat<VAR>k : Fin (n + 2)<GOAL>k + 1 < k ↔ k = Fin.last (n + 1)
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>k + 1 ≤ k ↔ k = Fin.last n
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>Fin.last n ≤ k ↔ k = Fin.last n
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>k < k + 1 ↔ k < Fin.last n
<VAR>n : Nat<VAR>k : Fin (n + 1)<GOAL>k ≤ 0 ↔ k = 0
<VAR>n : Nat<VAR>a : Fin n<GOAL>a.succ.succ ≠ 1
<VAR>m n : Nat<VAR>i : Fin m<VAR>h : ↑i < n<GOAL>↑(i.castLT h) = ↑i
<VAR>i n m : Nat<VAR>hn : i < n<VAR>hm : i < m<GOAL>⟨i, hn⟩.castLT hm = ⟨i, hm⟩
<VAR>n m : Nat<VAR>h : n ≤ m<VAR>i : Fin n<GOAL>↑(Fin.castLE h i) = ↑i
<VAR>i n m : Nat<VAR>hn : i < n<VAR>h : n ≤ m<GOAL>Fin.castLE h ⟨i, hn⟩ = ⟨i, ⋯⟩
<VAR>n m : Nat<VAR>h : n.succ ≤ m.succ<GOAL>Fin.castLE h 0 = 0
<VAR>m n : Nat<VAR>h : m + 1 ≤ n + 1<VAR>i : Fin m<GOAL>Fin.castLE h i.succ = (Fin.castLE ⋯ i).succ
<VAR>k m n : Nat<VAR>km : k ≤ m<VAR>mn : m ≤ n<VAR>i : Fin k<GOAL>Fin.castLE mn (Fin.castLE km i) = Fin.castLE ⋯ i
<VAR>k m n : Nat<VAR>km : k ≤ m<VAR>mn : m ≤ n<GOAL>Fin.castLE mn ∘ Fin.castLE km = Fin.castLE ⋯
<VAR>n m : Nat<VAR>h : n = m<VAR>i : Fin n<GOAL>↑(Fin.cast h i) = ↑i
<VAR>n n' : Nat<VAR>h : n + 1 = n' + 1<GOAL>Fin.cast h (Fin.last n) = Fin.last n'
<VAR>n m : Nat<VAR>h : n = m<VAR>i : Nat<VAR>hn : i < n<GOAL>Fin.cast h ⟨i, hn⟩ = ⟨i, ⋯⟩
<VAR>n m k : Nat<VAR>h : n = m<VAR>h' : m = k<VAR>i : Fin n<GOAL>Fin.cast h' (Fin.cast h i) = Fin.cast ⋯ i
<VAR>m n : Nat<VAR>h : m = n<VAR>h' : m ≤ n<GOAL>Fin.castLE h' = Fin.cast h
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin n<GOAL>↑(Fin.castAdd m i) = ↑i
<VAR>n : Nat<GOAL>Fin.castAdd 0 = Fin.cast ⋯
<VAR>m : Nat<VAR>n : Nat<VAR>i : Fin m<GOAL>↑(Fin.castAdd n i) < m
<VAR>n : Nat<VAR>m i : Nat<VAR>h : i < n<GOAL>Fin.castAdd m ⟨i, h⟩ = ⟨i, ⋯⟩
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin (n + m)<VAR>hi : ↑i < n<GOAL>Fin.castAdd m (i.castLT hi) = i
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin n<GOAL>(Fin.castAdd m i).castLT ⋯ = i
<VAR>n n' : Nat<VAR>m : Nat<VAR>i : Fin n'<VAR>h : n' = n<GOAL>Fin.castAdd m (Fin.cast h i) = Fin.cast ⋯ (Fin.castAdd m i)
<VAR>n n' m : Nat<VAR>i : Fin n'<VAR>h : n' + m = n + m<GOAL>Fin.cast h (Fin.castAdd m i) = Fin.castAdd m (Fin.cast ⋯ i)
<VAR>n m m' : Nat<VAR>i : Fin n<VAR>h : n + m' = n + m<GOAL>Fin.cast h (Fin.castAdd m' i) = Fin.castAdd m i
<VAR>m n p : Nat<VAR>i : Fin m<GOAL>Fin.castAdd p (Fin.castAdd n i) = Fin.cast ⋯ (Fin.castAdd (n + p) i)
<VAR>n n' : Nat<VAR>i : Fin n<VAR>h : n.succ = n'.succ<GOAL>Fin.cast h i.succ = (Fin.cast ⋯ i).succ
<VAR>n n' : Nat<VAR>i : Fin n<VAR>h : n = n'<GOAL>(Fin.cast h i).succ = Fin.cast ⋯ i.succ
<VAR>n : Nat<VAR>i : Fin n<GOAL>↑i.castSucc = ↑i
<VAR>n i : Nat<VAR>h : i < n<GOAL>⟨i, h⟩.castSucc = ⟨i, ⋯⟩
<VAR>n n' : Nat<VAR>h : n + 1 = n' + 1<VAR>i : Fin n<GOAL>Fin.cast h i.castSucc = (Fin.cast ⋯ i).castSucc
<VAR>n : Nat<VAR>i : Fin n<GOAL>i.castSucc < i.succ
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>i ≤ j.castSucc ↔ i < j.succ
<VAR>n : Nat<VAR>i : Fin n<VAR>j : Fin (n + 1)<GOAL>i.castSucc < j ↔ i.succ ≤ j
<VAR>n : Nat<GOAL>(Fin.last n).succ = Fin.last n.succ
<VAR>n : Nat<VAR>i : Fin n.succ<GOAL>i.succ = Fin.last (n + 1) ↔ i = Fin.last n
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>h : ↑i < n<GOAL>(i.castLT h).castSucc = i
<VAR>n : Nat<VAR>a : Fin n<VAR>h : ↑a < n<GOAL>a.castSucc.castLT h = a
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a.castSucc < b.castSucc ↔ a < b
<VAR>n : Nat<VAR>a b : Fin n<GOAL>a.castSucc = b.castSucc ↔ a = b
<VAR>n : Nat<VAR>a : Fin n<GOAL>a.castSucc < Fin.last n
<VAR>n : Nat<GOAL>Fin.castSucc 0 = 0
<VAR>n : Nat<GOAL>Fin.castSucc 1 = 1
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>h : 0 < i<GOAL>0 < i.castSucc
<VAR>n : Nat<VAR>a : Fin (n + 1)<GOAL>a.castSucc = 0 ↔ a = 0
<VAR>n : Nat<VAR>a : Fin (n + 1)<GOAL>a.castSucc ≠ 0 ↔ a ≠ 0
<VAR>n : Nat<VAR>j : Fin n<GOAL>j.succ.castSucc = j.castSucc.succ
<VAR>n : Nat<VAR>a : Fin n<GOAL>a.castSucc + 1 = a.succ
<VAR>n : Nat<VAR>a : Fin n<GOAL>a.castSucc < a.succ
<VAR>n : Nat<VAR>i : Fin (n + 1)<GOAL>(∃ j, j.castSucc = i) ↔ i ≠ Fin.last n
<VAR>n : Nat<VAR>i : Fin n<GOAL>i.castSucc.succ = i.succ.castSucc
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin n<GOAL>↑(i.addNat m) = ↑i + m
<VAR>n : Nat<VAR>i : Fin n<GOAL>i.addNat 1 = i.succ
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin n<GOAL>m ≤ ↑(i.addNat m)
<VAR>m : Nat<VAR>n i : Nat<VAR>hi : i < m<GOAL>⟨i, hi⟩.addNat n = ⟨i + n, ⋯⟩
<VAR>n n' : Nat<VAR>i : Fin n<VAR>h : n + 0 = n'<GOAL>Fin.cast h (i.addNat 0) = Fin.cast ⋯ i
<VAR>n n' m : Nat<VAR>i : Fin n'<VAR>h : n' = n<GOAL>(Fin.cast h i).addNat m = Fin.cast ⋯ (i.addNat m)
<VAR>n n' m : Nat<VAR>i : Fin n'<VAR>h : n' + m = n + m<GOAL>Fin.cast h (i.addNat m) = (Fin.cast ⋯ i).addNat m
<VAR>n m m' : Nat<VAR>i : Fin n<VAR>h : n + m' = n + m<GOAL>Fin.cast h (i.addNat m') = i.addNat m
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin m<GOAL>↑(Fin.natAdd n i) = n + ↑i
<VAR>m : Nat<VAR>n i : Nat<VAR>hi : i < m<GOAL>Fin.natAdd n ⟨i, hi⟩ = ⟨n + i, ⋯⟩
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin n<GOAL>m ≤ ↑(Fin.natAdd m i)
<VAR>n : Nat<GOAL>Fin.natAdd 0 = Fin.cast ⋯
<VAR>n n' : Nat<VAR>m : Nat<VAR>i : Fin n'<VAR>h : n' = n<GOAL>Fin.natAdd m (Fin.cast h i) = Fin.cast ⋯ (Fin.natAdd m i)
<VAR>n n' m : Nat<VAR>i : Fin n'<VAR>h : m + n' = m + n<GOAL>Fin.cast h (Fin.natAdd m i) = Fin.natAdd m (Fin.cast ⋯ i)
<VAR>n m m' : Nat<VAR>i : Fin n<VAR>h : m' + n = m + n<GOAL>Fin.cast h (Fin.natAdd m' i) = Fin.natAdd m i
<VAR>p m : Nat<VAR>n : Nat<VAR>i : Fin n<GOAL>Fin.castAdd p (Fin.natAdd m i) = Fin.cast ⋯ (Fin.natAdd m (Fin.castAdd p i))
<VAR>p m : Nat<VAR>n : Nat<VAR>i : Fin n<GOAL>Fin.natAdd m (Fin.castAdd p i) = Fin.cast ⋯ (Fin.castAdd p (Fin.natAdd m i))
<VAR>m n : Nat<VAR>p : Nat<VAR>i : Fin p<GOAL>Fin.natAdd m (Fin.natAdd n i) = Fin.cast ⋯ (Fin.natAdd (m + n) i)
<VAR>n n' : Nat<VAR>i : Fin n<VAR>h : 0 + n = n'<GOAL>Fin.cast h (Fin.natAdd 0 i) = Fin.cast ⋯ i
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin m<GOAL>Fin.cast ⋯ (Fin.natAdd n i) = i.addNat n
<VAR>n : Nat<VAR>m : Nat<VAR>i : Fin n<GOAL>Fin.cast ⋯ (i.addNat m) = Fin.natAdd m i
<VAR>m n : Nat<GOAL>Fin.natAdd n (Fin.last m) = Fin.last (n + m)
<VAR>m n : Nat<VAR>i : Fin m<GOAL>Fin.natAdd n i.castSucc = (Fin.natAdd n i).castSucc
<VAR>n : Nat<VAR>k : Fin n<VAR>m : Nat<GOAL>(Fin.castAdd m k).rev = k.rev.addNat m
<VAR>n : Nat<VAR>k : Fin n<VAR>m : Nat<GOAL>(k.addNat m).rev = Fin.castAdd m k.rev
<VAR>n : Nat<VAR>k : Fin n<GOAL>k.castSucc.rev = k.rev.succ
<VAR>n : Nat<VAR>k : Fin n<GOAL>k.succ.rev = k.rev.castSucc
<VAR>n : Nat<VAR>j : Fin (n + 1)<VAR>h : j ≠ 0<GOAL>↑(j.pred h) = ↑j - 1
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>h : i ≠ 0<GOAL>(i.pred h).succ = i
<VAR>n : Nat<VAR>i : Fin n<VAR>h : i.succ ≠ 0<GOAL>i.succ.pred h = i
<VAR>n : Nat<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<VAR>j : Fin n<GOAL>i.pred hi = j ↔ i = j.succ
<VAR>n : Nat<VAR>i : Nat<VAR>h : i < n + 1<GOAL>⟨i + 1, ⋯⟩.pred ⋯ = ⟨i, h⟩
<VAR>n : Nat<VAR>i : Nat<VAR>h₁ : i + 1 < n + 1 + 1<VAR>h₂ : ⟨i + 1, h₁⟩ ≠ 0<GOAL>⟨i + 1, h₁⟩.pred h₂ = ⟨i, ⋯⟩
<VAR>n : Nat<VAR>i : Nat<VAR>h : i < n + 1<VAR>w : ⟨i, h⟩ ≠ 0<GOAL>⟨i, h⟩.pred w = ⟨i - 1, ⋯⟩
<VAR>n : Nat<VAR>a b : Fin n.succ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.pred ha ≤ b.pred hb ↔ a ≤ b
<VAR>n : Nat<VAR>a b : Fin n.succ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.pred ha < b.pred hb ↔ a < b
<VAR>n : Nat<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.pred ha = b.pred hb ↔ a = b
<VAR>n : Nat<GOAL>Fin.pred 1 ⋯ = 0
<VAR>n : Nat<VAR>i : Fin (n + 2)<VAR>h : ↑i < n + 1<GOAL>(i + 1).pred ⋯ = i.castLT h
<VAR>n m : Nat<VAR>i : Fin (n + m)<VAR>h : m ≤ ↑i<GOAL>↑(Fin.subNat m i h) = ↑i - m
<VAR>n m i : Nat<VAR>h₁ : i < n + m<VAR>h₂ : m ≤ i<GOAL>Fin.subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, ⋯⟩
<VAR>n : Nat<VAR>i : Fin n<GOAL>i.succ.castSucc.pred ⋯ = i.castSucc
<VAR>n m : Nat<VAR>i : Fin (n + m)<VAR>h : m ≤ ↑i<GOAL>(Fin.subNat m i h).addNat m = i
<VAR>n : Nat<VAR>i : Fin n<VAR>m : Nat<VAR>h : m ≤ ↑(i.addNat m) := ⋯<GOAL>Fin.subNat m (i.addNat m) h = i
<VAR>n m : Nat<VAR>i : Fin (n + m)<VAR>h : n ≤ ↑i<GOAL>Fin.natAdd n (Fin.subNat n (Fin.cast ⋯ i) h) = i
<VAR>motive : (n : Nat) → Fin n → Sort u_1<VAR>zero : (n : Nat) → motive (n + 1) 0<VAR>succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ<VAR>n : Nat<GOAL>Fin.succRecOn 0 zero succ = zero n
<VAR>motive : (n : Nat) → Fin n → Sort u_1<VAR>zero : (n : Nat) → motive (n + 1) 0<VAR>succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ<VAR>n : Nat<VAR>i : Fin n<GOAL>i.succ.succRecOn zero succ = succ n i (i.succRecOn zero succ)
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive 0<VAR>hs : (i : Fin n) → motive i.castSucc → motive i.succ<GOAL>(fun i => Fin.induction zero hs i) 0 = zero
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive 0<VAR>succ : (i : Fin n) → motive i.castSucc → motive i.succ<VAR>i : Fin n<GOAL>Fin.induction zero succ i.succ = succ i (Fin.induction zero succ i.castSucc)
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive 0<VAR>succ : (i : Fin n) → motive i.succ<GOAL>Fin.cases zero succ 0 = zero
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive 0<VAR>succ : (i : Fin n) → motive i.succ<VAR>i : Fin n<GOAL>Fin.cases zero succ i.succ = succ i
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive 0<VAR>succ : (i : Fin n) → motive i.succ<VAR>i : Nat<VAR>h : i + 1 < n + 1<GOAL>Fin.cases zero succ ⟨i.succ, h⟩ = succ ⟨i, ⋯⟩
<VAR>n : Nat<VAR>P : Fin (n + 1) → Prop<GOAL>(∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ
<VAR>n : Nat<VAR>P : Fin (n + 1) → Prop<GOAL>(∃ i, P i) ↔ P 0 ∨ ∃ i, P i.succ
<VAR>p : Fin 1 → Prop<GOAL>(∀ (i : Fin 1), p i) ↔ p 0
<VAR>p : Fin 1 → Prop<GOAL>(∃ i, p i) ↔ p 0
<VAR>p : Fin 2 → Prop<GOAL>(∀ (i : Fin 2), p i) ↔ p 0 ∧ p 1
<VAR>p : Fin 2 → Prop<GOAL>(∃ i, p i) ↔ p 0 ∨ p 1
<VAR>a b : Fin 2<GOAL>(a = 0 ↔ b = 0) → a = b
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive (Fin.last n)<VAR>succ : (i : Fin n) → motive i.succ → motive i.castSucc<GOAL>Fin.reverseInduction zero succ (Fin.last n) = zero
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>zero : motive (Fin.last n)<VAR>succ : (i : Fin n) → motive i.succ → motive i.castSucc<VAR>i : Fin n<GOAL>Fin.reverseInduction zero succ i.castSucc = succ i (Fin.reverseInduction zero succ i.succ)
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>last : motive (Fin.last n)<VAR>cast : (i : Fin n) → motive i.castSucc<GOAL>Fin.lastCases last cast (Fin.last n) = last
<VAR>n : Nat<VAR>motive : Fin (n + 1) → Sort u_1<VAR>last : motive (Fin.last n)<VAR>cast : (i : Fin n) → motive i.castSucc<VAR>i : Fin n<GOAL>Fin.lastCases last cast i.castSucc = cast i
<VAR>m n : Nat<VAR>motive : Fin (m + n) → Sort u_1<VAR>left : (i : Fin m) → motive (Fin.castAdd n i)<VAR>right : (i : Fin n) → motive (Fin.natAdd m i)<VAR>i : Fin m<GOAL>Fin.addCases left right (Fin.castAdd n i) = left i
<VAR>m n : Nat<VAR>motive : Fin (m + n) → Sort u_1<VAR>left : (i : Fin m) → motive (Fin.castAdd n i)<VAR>right : (i : Fin n) → motive (Fin.natAdd m i)<VAR>i : Fin n<GOAL>Fin.addCases left right (Fin.natAdd m i) = right i
<VAR>n : Nat<VAR>x : Nat<VAR>lt : 0 < n<VAR>y : Fin n<GOAL>Fin.ofNat' x lt + y = Fin.ofNat' (x + ↑y) lt
<VAR>n : Nat<VAR>x : Fin n<VAR>y : Nat<VAR>lt : 0 < n<GOAL>x + Fin.ofNat' y lt = Fin.ofNat' (↑x + y) lt
<VAR>n : Nat<VAR>a b : Fin n<GOAL>↑(a - b) = (n - ↑b + ↑a) % n
<VAR>n : Nat<VAR>x : Nat<VAR>lt : 0 < n<VAR>y : Fin n<GOAL>Fin.ofNat' x lt - y = Fin.ofNat' (n - ↑y + x) lt
<VAR>n : Nat<VAR>x : Fin n<VAR>y : Nat<VAR>lt : 0 < n<GOAL>x - Fin.ofNat' y lt = Fin.ofNat' (n - y % n + ↑x) lt