ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>0 < Nat.clog b n
<VAR>b n : ℕ<VAR>hn : 2 ≤ n<VAR>h : n ≤ b<GOAL>Nat.clog b n = 1
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x y : ℕ<GOAL>x ≤ b ^ y ↔ Nat.clog b x ≤ y
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x y : ℕ<GOAL>b ^ y < x ↔ y < Nat.clog b x
<VAR>b x : ℕ<VAR>hb : 1 < b<GOAL>Nat.clog b (b ^ x) = x
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<VAR>hx : 1 < x<GOAL>b ^ (Nat.clog b x).pred < x
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<GOAL>x ≤ b ^ Nat.clog b x
<VAR>b : ℕ<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>Nat.clog b n ≤ Nat.clog b m
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<GOAL>Nat.clog b n ≤ Nat.clog c n
<VAR>b : ℕ<GOAL>Monotone (Nat.clog b)
<VAR>n : ℕ<GOAL>AntitoneOn (fun b => Nat.clog b n) (Set.Ioi 1)
<VAR>b n : ℕ<GOAL>Nat.log b n ≤ Nat.clog b n
<VAR>a b : ℕ<GOAL>Nat.cast '' Set.Icc a b = Set.Icc ↑a ↑b
<VAR>a b : ℕ<GOAL>Nat.cast '' Set.Ico a b = Set.Ico ↑a ↑b
<VAR>a b : ℕ<GOAL>Nat.cast '' Set.Ioc a b = Set.Ioc ↑a ↑b
<VAR>a b : ℕ<GOAL>Nat.cast '' Set.Ioo a b = Set.Ioo ↑a ↑b
<VAR>a : ℕ<GOAL>Nat.cast '' Set.Iic a = Set.Icc 0 ↑a
<VAR>a : ℕ<GOAL>Nat.cast '' Set.Iio a = Set.Ico 0 ↑a
<VAR>a : ℕ<GOAL>Nat.cast '' Set.Ici a = Set.Ici ↑a
<VAR>a : ℕ<GOAL>Nat.cast '' Set.Ioi a = Set.Ioi ↑a
<VAR>n : ℕ<VAR>NeZero n<GOAL>1 ≤ n
<VAR>n : ℕ<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>h : NeZero ↑n<GOAL>↑n ≠ 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n : ℕ<VAR>h : NeZero ↑n<GOAL>NeZero n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n : ℕ<VAR>NeZero ↑n<GOAL>0 < n
<VAR>u : PNat.XgcdType<GOAL>u.v = PNat.XgcdType.succ₂ u.vp
<VAR>u : PNat.XgcdType<GOAL>u.IsSpecial ↔ u.IsSpecial'
<VAR>u : PNat.XgcdType<GOAL>u.IsReduced ↔ u.IsReduced'
<VAR>u : PNat.XgcdType<GOAL>u.flip.w = u.z
<VAR>u : PNat.XgcdType<GOAL>u.flip.x = u.y
<VAR>u : PNat.XgcdType<GOAL>u.flip.y = u.x
<VAR>u : PNat.XgcdType<GOAL>u.flip.z = u.w
<VAR>u : PNat.XgcdType<GOAL>u.flip.a = u.b
<VAR>u : PNat.XgcdType<GOAL>u.flip.b = u.a
<VAR>u : PNat.XgcdType<GOAL>u.flip.IsReduced ↔ u.IsReduced
<VAR>u : PNat.XgcdType<GOAL>u.flip.IsSpecial ↔ u.IsSpecial
<VAR>u : PNat.XgcdType<GOAL>u.flip.v = u.v.swap
<VAR>u : PNat.XgcdType<GOAL>u.r + (u.bp + 1) * u.q = u.ap + 1
<VAR>u : PNat.XgcdType<VAR>hr : u.r = 0<GOAL>u.q = u.qp + 1
<VAR>a b : ℕ+<GOAL>(PNat.XgcdType.start a b).IsSpecial
<VAR>a b : ℕ+<GOAL>(PNat.XgcdType.start a b).v = (↑a, ↑b)
<VAR>u : PNat.XgcdType<GOAL>u.finish.IsReduced
<VAR>u : PNat.XgcdType<VAR>hs : u.IsSpecial<GOAL>u.finish.IsSpecial
<VAR>u : PNat.XgcdType<VAR>hr : u.r = 0<GOAL>u.finish.v = u.v
<VAR>u : PNat.XgcdType<VAR>hr : u.r ≠ 0<GOAL>sizeOf u.step < sizeOf u
<VAR>u : PNat.XgcdType<VAR>hs : u.IsSpecial<GOAL>u.step.IsSpecial
<VAR>u : PNat.XgcdType<VAR>hr : u.r ≠ 0<GOAL>u.step.v = u.v.swap
<VAR>u : PNat.XgcdType<VAR>h : u.r = 0<GOAL>u.reduce = u.finish
<VAR>u : PNat.XgcdType<VAR>h : u.r ≠ 0<GOAL>u.reduce = u.step.reduce.flip
<VAR>u : PNat.XgcdType<GOAL>u.reduce.IsReduced
<VAR>u : PNat.XgcdType<GOAL>u.reduce.IsReduced'
<VAR>u : PNat.XgcdType<GOAL>u.IsSpecial → u.reduce.IsSpecial
<VAR>u : PNat.XgcdType<VAR>hs : u.IsSpecial<GOAL>u.reduce.IsSpecial'
<VAR>u : PNat.XgcdType<GOAL>u.reduce.v = u.v
<VAR>a b : ℕ+<GOAL>↑(a.gcdA' b) = ↑(a.gcdW b) + a.gcdX b
<VAR>a b : ℕ+<GOAL>↑(a.gcdB' b) = a.gcdY b + ↑(a.gcdZ b)
<VAR>a b : ℕ+<GOAL>let d := a.gcdD b;
w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<GOAL>a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
<VAR>a b : ℕ+<GOAL>a = a.gcdA' b * a.gcd b
<VAR>a b : ℕ+<GOAL>b = a.gcdB' b * a.gcd b
<VAR>a b : ℕ+<GOAL>a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
<VAR>a b : ℕ+<GOAL>a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
<VAR>a b : ℕ+<GOAL>↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcd b)
<VAR>a b : ℕ+<GOAL>↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcd b)
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>OrderDual.toDual ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>OrderDual.ofDual ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OrderDual.ofDual (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>toLex ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>toLex (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<GOAL>ofLex ↑n = ↑n
<VAR>α : Type u_1<VAR>NatCast α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>ofLex (OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoidWithOne α<VAR>AddMonoidWithOne β<VAR>n : ℕ<GOAL>(↑n).1 = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoidWithOne α<VAR>AddMonoidWithOne β<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).1 = OfNat.ofNat n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoidWithOne α<VAR>AddMonoidWithOne β<VAR>n : ℕ<GOAL>(↑n).2 = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoidWithOne α<VAR>AddMonoidWithOne β<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).2 = OfNat.ofNat n
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>n : ℕ<VAR>x : α<GOAL>Commute (↑n) x
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>x : α<GOAL>Commute (OfNat.ofNat n) x
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>n : ℕ<VAR>x : α<GOAL>↑n * x = x * ↑n
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>x : α<VAR>n : ℕ<GOAL>Commute x ↑n
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>x : α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Commute x (OfNat.ofNat n)
<VAR>α : Type u_1<VAR>Semiring α<VAR>a x y : α<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (↑n * x) (↑n * y)
<VAR>α : Type u_1<VAR>Semiring α<VAR>a x y : α<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy (↑n * a) x y
<VAR>α : Type u_1<VAR>Semiring α<VAR>a x y : α<VAR>h : SemiconjBy a x y<VAR>m n : ℕ<GOAL>SemiconjBy (↑m * a) (↑n * x) (↑n * y)
<VAR>α : Type u_1<VAR>Semiring α<VAR>a b : α<VAR>h : Commute a b<VAR>n : ℕ<GOAL>Commute a (↑n * b)
<VAR>α : Type u_1<VAR>Semiring α<VAR>a b : α<VAR>h : Commute a b<VAR>n : ℕ<GOAL>Commute (↑n * a) b
<VAR>α : Type u_1<VAR>Semiring α<VAR>a b : α<VAR>h : Commute a b<VAR>m n : ℕ<GOAL>Commute (↑m * a) (↑n * b)
<VAR>α : Type u_1<VAR>Semiring α<VAR>a : α<VAR>n : ℕ<GOAL>Commute a (↑n * a)
<VAR>α : Type u_1<VAR>Semiring α<VAR>a : α<VAR>n : ℕ<GOAL>Commute (↑n * a) a
<VAR>α : Type u_1<VAR>Semiring α<VAR>a : α<VAR>m n : ℕ<GOAL>Commute (↑m * a) (↑n * a)
<VAR>n : ℕ<GOAL>Function.Injective Fin.val
<VAR>n : ℕ<GOAL>Fin n → 0 < n
<VAR>n : ℕ<VAR>Nonempty (Fin n)<GOAL>0 < n
<VAR>n : ℕ<VAR>a : Fin n<GOAL>↑a < n
<VAR>n : ℕ<VAR>a b c : Fin n<GOAL>a ≤ b → b < c → a < c
<VAR>n : ℕ<VAR>a b c : Fin n<GOAL>a < b → b ≤ c → a < c
<VAR>n : ℕ<VAR>a : Fin n<GOAL>a ≤ a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a < b ↔ a ≤ b ∧ a ≠ b
<VAR>n : ℕ<VAR>a b : Fin n<VAR>h : a ≠ b<GOAL>a < b ∨ b < a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a < b ∨ b ≤ a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a ≤ b ∨ b < a
<VAR>n : ℕ<VAR>a b : Fin n<VAR>hab : a = b<GOAL>a ≤ b
<VAR>n : ℕ<VAR>a b : Fin n<VAR>hab : a = b<GOAL>b ≤ a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a ≤ b → a = b ∨ a < b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a ≤ b → a < b ∨ a = b
<VAR>n : ℕ<VAR>a : Fin (n + 1)<GOAL>a < Fin.last n ↔ a ≠ Fin.last n
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>hab : a < b<GOAL>b ≠ 0
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>hab : a < b<GOAL>a ≠ Fin.last n
<VAR>n : ℕ<VAR>a : { i // i < n }<GOAL>Fin.equivSubtype.symm a = ⟨↑a, ⋯⟩
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Fin.equivSubtype a = ⟨↑a, ⋯⟩
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑a = ↑b ↔ a = b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a = b ↔ ↑a = ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a ≠ b ↔ ↑a ≠ ↑b
<VAR>n a : ℕ<VAR>h : a < n<VAR>a' : ℕ<VAR>h' : a' < n<GOAL>⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'
<VAR>α : Sort u_1<VAR>k l : ℕ<VAR>h : k = l<VAR>f : Fin k → α<VAR>g : Fin l → α<GOAL>HEq f g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩
<VAR>α : Sort u_1<VAR>k l k' l' : ℕ<VAR>h : k = l<VAR>h' : k' = l'<VAR>f : Fin k → Fin k' → α<VAR>g : Fin l → Fin l' → α<GOAL>HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
<VAR>k l : ℕ<VAR>h : k = l<VAR>i : Fin k<VAR>j : Fin l<GOAL>HEq i j ↔ ↑i = ↑j
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a ≤ b ↔ ↑a ≤ ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑a < ↑b ↔ a < b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>n : ℕ<VAR>a : Fin n<GOAL>min (↑a) n = ↑a
<VAR>n : ℕ<VAR>a : Fin n<GOAL>max (↑a) n = n
<VAR>n : ℕ<VAR>self : Fin n<GOAL>Fin.valEmbedding self = ↑self
<VAR>n : ℕ<GOAL>Fin.equivSubtype.symm.toEmbedding.trans Fin.valEmbedding = Function.Embedding.subtype fun x => x < n
<VAR>n : ℕ<VAR>NeZero n<GOAL>↑0 = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin n<GOAL>0 ≤ a
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin n<GOAL>0 < a ↔ a ≠ 0
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Fin.cast ⋯ a = a
<VAR>n : ℕ<GOAL>Function.Involutive Fin.rev
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Fin.revPerm i = i.rev
<VAR>n : ℕ<VAR>i : Fin n<GOAL>(Equiv.symm Fin.revPerm) i = i.rev
<VAR>n : ℕ<GOAL>Function.Injective Fin.rev
<VAR>n : ℕ<GOAL>Function.Surjective Fin.rev
<VAR>n : ℕ<GOAL>Function.Bijective Fin.rev
<VAR>n : ℕ<GOAL>Equiv.symm Fin.revPerm = Fin.revPerm
<VAR>n m : ℕ<VAR>i : Fin n<VAR>h : n = m<GOAL>Fin.cast h i.rev = (Fin.cast h i).rev
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i.rev = j ↔ i = j.rev
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i.rev ≠ j ↔ i ≠ j.rev
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i.rev < j ↔ j.rev < i
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i.rev ≤ j ↔ j.rev ≤ i
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i < j.rev ↔ j < i.rev
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i ≤ j.rev ↔ j ≤ i.rev
<VAR>n : ℕ<VAR>NeZero n<GOAL>↑(Fin.rev 0) = n.pred
<VAR>n : ℕ<VAR>NeZero n<GOAL>0 < Fin.last n
<VAR>n : ℕ<VAR>NeZero n<GOAL>1 < Fin.last (n + 1)
<VAR>n : ℕ<VAR>NeZero n<GOAL>↑1 = 1 % n
<VAR>n : ℕ<GOAL>↑1 = 1 % (n + 1)
<VAR>n : ℕ<GOAL>Nontrivial (Fin n) ↔ 2 ≤ n
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>k + 0 = k
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>0 + k = k
<VAR>n : ℕ<VAR>NeZero n<GOAL>default = 0
<VAR>n : ℕ<VAR>h : 0 < n<VAR>NeZero n<GOAL>Fin.ofNat' 0 h = 0
<VAR>n : ℕ<VAR>h : 0 < n<VAR>NeZero n<GOAL>Fin.ofNat' 1 h = 1
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ℕ<GOAL>↑a = ⟨a % n, ⋯⟩
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ℕ<GOAL>Fin.ofNat'' a = ↑a
<VAR>a n : ℕ<VAR>NeZero n<GOAL>↑↑a = a % n
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ℕ<VAR>h : a < n<GOAL>↑↑a = a
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin n<GOAL>↑↑a = a
<VAR>n : ℕ<VAR>NeZero n<GOAL>↑n = 0
<VAR>a n : ℕ<VAR>NeZero n<GOAL>↑a = 0 ↔ n ∣ a
<VAR>n : ℕ<GOAL>↑n = Fin.last n
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>i ≤ ↑n
<VAR>n a b : ℕ<VAR>han : a ≤ n<VAR>hbn : b ≤ n<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>n a b : ℕ<VAR>han : a ≤ n<VAR>hbn : b ≤ n<GOAL>↑a < ↑b ↔ a < b
<VAR>n a b : ℕ<VAR>hbn : b ≤ n<VAR>hab : a ≤ b<GOAL>↑a ≤ ↑b
<VAR>n a b : ℕ<VAR>hbn : b ≤ n<VAR>hab : a < b<GOAL>↑a < ↑b
<VAR>n : ℕ<VAR>NeZero n<GOAL>1 = 0 ↔ n = 1
<VAR>n : ℕ<VAR>NeZero n<GOAL>0 = 1 ↔ n = 1
<VAR>n : ℕ<GOAL>Function.Injective Fin.succ
<VAR>n : ℕ<GOAL>⇑(Fin.succEmb n) = Fin.succ
<VAR>n : ℕ<VAR>x : Fin (n + 1)<GOAL>(∃ y, y.succ = x) ↔ x ≠ 0
<VAR>n : ℕ<VAR>x : Fin (n + 1)<VAR>h : x ≠ 0<GOAL>∃ y, y.succ = x
<VAR>n : ℕ<VAR>NeZero n<GOAL>Fin.succ 0 = 1
<VAR>n : ℕ<VAR>NeZero n<GOAL>0 < 1
<VAR>n : ℕ<VAR>NeZero n<GOAL>0 ≠ 1
<VAR>n : ℕ<VAR>NeZero n<GOAL>Fin.succ 1 = 2
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>k ≤ 0 ↔ k = 0
<VAR>n : ℕ<VAR>h : n = n<GOAL>Fin.cast h = id
<VAR>n m : ℕ<VAR>hmn : m ≤ n<VAR>a b : Fin m<GOAL>Fin.castLE hmn a = Fin.castLE hmn b ↔ a = b
<VAR>n m : ℕ<VAR>a b : Fin m<GOAL>Fin.castAdd n a = Fin.castAdd n b ↔ a = b
<VAR>n m : ℕ<VAR>hmn : m ≤ n<GOAL>Function.Injective (Fin.castLE hmn)
<VAR>m n : ℕ<GOAL>Function.Injective (Fin.castAdd n)
<VAR>n : ℕ<GOAL>Function.Injective Fin.castSucc
<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>i : Fin n<GOAL>(Fin.castLEEmb h) i = Fin.castLE h i
<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>⇑(Fin.castLEEmb hmn) = Fin.castLE hmn
<VAR>n m : ℕ<GOAL>Nonempty (Fin n ↪ Fin m) ↔ n ≤ m
<VAR>n m : ℕ<GOAL>Nonempty (Fin m ≃ Fin n) ↔ m = n
<VAR>n m : ℕ<VAR>i : Fin n<VAR>h : n + 1 ≤ m<GOAL>Fin.castLE h i.castSucc = Fin.castLE ⋯ i
<VAR>n m : ℕ<VAR>h : n + 1 ≤ m<GOAL>Fin.castLE h ∘ Fin.castSucc = Fin.castLE ⋯
<VAR>n : ℕ<GOAL>Fin.castLE ⋯ = id
<VAR>n k : ℕ<VAR>h : n ≤ k<GOAL>Set.range (Fin.castLE h) = {i | ↑i < n}
<VAR>n k : ℕ<VAR>h : n ≤ k<VAR>i : Fin k<VAR>hi : i ∈ Set.range (Fin.castLE h)<GOAL>↑((Equiv.ofInjective (Fin.castLE h) ⋯).symm ⟨i, hi⟩) = ↑i
<VAR>n m : ℕ<VAR>eq : n = m<GOAL>Function.LeftInverse (Fin.cast ⋯) (Fin.cast eq)
<VAR>n m : ℕ<VAR>eq : n = m<GOAL>Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)
<VAR>n m : ℕ<VAR>eq : n = m<VAR>a b : Fin n<GOAL>Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b
<VAR>n m : ℕ<VAR>eq : n = m<VAR>i : Fin m<GOAL>(finCongr eq).symm i = Fin.cast ⋯ i
<VAR>n m : ℕ<VAR>eq : n = m<VAR>i : Fin n<GOAL>(finCongr eq) i = Fin.cast eq i
<VAR>n m : ℕ<VAR>h : m = n<VAR>k : ℕ<VAR>hk : k < m<GOAL>(finCongr h) ⟨k, hk⟩ = ⟨k, ⋯⟩
<VAR>n : ℕ<VAR>h : n = n := ⋯<GOAL>finCongr h = Equiv.refl (Fin n)
<VAR>n m : ℕ<VAR>h : m = n<GOAL>(finCongr h).symm = finCongr ⋯
<VAR>n m : ℕ<VAR>h : m = n<VAR>k : Fin m<GOAL>↑((finCongr h) k) = ↑k
<VAR>n m : ℕ<VAR>h : m = n<VAR>k : Fin n<GOAL>↑((finCongr h).symm k) = ↑k
<VAR>n m : ℕ<VAR>h : n = m<GOAL>finCongr h = Equiv.cast ⋯
<VAR>n n' : ℕ<VAR>NeZero n<VAR>h : n = n'<GOAL>Fin.cast h 0 = 0
<VAR>n m : ℕ<VAR>h : n = m<GOAL>Fin.cast h = cast ⋯
<VAR>n : ℕ<VAR>m : ℕ<VAR>i : Fin n<GOAL>(Fin.castAddEmb m) i = Fin.castLE ⋯ i
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Fin.castSuccEmb i = Fin.castLE ⋯ i
<VAR>n : ℕ<GOAL>⇑Fin.castSuccEmb = Fin.castSucc
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a.castSucc ≤ b.castSucc ↔ a ≤ b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a.succ ≤ b.castSucc ↔ a < b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>a.castSucc < b.succ ↔ a ≤ b
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>i : Fin n<VAR>hl : i.castSucc < a<VAR>hu : b < i.succ<GOAL>b < a
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>i.castSucc < p ∨ p < i.succ
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>i.succ ≤ p ∨ p ≤ i.castSucc
<VAR>n : ℕ<VAR>x : Fin (n + 1)<VAR>h : x ≠ Fin.last n<GOAL>∃ y, y.castSucc = x
<VAR>n : ℕ<VAR>P : Fin (n + 1) → Prop<GOAL>(∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P i.castSucc) ∧ P (Fin.last n)
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(∃ j, i = j.castSucc) ∨ i = Fin.last n
<VAR>n : ℕ<VAR>P : Fin (n + 1) → Prop<GOAL>(∃ i, P i) ↔ (∃ i, P i.castSucc) ∨ P (Fin.last n)
<VAR>n : ℕ<VAR>NeZero n<GOAL>Fin.castSucc 0 = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin n<VAR>h : 0 < i<GOAL>0 < i.castSucc
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin n<GOAL>a.castSucc = 0 ↔ a = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin n<GOAL>a.castSucc ≠ 0 ↔ a ≠ 0
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : p < i<GOAL>i.castSucc ≠ 0
<VAR>n : ℕ<VAR>a : Fin (n + 1)<GOAL>a.succ ≠ Fin.last (n + 1) ↔ a ≠ Fin.last n
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : i < p<GOAL>i.succ ≠ Fin.last n
<VAR>n : ℕ<VAR>a : Fin n<GOAL>↑↑a = a.castSucc
<VAR>n : ℕ<VAR>j k : Fin n<GOAL>↑↑j < ↑↑k ↔ j < k
<VAR>n : ℕ<GOAL>Set.range Fin.castSucc = {i | ↑i < n}
<VAR>n : ℕ<VAR>i : Fin n.succ<VAR>hi : i ∈ Set.range Fin.castSucc<GOAL>↑((Equiv.ofInjective Fin.castSucc ⋯).symm ⟨i, hi⟩) = ↑i
<VAR>n : ℕ<VAR>m : ℕ<GOAL>∀ (x : Fin n), (Fin.addNatEmb m) x = x.addNat m
<VAR>n : ℕ<VAR>m : ℕ<VAR>i : Fin m<GOAL>(Fin.natAddEmb n) i = Fin.natAdd n i
<VAR>n : ℕ<VAR>NeZero n<VAR>h : 1 ≠ 0 := ⋯<GOAL>Fin.pred 1 h = 0
<VAR>n : ℕ<VAR>h : ¬Fin.last (n + 1) = 0 := ⋯<GOAL>(Fin.last (n + 1)).pred h = Fin.last n
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>i.pred hi < j ↔ i < j.succ
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>j < i.pred hi ↔ j.succ < i
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>i.pred hi ≤ j ↔ i ≤ j.succ
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>j ≤ i.pred hi ↔ j.succ ≤ i
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<VAR>ha' : a.castSucc ≠ 0 := ⋯<GOAL>(a.pred ha).castSucc = a.castSucc.pred ha'
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>(a.pred ha).castSucc + 1 = a
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.castSucc ≠ 0<GOAL>b ≤ a.castSucc.pred ha ↔ b < a
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.castSucc ≠ 0<GOAL>a.castSucc.pred ha < b ↔ a ≤ b
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a.castSucc ≠ 0<GOAL>a.castSucc.pred ha < a
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>b ≤ (a.pred ha).castSucc ↔ b < a
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>(a.pred ha).castSucc < b ↔ a ≤ b
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>(a.pred ha).castSucc < a
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i < Fin.last n<VAR>h' : ¬i = Fin.last n := ⋯<GOAL>i.castLT h = i.castPred h'
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ Fin.last n<GOAL>↑(i.castPred h) = ↑i
<VAR>n : ℕ<VAR>i : Fin n<VAR>h' : ¬i.castSucc = Fin.last n := ⋯<GOAL>i.castSucc.castPred h' = i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ Fin.last n<GOAL>(i.castPred h).castSucc = i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>j : Fin n<GOAL>i.castPred hi = j ↔ i = j.castSucc
<VAR>n : ℕ<VAR>i : ℕ<VAR>h₁ : i < n<VAR>h₂ : i < n.succ := ⋯<VAR>h₃ : ⟨i, h₂⟩ ≠ Fin.last n := ⋯<GOAL>⟨i, h₂⟩.castPred h₃ = ⟨i, h₁⟩
<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>hj : j ≠ Fin.last n<GOAL>i.castPred hi ≤ j.castPred hj ↔ i ≤ j
<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>hj : j ≠ Fin.last n<GOAL>i.castPred hi < j.castPred hj ↔ i < j
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<GOAL>i.castPred hi < j ↔ i < j.castSucc
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<GOAL>j < i.castPred hi ↔ j.castSucc < i
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<GOAL>i.castPred hi ≤ j ↔ i ≤ j.castSucc
<VAR>n : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<GOAL>j ≤ i.castPred hi ↔ j.castSucc ≤ i
<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>hj : j ≠ Fin.last n<GOAL>i.castPred hi = j.castPred hj ↔ i = j
<VAR>n : ℕ<VAR>NeZero n<VAR>h : ¬0 = Fin.last n := ⋯<GOAL>Fin.castPred 0 h = 0
<VAR>n : ℕ<VAR>h : ¬0 = Fin.last (n + 1) := ⋯<GOAL>Fin.castPred 0 h = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>h : ¬1 = Fin.last (n + 1) := ⋯<GOAL>Fin.castPred 1 h = 1
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ 0<VAR>h' : i.rev ≠ Fin.last n := ⋯<GOAL>(i.pred h).rev = i.rev.castPred h'
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ Fin.last n<VAR>h' : i.rev ≠ 0 := ⋯<GOAL>(i.castPred h).rev = i.rev.pred h'
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ Fin.last n<VAR>ha' : a.succ ≠ Fin.last (n + 1) := ⋯<GOAL>(a.castPred ha).succ = a.succ.castPred ha'
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ Fin.last n<GOAL>(a.castPred ha).succ = a + 1
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.succ ≠ Fin.last (n + 1)<GOAL>a.succ.castPred ha ≤ b ↔ a < b
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.succ ≠ Fin.last (n + 1)<GOAL>b < a.succ.castPred ha ↔ b ≤ a
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a.succ ≠ Fin.last (n + 1)<GOAL>a < a.succ.castPred ha
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ Fin.last n<GOAL>(a.castPred ha).succ ≤ b ↔ a < b
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ Fin.last n<GOAL>b < (a.castPred ha).succ ↔ b ≤ a
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a ≠ Fin.last n<GOAL>a < (a.castPred ha).succ
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ Fin.last n<VAR>hb : b ≠ 0<GOAL>a.castPred ha ≤ b.pred hb ↔ a < b
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<VAR>hb : b ≠ Fin.last n<GOAL>a.pred ha < b.castPred hb ↔ a ≤ b
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>h₁ : a ≠ 0<VAR>h₂ : a ≠ Fin.last n<GOAL>a.pred h₁ < a.castPred h₂
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : i.castSucc < p<GOAL>p.succAbove i = i.castSucc
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : i.succ ≤ p<GOAL>p.succAbove i = i.castSucc
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : p ≤ i.castSucc<GOAL>p.succAbove i = i.succ
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : p < i.succ<GOAL>p.succAbove i = i.succ
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : p < i<GOAL>p.succ.succAbove i = i.succ
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : i ≤ p<GOAL>p.succ.succAbove i = i.castSucc
<VAR>n : ℕ<VAR>j : Fin n<GOAL>j.succ.succAbove j = j.castSucc
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : i < p<GOAL>p.castSucc.succAbove i = i.castSucc
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : p ≤ i<GOAL>p.castSucc.succAbove i = i.succ
<VAR>n : ℕ<VAR>j : Fin n<GOAL>j.castSucc.succAbove j = j.succ
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : p < i<VAR>hi : i ≠ 0 := ⋯<GOAL>p.succAbove (i.pred hi) = i
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : i ≤ p<VAR>hi : i ≠ 0<GOAL>p.succAbove (i.pred hi) = (i.pred hi).castSucc
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ 0<GOAL>p.succAbove (p.pred h) = (p.pred h).castSucc
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : i < p<VAR>hi : i ≠ Fin.last n := ⋯<GOAL>p.succAbove (i.castPred hi) = i
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : p ≤ i<VAR>hi : i ≠ Fin.last n<GOAL>p.succAbove (i.castPred hi) = (i.castPred hi).succ
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ Fin.last n<GOAL>p.succAbove (p.castPred h) = (p.castPred h).succ
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.rev.succAbove i = (p.succAbove i.rev).rev
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i.rev = (p.rev.succAbove i).rev
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i ≠ p
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p ≠ p.succAbove i
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>Function.Injective p.succAbove
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<GOAL>p.succAbove i = p.succAbove j ↔ i = j
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAboveEmb i = p.succAbove i
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>⇑p.succAboveEmb = p.succAbove
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>a.succAbove 0 = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin (n + 1)<VAR>b : Fin n<VAR>ha : a ≠ 0<GOAL>a.succAbove b = 0 ↔ b = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>a : Fin (n + 1)<VAR>b : Fin n<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.succAbove b ≠ 0
<VAR>n : ℕ<GOAL>Fin.succAbove 0 = Fin.succ
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Fin.succAbove 0 i = i.succ
<VAR>n : ℕ<VAR>a : Fin (n + 2)<VAR>h : a ≠ Fin.last (n + 1)<GOAL>a.succAbove (Fin.last n) = Fin.last (n + 1)
<VAR>n : ℕ<VAR>a : Fin (n + 2)<VAR>b : Fin (n + 1)<VAR>ha : a ≠ Fin.last (n + 1)<GOAL>a.succAbove b = Fin.last (n + 1) ↔ b = Fin.last n
<VAR>n : ℕ<VAR>a : Fin (n + 2)<VAR>b : Fin (n + 1)<VAR>ha : a ≠ Fin.last (n + 1)<VAR>hb : b ≠ Fin.last n<GOAL>a.succAbove b ≠ Fin.last (n + 1)
<VAR>n : ℕ<GOAL>(Fin.last n).succAbove = Fin.castSucc
<VAR>n : ℕ<VAR>i : Fin n<GOAL>(Fin.last n).succAbove i = i.castSucc
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>i.castSucc < p ∨ p ≤ i.castSucc
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i < p ↔ i.castSucc < p
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i < p ↔ i.succ ≤ p
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p < p.succAbove i ↔ p ≤ i.castSucc
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p < p.succAbove i ↔ p < i.succ
<VAR>n : ℕ<VAR>NeZero n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : 0 < i<GOAL>0 < p.succAbove i
<VAR>n : ℕ<VAR>x : Fin n<VAR>y : Fin (n + 1)<VAR>h : x.castSucc < y<VAR>h' : y.succAbove x ≠ Fin.last n := ⋯<GOAL>(y.succAbove x).castPred h' = x
<VAR>n : ℕ<VAR>x : Fin n<VAR>y : Fin (n + 1)<VAR>h : y ≤ x.castSucc<VAR>h' : y.succAbove x ≠ 0 := ⋯<GOAL>(y.succAbove x).pred h' = x
<VAR>n : ℕ<VAR>x y : Fin (n + 1)<VAR>h : x ≠ y<GOAL>∃ z, y.succAbove z = x
<VAR>n : ℕ<VAR>x y : Fin (n + 1)<GOAL>(∃ z, x.succAbove z = y) ↔ y ≠ x
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>Set.range p.succAbove = {p}ᶜ
<VAR>n : ℕ<GOAL>Set.range Fin.succ = {0}ᶜ
<VAR>n : ℕ<GOAL>Function.Injective Fin.succAbove
<VAR>n : ℕ<VAR>x y : Fin (n + 1)<GOAL>x.succAbove = y.succAbove ↔ x = y
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin n<GOAL>i.succ.succAbove 0 = 0
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>i.succ.succAbove j.succ = (i.succAbove j).succ
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
<VAR>n : ℕ<VAR>a : Fin (n + 2)<VAR>b : Fin (n + 1)<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hk : a.succAbove b ≠ 0 := ⋯<GOAL>(a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
<VAR>n : ℕ<VAR>a : Fin (n + 2)<VAR>b : Fin (n + 1)<VAR>ha : a ≠ Fin.last (n + 1)<VAR>hb : b ≠ Fin.last n<VAR>hk : a.succAbove b ≠ Fin.last (n + 1) := ⋯<GOAL>(a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>(p.succAbove i).rev = p.rev.succAbove i.rev
<VAR>n : ℕ<GOAL>Fin.succAbove 1 0 = 0