ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b : ℕ<VAR>l : List ℕ<VAR>co : List.Pairwise Nat.Coprime l<GOAL>a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
<VAR>ι : Type u_1<VAR>a b : ℕ<VAR>s : ι → ℕ<VAR>l : List ι<VAR>co : List.Pairwise (Nat.Coprime on s) l<GOAL>a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<GOAL>↑(Nat.chineseRemainderOfList a s [] ⋯) = 0
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l : List ι<VAR>co : List.Pairwise (Nat.Coprime on s) l<VAR>hs : ∀ i ∈ l, s i ≠ 0<GOAL>↑(Nat.chineseRemainderOfList a s l co) < (List.map s l).prod
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l : List ι<VAR>co : List.Pairwise (Nat.Coprime on s) l<VAR>z : ℕ<VAR>hz : ∀ i ∈ l, z ≡ a i [MOD s i]<GOAL>z ≡ ↑(Nat.chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l l' : List ι<VAR>hl : l.Perm l'<VAR>hs : ∀ i ∈ l, s i ≠ 0<VAR>co : List.Pairwise (Nat.Coprime on s) l<GOAL>↑(Nat.chineseRemainderOfList a s l co) = ↑(Nat.chineseRemainderOfList a s l' ⋯)
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>m : Multiset ι<VAR>nod : m.Nodup<VAR>hs : ∀ i ∈ m, s i ≠ 0<VAR>pp : {x | x ∈ m}.Pairwise (Nat.Coprime on s)<GOAL>↑(Nat.chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>t : Finset ι<VAR>hs : ∀ i ∈ t, s i ≠ 0<VAR>pp : (↑t).Pairwise (Nat.Coprime on s)<GOAL>↑(Nat.chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i
<VAR>n : ℕ<GOAL>n.choose 0 = 1
<VAR>k : ℕ<GOAL>Nat.choose 0 k.succ = 0
<VAR>n k : ℕ<GOAL>n.succ.choose k.succ = n.choose k + n.choose k.succ
<VAR>n k : ℕ<GOAL>(n + 1).choose (k + 1) = n.choose k + n.choose (k + 1)
<VAR>n k : ℕ<GOAL>n < k → n.choose k = 0
<VAR>n : ℕ<GOAL>n.choose n.succ = 0
<VAR>n : ℕ<GOAL>n.choose 2 = n * (n - 1) / 2
<VAR>n k : ℕ<GOAL>k ≤ n → 0 < n.choose k
<VAR>n k : ℕ<GOAL>n.choose k = 0 ↔ n < k
<VAR>n k : ℕ<GOAL>n.succ * n.choose k = n.succ.choose k.succ * k.succ
<VAR>n k : ℕ<GOAL>k ≤ n → n.choose k * k ! * (n - k)! = n !
<VAR>n k s : ℕ<VAR>hkn : k ≤ n<VAR>hsk : s ≤ k<GOAL>n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>n.choose (n - k) = n.choose k
<VAR>a b : ℕ<GOAL>(a + b).choose a = (a + b).choose b
<VAR>n : ℕ<GOAL>(n + 1).choose n = n + 1
<VAR>n k : ℕ<GOAL>n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
<VAR>n k : ℕ<GOAL>n.ascFactorial k = k ! * (n + k - 1).choose k
<VAR>n k : ℕ<GOAL>k ! ∣ n.ascFactorial k
<VAR>n k : ℕ<GOAL>(n + k - 1).choose k = n.ascFactorial k / k !
<VAR>n k : ℕ<GOAL>n.descFactorial k = k ! * n.choose k
<VAR>n k : ℕ<GOAL>k ! ∣ n.descFactorial k
<VAR>n k : ℕ<GOAL>n.choose k = n.descFactorial k / k !
<VAR>a b c : ℕ<GOAL>a.choose c ≤ (a + b).choose c
<VAR>a b : ℕ<VAR>c : ℕ<VAR>h : a ≤ b<GOAL>a.choose c ≤ b.choose c
<VAR>b : ℕ<GOAL>Monotone fun a => a.choose b
<VAR>n : ℕ<GOAL>n.multichoose 0 = 1
<VAR>k : ℕ<GOAL>Nat.multichoose 0 (k + 1) = 0
<VAR>n k : ℕ<GOAL>(n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k
<VAR>k : ℕ<GOAL>Nat.multichoose 1 k = 1
<VAR>k : ℕ<GOAL>Nat.multichoose 2 k = k + 1
<VAR>n : ℕ<GOAL>n.multichoose 1 = n
<VAR>n k : ℕ<GOAL>n.multichoose k = (n + k - 1).choose k
<VAR>α : Fin 0 → Type u_1<VAR>(i : Fin 0) → Preorder (α i)<VAR>f g : (i : Fin 0) → α i<GOAL>f ≤ g
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>q : (i : Fin (n + 1)) → α i<GOAL>(Fin.tail fun k => q k) = fun k => q k.succ
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>p : (i : Fin n) → α i.succ<GOAL>Fin.tail (Fin.cons x p) = p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<GOAL>Fin.cons x p i.succ = p i
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>p : (i : Fin n) → α i.succ<GOAL>Fin.cons x p 0 = x
<VAR>n : ℕ<VAR>α : Fin (n + 2) → Type u_1<VAR>x : α 0<VAR>p : (i : Fin n.succ) → α i.succ<GOAL>Fin.cons x p 1 = p 0
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y : α i.succ<GOAL>Fin.cons x (Function.update p i y) = Function.update (Fin.cons x p) i.succ y
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<GOAL>Function.Injective2 Fin.cons
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x₀ y₀ : α 0<VAR>x y : (i : Fin n) → α i.succ<GOAL>Fin.cons x₀ x = Fin.cons y₀ y ↔ x₀ = y₀ ∧ x = y
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : (i : Fin n) → α i.succ<GOAL>Function.Injective fun x₀ => Fin.cons x₀ x
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x₀ : α 0<GOAL>Function.Injective (Fin.cons x₀)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>p : (i : Fin n) → α i.succ<VAR>z : α 0<GOAL>Function.update (Fin.cons x p) 0 z = Fin.cons z p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>q : (i : Fin (n + 1)) → α i<GOAL>Fin.cons (q 0) (Fin.tail q) = q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>P : ((i : Fin n.succ) → α i) → Sort v<VAR>h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (Fin.cons x₀ x)<VAR>x₀ : α 0<VAR>x : (i : Fin n) → α i.succ<GOAL>Fin.consCases h (Fin.cons x₀ x) = h x₀ x
<VAR>n : ℕ<VAR>α : Type u_1<VAR>x₀ : α<VAR>x : Fin n → α<VAR>hx₀ : x₀ ∉ Set.range x<VAR>hx : Function.Injective x<GOAL>Function.Injective (Fin.cons x₀ x)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>x₀ : α<VAR>x : Fin n → α<GOAL>Function.Injective (Fin.cons x₀ x) ↔ x₀ ∉ Set.range x ∧ Function.Injective x
<VAR>α : Fin 0 → Sort u_1<VAR>P : ((i : Fin 0) → α i) → Prop<GOAL>(∀ (x : (i : Fin 0) → α i), P x) ↔ P finZeroElim
<VAR>α : Fin 0 → Sort u_1<VAR>P : ((i : Fin 0) → α i) → Prop<GOAL>(∃ x, P x) ↔ P finZeroElim
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>P : ((i : Fin (n + 1)) → α i) → Prop<GOAL>(∀ (x : (i : Fin (n + 1)) → α i), P x) ↔ ∀ (a : α 0) (v : (i : Fin n) → α i.succ), P (Fin.cons a v)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>P : ((i : Fin (n + 1)) → α i) → Prop<GOAL>(∃ x, P x) ↔ ∃ a v, P (Fin.cons a v)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>q : (i : Fin (n + 1)) → α i<VAR>z : α 0<GOAL>Fin.tail (Function.update q 0 z) = Fin.tail q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>q : (i : Fin (n + 1)) → α i<VAR>i : Fin n<VAR>y : α i.succ<GOAL>Fin.tail (Function.update q i.succ y) = Function.update (Fin.tail q) i y
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : α → β<VAR>y : α<VAR>q : Fin n → α<GOAL>g ∘ Fin.cons y q = Fin.cons (g y) (g ∘ q)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : α → β<VAR>q : Fin n.succ → α<GOAL>g ∘ Fin.tail q = Fin.tail (g ∘ q)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>x : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<GOAL>q ≤ Fin.cons x p ↔ q 0 ≤ x ∧ Fin.tail q ≤ p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>x : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<GOAL>Fin.cons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ Fin.tail q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>x₀ y₀ : α 0<VAR>x y : (i : Fin n) → α i.succ<GOAL>Fin.cons x₀ x ≤ Fin.cons y₀ y ↔ x₀ ≤ y₀ ∧ x ≤ y
<VAR>n : ℕ<VAR>α : Type u_1<VAR>f : Fin (n + 1) → α<GOAL>Set.range f = insert (f 0) (Set.range (Fin.tail f))
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>b : Fin n → α<GOAL>Set.range (Fin.cons x b) = insert x (Set.range b)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin m<GOAL>Fin.append u v (Fin.castAdd n i) = u i
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin n<GOAL>Fin.append u v (Fin.natAdd m i) = v i
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hv : n = 0<GOAL>Fin.append u v = u ∘ Fin.cast ⋯
<VAR>m : ℕ<VAR>α : Type u_1<VAR>u : Fin m → α<GOAL>Fin.append u Fin.elim0 = u ∘ Fin.cast ⋯
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hu : m = 0<GOAL>Fin.append u v = v ∘ Fin.cast ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Fin n → α<GOAL>Fin.append Fin.elim0 v = v ∘ Fin.cast ⋯
<VAR>m n p : ℕ<VAR>α : Type u_1<VAR>a : Fin m → α<VAR>b : Fin n → α<VAR>c : Fin p → α<GOAL>Fin.append (Fin.append a b) c = Fin.append a (Fin.append b c) ∘ Fin.cast ⋯
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x₀ : Fin 1 → α<VAR>x : Fin n → α<GOAL>Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>x : α<VAR>xs : Fin n → α<GOAL>Fin.cons x xs = Fin.append (Fin.cons x Fin.elim0) xs ∘ Fin.cast ⋯
<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>ys : Fin m → α<VAR>n' : ℕ<VAR>h : n' = n<GOAL>Fin.append (xs ∘ Fin.cast h) ys = Fin.append xs ys ∘ Fin.cast ⋯
<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>ys : Fin m → α<VAR>m' : ℕ<VAR>h : m' = m<GOAL>Fin.append xs (ys ∘ Fin.cast h) = Fin.append xs ys ∘ Fin.cast ⋯
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>xs : Fin m → α<VAR>ys : Fin n → α<VAR>i : Fin (m + n)<GOAL>Fin.append xs ys i.rev = Fin.append (ys ∘ Fin.rev) (xs ∘ Fin.rev) (Fin.cast ⋯ i)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>xs : Fin m → α<VAR>ys : Fin n → α<GOAL>Fin.append xs ys ∘ Fin.rev = Fin.append (ys ∘ Fin.rev) (xs ∘ Fin.rev) ∘ Fin.cast ⋯
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>i : Fin (m * n)<GOAL>Fin.repeat m a i = a i.modNat
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<GOAL>Fin.repeat 0 a = Fin.elim0 ∘ Fin.cast ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<GOAL>Fin.repeat 1 a = a ∘ Fin.cast ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m : ℕ<GOAL>Fin.repeat m.succ a = Fin.append a (Fin.repeat m a) ∘ Fin.cast ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m₁ m₂ : ℕ<GOAL>Fin.repeat (m₁ + m₂) a = Fin.append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast ⋯
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>k : Fin (m * n)<GOAL>Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>a : Fin n → α<GOAL>Fin.repeat m a ∘ Fin.rev = Fin.repeat m (a ∘ Fin.rev)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>q : (i : Fin (n + 1)) → α i<GOAL>(Fin.init fun k => q k) = fun k => q k.castSucc
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (Fin.last n)<VAR>p : (i : Fin n) → α i.castSucc<GOAL>Fin.init (Fin.snoc p x) = p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (Fin.last n)<VAR>p : (i : Fin n) → α i.castSucc<VAR>i : Fin n<GOAL>Fin.snoc p x i.castSucc = p i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>f : Fin n → α<GOAL>Fin.snoc f a ∘ Fin.castSucc = f
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (Fin.last n)<VAR>p : (i : Fin n) → α i.castSucc<GOAL>Fin.snoc p x (Fin.last n) = x
<VAR>α : Type u_1<VAR>p : Fin 0 → α<VAR>x : α<GOAL>Fin.snoc p x = fun x_1 => x
<VAR>n m : ℕ<VAR>α : Type u_1<VAR>f : Fin (m + n) → α<VAR>a : α<GOAL>Fin.snoc f a ∘ Fin.natAdd m = Fin.snoc (f ∘ Fin.natAdd m) a
<VAR>m n : ℕ<VAR>α : Fin (n + m + 1) → Type u_1<VAR>f : (i : Fin (n + m)) → α i.castSucc<VAR>a : α (Fin.last (n + m))<VAR>i : Fin n<GOAL>Fin.snoc f a (Fin.castAdd (m + 1) i) = f (Fin.castAdd m i)
<VAR>n m : ℕ<VAR>α : Type u_1<VAR>f : Fin (n + m) → α<VAR>a : α<GOAL>Fin.snoc f a ∘ Fin.castAdd (m + 1) = f ∘ Fin.castAdd m
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (Fin.last n)<VAR>p : (i : Fin n) → α i.castSucc<VAR>i : Fin n<VAR>y : α i.castSucc<GOAL>Fin.snoc (Function.update p i y) x = Function.update (Fin.snoc p x) i.castSucc y
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (Fin.last n)<VAR>p : (i : Fin n) → α i.castSucc<VAR>z : α (Fin.last n)<GOAL>Function.update (Fin.snoc p x) (Fin.last n) z = Fin.snoc p z
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>q : (i : Fin (n + 1)) → α i<GOAL>Fin.snoc (Fin.init q) (q (Fin.last n)) = q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>q : (i : Fin (n + 1)) → α i<VAR>z : α (Fin.last n)<GOAL>Fin.init (Function.update q (Fin.last n) z) = Fin.init q
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>q : (i : Fin (n + 1)) → α i<VAR>i : Fin n<VAR>y : α i.castSucc<GOAL>Fin.init (Function.update q i.castSucc y) = Function.update (Fin.init q) i y
<VAR>n : ℕ<VAR>β : Type u_1<VAR>q : Fin (n + 2) → β<GOAL>Fin.tail (Fin.init q) = Fin.init (Fin.tail q)
<VAR>n : ℕ<VAR>β : Type u_1<VAR>a : β<VAR>q : Fin n → β<VAR>b : β<GOAL>Fin.cons a (Fin.snoc q b) = Fin.snoc (Fin.cons a q) b
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : α → β<VAR>q : Fin n → α<VAR>y : α<GOAL>g ∘ Fin.snoc q y = Fin.snoc (g ∘ q) (g y)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : Fin n → α<VAR>x₀ : Fin 1 → α<GOAL>Fin.append x x₀ = Fin.snoc x (x₀ 0)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>x : α<GOAL>Fin.snoc xs x = Fin.append xs (Fin.cons x Fin.elim0)
<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>x : α<VAR>ys : Fin m → α<GOAL>Fin.append (Fin.snoc xs x) ys = Fin.append xs (Fin.cons x ys) ∘ Fin.cast ⋯
<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>y : α<VAR>ys : Fin m → α<GOAL>Fin.append xs (Fin.cons y ys) = Fin.append (Fin.snoc xs y) ys ∘ Fin.cast ⋯
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>as : Fin n → α<VAR>bs : Fin m → α<GOAL>Fin.append (Fin.cons a as) bs = Fin.cons a (Fin.append as bs) ∘ Fin.cast ⋯
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>b : α<GOAL>Fin.append as (Fin.snoc bs b) = Fin.snoc (Fin.append as bs) b
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : α → β<VAR>q : Fin n.succ → α<GOAL>g ∘ Fin.init q = Fin.init (g ∘ q)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>P : ((i : Fin (n + 1)) → α i) → Sort u_1<VAR>h : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (Fin.last n)) → P (Fin.snoc x x₀)<VAR>x : (i : Fin n) → Fin.init α i<VAR>x₀ : α (Fin.last n)<GOAL>Fin.snocCases h (Fin.snoc x x₀) = h x x₀
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>i : Fin (n + 1)<GOAL>(∀ (j : Fin (n + 1)), p j) ↔ p i ∧ ∀ (j : Fin n), p (i.succAbove j)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth x p i = x
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>j : Fin n<GOAL>i.insertNth x p (i.succAbove j) = p j
<GOAL>@Fin.succAboveCases = @Fin.insertNth
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>p : Fin (n + 1)<VAR>a : α p<VAR>f : (i : Fin n) → α (p.succAbove i)<GOAL>p.removeNth (p.insertNth a f) = f
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>f : (i : Fin (n + 1)) → α i<GOAL>Fin.removeNth 0 f = Fin.tail f
<VAR>n : ℕ<VAR>α : Type u_1<VAR>f : Fin (n + 1) → α<GOAL>(Fin.last n).removeNth f = Fin.init f
<VAR>n : ℕ<VAR>β : Type v<VAR>i : Fin (n + 1)<VAR>x : β<VAR>p : Fin n → β<GOAL>i.insertNth x p ∘ i.succAbove = p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>p : Fin (n + 1)<VAR>a : α p<VAR>f : (i : Fin n) → α (p.succAbove i)<VAR>g : (j : Fin (n + 1)) → α j<GOAL>p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>p : Fin (n + 1)<VAR>a : α p<VAR>f : (i : Fin n) → α (p.succAbove i)<VAR>g : (j : Fin (n + 1)) → α j<GOAL>g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>i j : Fin (n + 1)<VAR>h : j < i<VAR>x : α i<VAR>p : (k : Fin n) → α (i.succAbove k)<GOAL>i.insertNth x p j = Eq.recOn ⋯ (p (j.castPred ⋯))
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>i j : Fin (n + 1)<VAR>h : i < j<VAR>x : α i<VAR>p : (k : Fin n) → α (i.succAbove k)<GOAL>i.insertNth x p j = Eq.recOn ⋯ (p (j.pred ⋯))
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>p : (j : Fin n) → α (Fin.succAbove 0 j)<GOAL>Fin.insertNth 0 x p = Fin.cons x fun j => cast ⋯ (p j)
<VAR>n : ℕ<VAR>β : Type v<VAR>x : β<VAR>p : Fin n → β<GOAL>Fin.insertNth 0 x p = Fin.cons x p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (Fin.last n)<VAR>p : (j : Fin n) → α ((Fin.last n).succAbove j)<GOAL>(Fin.last n).insertNth x p = Fin.snoc (fun j => cast ⋯ (p j)) x
<VAR>n : ℕ<VAR>β : Type v<VAR>x : β<VAR>p : Fin n → β<GOAL>(Fin.last n).insertNth x p = Fin.snoc p x
<VAR>n : ℕ<VAR>α : Type u_1<VAR>i : Fin (n + 1)<VAR>a : α<VAR>f : Fin n → α<VAR>j : Fin (n + 1)<GOAL>i.insertNth a f j.rev = i.rev.insertNth a (f ∘ Fin.rev) j
<VAR>n : ℕ<VAR>α : Type u_1<VAR>i : Fin (n + 1)<VAR>x : α<VAR>p : Fin n → α<GOAL>i.insertNth x p ∘ Fin.rev = i.rev.insertNth x (p ∘ Fin.rev)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<VAR>i : Fin (n + 1)<GOAL>Fin.cons a f i.rev = Fin.snoc (f ∘ Fin.rev) a i
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<GOAL>Fin.cons a f ∘ Fin.rev = Fin.snoc (f ∘ Fin.rev) a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<VAR>i : Fin (n + 1)<GOAL>Fin.snoc f a i.rev = Fin.cons a (f ∘ Fin.rev) i
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<GOAL>Fin.snoc f a ∘ Fin.rev = Fin.cons a (f ∘ Fin.rev)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>op : (j : Fin (n + 1)) → α j → α j → α j<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p q : (j : Fin n) → α (i.succAbove j)<GOAL>(i.insertNth (op i x y) fun j => op (i.succAbove j) (p j) (q j)) = fun j => op j (i.insertNth x p j) (i.insertNth y q j)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>q : (j : Fin (n + 1)) → α j<GOAL>i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (i.succAbove j)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>(i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>q : (j : Fin (n + 1)) → α j<GOAL>q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j => q (i.succAbove j)) ≤ p
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>p : Fin (n + 1)<VAR>x : α p<VAR>f : (j : Fin (n + 1)) → α j<GOAL>p.removeNth (Function.update f p x) = p.removeNth f
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>p : Fin (n + 1)<VAR>x : α p<VAR>f : (j : Fin (n + 1)) → α j<GOAL>p.insertNth x (p.removeNth f) = Function.update f p x
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>p : Fin (n + 1)<VAR>f : (j : Fin (n + 1)) → α j<GOAL>p.insertNth (f p) (p.removeNth f) = f
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>i : Fin n<GOAL>i ∈ Fin.find p → p i
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<GOAL>(Fin.find p).isSome = true ↔ ∃ i, p i
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<GOAL>Fin.find p = none ↔ ∀ (i : Fin n), ¬p i
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>i : Fin n<GOAL>i ∈ Fin.find p → ∀ {j : Fin n}, j < i → ¬p j
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>i : Fin n<VAR>h : i ∈ Fin.find p<VAR>j : Fin n<VAR>hj : p j<GOAL>i ≤ j
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩<GOAL>⟨Nat.find h, ⋯⟩ ∈ Fin.find p
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>i : Fin n<GOAL>i ∈ Fin.find p ↔ p i ∧ ∀ (j : Fin n), p j → i ≤ j
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>i : Fin n<GOAL>Fin.find p = some i ↔ p i ∧ ∀ (j : Fin n), p j → i ≤ j
<VAR>n : ℕ<VAR>p : Fin n → Prop<VAR>DecidablePred p<VAR>h : ∀ (i j : Fin n), p i → p j → i = j<VAR>i : Fin n<VAR>hi : p i<GOAL>i ∈ Fin.find p
<VAR>n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>h : ↑k < ↑j<GOAL>j.contractNth op g k = g k.castSucc
<VAR>n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>h : ↑k = ↑j<GOAL>j.contractNth op g k = op (g k.castSucc) (g k.succ)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>h : ↑j < ↑k<GOAL>j.contractNth op g k = g k.succ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>hjk : ↑j ≠ ↑k<GOAL>j.contractNth op g k = g (j.succAbove k)
<VAR>α : Type u_1<VAR>a b : (ii : ℕ) × (Fin ii → α)<VAR>h : a.fst = b.fst<GOAL>a.snd = b.snd ∘ Fin.cast h → a = b
<VAR>α : Type u_1<VAR>a b : (ii : ℕ) × (Fin ii → α)<GOAL>a = b ↔ ∃ (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h
<VAR>n k p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]
<VAR>n k p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℕ<GOAL>↑(n.choose k) ≡ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha₁ : n < p ^ a<VAR>ha₂ : k < p ^ a<GOAL>↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha₁ : n < p ^ a<VAR>ha₂ : k < p ^ a<GOAL>n.choose k ≡ ∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p) [MOD p]
<GOAL>{0} ∪ Set.range Nat.succ = Set.univ
<GOAL>Set.range Nat.succ = {i | 0 < i}
<VAR>α : Type u_1<VAR>f : ℕ → α<GOAL>{f 0} ∪ Set.range (f ∘ Nat.succ) = Set.range f
<VAR>α : Type u_2<VAR>x : α<VAR>f : ℕ → α → α<GOAL>(Set.range fun n => Nat.rec x f n) = {x} ∪ Set.range fun n => Nat.rec (f 0 x) (f ∘ Nat.succ) n
<VAR>α : Type u_2<VAR>x : α<VAR>f : ℕ → α<GOAL>(Set.range fun n => Nat.casesOn n x f) = {x} ∪ Set.range f
<VAR>n : ℕ<GOAL>n.succ.ppred = some n
<VAR>m : ℕ<GOAL>m.psub 0 = some m
<VAR>m n : ℕ<GOAL>m.psub n.succ = m.psub n >>= Nat.ppred
<VAR>n : ℕ<GOAL>n.pred = n.ppred.getD 0
<VAR>m n : ℕ<GOAL>m - n = (m.psub n).getD 0
<VAR>m n : ℕ<GOAL>n.ppred = some m ↔ m.succ = n
<VAR>n : ℕ<GOAL>n.ppred = none ↔ n = 0
<VAR>m n k : ℕ<GOAL>m.psub n = some k ↔ k + n = m
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>n.ppred = some n.pred
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>m.psub n = some (m - n)
<VAR>m n : ℕ<GOAL>m.psub' n = m.psub n
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<GOAL>Nat.evenOddRec h0 h_even h_odd 0 = h0
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<VAR>H : h_even 0 h0 = h0<VAR>n : ℕ<GOAL>Nat.evenOddRec h0 h_even h_odd (2 * n) = h_even n (Nat.evenOddRec h0 h_even h_odd n)
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<VAR>H : h_even 0 h0 = h0<VAR>n : ℕ<GOAL>Nat.evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (Nat.evenOddRec h0 h_even h_odd n)
<VAR>P : ℕ → Prop<VAR>h₀ : P 0<VAR>h₁ : P 1<VAR>h : ∀ (p a : ℕ), Nat.Prime p → P a → P (p * a)<VAR>n : ℕ<GOAL>P n
<VAR>P : ℕ → Prop<VAR>zero : P 0<VAR>one : P 1<VAR>prime : ∀ (p : ℕ), Nat.Prime p → P p<VAR>composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)<VAR>n : ℕ<GOAL>P n
<VAR>β : Type u_1<VAR>CommMonoid β<VAR>f : ℕ → β<VAR>h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y<VAR>hf : f 1 = 1<VAR>n : ℕ<GOAL>n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)
<VAR>n : ℕ<VAR>β : Type u_1<VAR>CommMonoid β<VAR>f : ℕ → β<VAR>h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y<VAR>hf0 : f 0 = 1<VAR>hf1 : f 1 = 1<GOAL>f n = n.factorization.prod fun p k => f (p ^ k)
<VAR>n : ℕ<GOAL>n.succ.bodd = !n.bodd
<VAR>m n : ℕ<GOAL>(m + n).bodd = bxor m.bodd n.bodd
<VAR>m n : ℕ<GOAL>(m * n).bodd = (m.bodd && n.bodd)
<VAR>n : ℕ<GOAL>n % 2 = bif n.bodd then 1 else 0
<VAR>n : ℕ<GOAL>n.succ.div2 = bif n.bodd then n.div2.succ else n.div2
<VAR>n : ℕ<GOAL>(bif n.bodd then 1 else 0) + 2 * n.div2 = n
<VAR>n : ℕ<GOAL>n.div2 = n / 2
<VAR>b : Bool<VAR>n : ℕ<GOAL>Nat.bit b n = 2 * n + bif b then 1 else 0
<VAR>n : ℕ<GOAL>Nat.bit n.bodd n.div2 = n
<VAR>m : ℕ<VAR>n : ℕ<GOAL>Nat.shiftLeft' false m n = m <<< n
<VAR>m n : ℕ<GOAL>m.shiftLeft n = m <<< n
<VAR>m n : ℕ<GOAL>m.shiftRight n = m >>> n
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>n.div2 < n
<VAR>C : ℕ → Sort u<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)<GOAL>Nat.binaryRec z f 0 = z
<VAR>b : Bool<VAR>n : ℕ<GOAL>(Nat.bit b n).bodd = b
<VAR>b : Bool<VAR>n : ℕ<GOAL>(Nat.bit b n).div2 = n
<VAR>b : Bool<VAR>m n k : ℕ<GOAL>Nat.shiftLeft' b m (n + k) = Nat.shiftLeft' b (Nat.shiftLeft' b m n) k
<VAR>b : Bool<VAR>m : ℕ<VAR>n k : ℕ<GOAL>k ≤ n → Nat.shiftLeft' b m (n - k) = Nat.shiftLeft' b m n >>> k
<VAR>m : ℕ<VAR>n k : ℕ<GOAL>k ≤ n → m <<< (n - k) = m <<< n >>> k
<VAR>b : Bool<VAR>n : ℕ<GOAL>(Nat.bit b n).testBit 0 = b
<VAR>n : ℕ<GOAL>n.bodd = (1 &&& n != 0)
<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(Nat.bit b n).testBit m.succ = n.testBit m
<VAR>C : ℕ → Sort u<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)<VAR>h : f false 0 z = z<VAR>b : Bool<VAR>n : ℕ<GOAL>Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)
<VAR>n : ℕ<GOAL>n.boddDiv2 = (n.bodd, n.div2)
<VAR>n : ℕ<GOAL>(2 * n).div2 = n
<VAR>n : ℕ<GOAL>(2 * n + 1).div2 = n
<VAR>b : Bool<VAR>n m : ℕ<GOAL>Nat.bit b (n + m) = Nat.bit false n + Nat.bit b m
<VAR>b : Bool<VAR>n m : ℕ<GOAL>Nat.bit b (n + m) = Nat.bit b n + Nat.bit false m
<VAR>b : Bool<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Nat.bit b n ≠ 0