ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Icc (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Icc b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Ico (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ico b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Ioc (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioc b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Ioo (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioo b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Icc (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Icc a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Ico (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ico a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Ioc (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioc a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a₁ a₂ : α<GOAL>Finset.Ioo (Sum.inlₗ a₁) (Sum.inlₗ a₂) = Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioo a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Icc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iic b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Ico (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ici a).disjSum (Finset.Iio b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Ioc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iic b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Ioo (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iio b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Icc (Sum.inrₗ b) (Sum.inlₗ a) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Ico (Sum.inrₗ b) (Sum.inlₗ a) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Ioc (Sum.inrₗ b) (Sum.inlₗ a) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>a : α<VAR>b : β<GOAL>Finset.Ioo (Sum.inrₗ b) (Sum.inlₗ a) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Icc (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Icc b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Ico (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ico b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Ioc (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioc b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop α<VAR>OrderBot β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>b₁ b₂ : β<GOAL>Finset.Ioo (Sum.inrₗ b₁) (Sum.inrₗ b₂) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioo b₁ b₂)
<VAR>n : ℕ<GOAL>(↑n).bodd = n.bodd
<VAR>m n : ℕ<GOAL>(Int.subNatNat m n).bodd = xor m.bodd n.bodd
<VAR>n : ℕ<GOAL>(Int.negOfNat n).bodd = n.bodd
<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>Int.bit b n = 2 * n + bif b then 1 else 0
<VAR>n : ℤ<GOAL>Int.bit n.bodd n.div2 = n
<VAR>b : Bool<VAR>n : ℕ<GOAL>Int.bit b ↑n = ↑(Nat.bit b n)
<VAR>b : Bool<VAR>n : ℕ<GOAL>Int.bit b (Int.negSucc n) = Int.negSucc (Nat.bit (!b) n)
<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit b n).bodd = b
<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit b n).testBit 0 = b
<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit b n).testBit m.succ = n.testBit m
<GOAL>(Int.bitwise fun a b => a && !b) = Int.ldiff
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>Int.bitwise f (Int.bit a m) (Int.bit b n) = Int.bit (f a b) (Int.bitwise f m n)
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit a m).lor (Int.bit b n) = Int.bit (a || b) (m.lor n)
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit a m).land (Int.bit b n) = Int.bit (a && b) (m.land n)
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit a m).ldiff (Int.bit b n) = Int.bit (a && !b) (m.ldiff n)
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit a m).xor (Int.bit b n) = Int.bit (xor a b) (m.xor n)
<VAR>b : Bool<VAR>n : ℤ<GOAL>(Int.bit b n).lnot = Int.bit (!b) n.lnot
<VAR>f : Bool → Bool → Bool<VAR>m n : ℤ<VAR>k : ℕ<GOAL>(Int.bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)
<VAR>n : ℤ<VAR>k : ℕ<GOAL>n.lnot.testBit k = !n.testBit k
<VAR>m n : ℤ<GOAL>m <<< (-n) = m >>> n
<VAR>m n : ℕ<GOAL>↑m <<< ↑n = ↑(m <<< n)
<VAR>m n : ℕ<GOAL>↑m >>> ↑n = ↑(m >>> n)
<VAR>m n : ℕ<GOAL>Int.negSucc m <<< ↑n = Int.negSucc (Nat.shiftLeft' true m n)
<VAR>m n : ℕ<GOAL>Int.negSucc m >>> ↑n = Int.negSucc (m >>> n)
<VAR>m : ℤ<VAR>n k : ℕ<GOAL>m >>> (↑n + ↑k) = m >>> ↑n >>> ↑k
<VAR>m : ℤ<VAR>n : ℕ<VAR>k : ℤ<GOAL>m <<< (↑n + k) = m <<< ↑n <<< k
<VAR>m : ℤ<VAR>n : ℕ<VAR>k : ℤ<GOAL>m <<< (↑n - k) = m <<< ↑n >>> k
<VAR>m : ℤ<VAR>n : ℕ<GOAL>m <<< ↑n = m * ↑(2 ^ n)
<VAR>n : ℕ<GOAL>1 <<< ↑n = ↑(2 ^ n)
<VAR>n : ℤ<GOAL>0 <<< n = 0
<VAR>n : ℤ<GOAL>0 >>> n = 0
<VAR>s step : ℕ<GOAL>List.range' s 1 step = [s]
<VAR>s n : ℕ<VAR>step : ℕ := 1<GOAL>autoParam (0 < step) _auto✝ → List.Pairwise (fun x x_1 => x < x_1) (List.range' s n step)
<VAR>s n : ℕ<VAR>step : ℕ := 1<VAR>h : 0 < step := by simp<GOAL>(List.range' s n step).Nodup
<VAR>n m step : ℕ<VAR>i : ℕ<VAR>H : i < (List.range' n m step).length<GOAL>(List.range' n m step).nthLe i H = n + step * i
<VAR>n m : ℕ<VAR>i : ℕ<VAR>H : i < (List.range' n m).length<GOAL>(List.range' n m).nthLe i H = n + i
<VAR>n : ℕ<GOAL>List.Pairwise (fun x x_1 => x < x_1) (List.range n)
<VAR>n : ℕ<GOAL>List.Pairwise (fun x x_1 => x ≤ x_1) (List.range n)
<VAR>m n : ℕ<GOAL>List.take m (List.range n) = List.range (min m n)
<VAR>n : ℕ<GOAL>(List.range n).Nodup
<VAR>r : ℕ → ℕ → Prop<VAR>n : ℕ<GOAL>List.Chain' r (List.range n.succ) ↔ ∀ m < n, r m m.succ
<VAR>r : ℕ → ℕ → Prop<VAR>n a : ℕ<GOAL>List.Chain r a (List.range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ
<VAR>n : ℕ<GOAL>List.Pairwise (fun x x_1 => x > x_1) (List.iota n)
<VAR>n : ℕ<GOAL>(List.iota n).Nodup
<VAR>n : ℕ<VAR>a : Fin n<GOAL>a ∈ List.finRange n
<VAR>n : ℕ<GOAL>(List.finRange n).Nodup
<VAR>n : ℕ<GOAL>(List.finRange n).length = n
<VAR>n : ℕ<GOAL>List.finRange n = [] ↔ n = 0
<VAR>n : ℕ<GOAL>List.Pairwise (fun x x_1 => x < x_1) (List.finRange n)
<VAR>n : ℕ<GOAL>List.Pairwise (fun x x_1 => x ≤ x_1) (List.finRange n)
<VAR>α : Type u<VAR>l : List α<GOAL>l.enum = (List.range l.length).zip l
<VAR>α : Type u<VAR>l : List α<GOAL>l.enum.unzip = (List.range l.length, l)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>List.enumFrom n l = (List.range' n l.length).zip l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(List.enumFrom n l).unzip = (List.range' n l.length, l)
<VAR>n : ℕ<VAR>i : ℕ<VAR>H : i < (List.range n).length<GOAL>(List.range n).nthLe i H = i
<VAR>n i : ℕ<VAR>h : i < (List.finRange n).length<GOAL>(List.finRange n)[i] = ⟨i, ⋯⟩
<VAR>n i : ℕ<VAR>h : i < (List.finRange n).length<GOAL>(List.finRange n).get ⟨i, h⟩ = ⟨i, ⋯⟩
<VAR>α : Type u<VAR>l : List α<GOAL>List.map l.get (List.finRange l.length) = l
<VAR>n i : ℕ<VAR>h : i < (List.finRange n).length<GOAL>(List.finRange n).nthLe i h = ⟨i, ⋯⟩
<VAR>k : ℕ<VAR>i : Fin k<GOAL>List.indexOf i (List.finRange k) = ↑i
<VAR>l : List ℕ<GOAL>List.Pairwise List.Disjoint l.ranges
<VAR>l : List ℕ<GOAL>List.map List.length l.ranges = l
<VAR>l : List ℕ<GOAL>l.ranges.join = List.range (Nat.sum l)
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>(∃ s ∈ l.ranges, n ∈ s) ↔ n < Nat.sum l
<VAR>l s : List ℕ<VAR>hs : s ∈ l.ranges<GOAL>s.Nodup
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>hx : x ∉ l<GOAL>Set.InjOn (fun k => List.insertNth k x l) {n | n ≤ l.length}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → α → α<VAR>g : γ → α → α<VAR>hfg : Set.range f ⊆ Set.range g<VAR>a : α<GOAL>Set.range (List.foldr f a) ⊆ Set.range (List.foldr g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → α<VAR>g : α → γ → α<VAR>hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b<VAR>a : α<GOAL>Set.range (List.foldl f a) ⊆ Set.range (List.foldl g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → α → α<VAR>g : γ → α → α<VAR>hfg : Set.range f = Set.range g<VAR>a : α<GOAL>Set.range (List.foldr f a) = Set.range (List.foldr g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → α<VAR>g : α → γ → α<VAR>hfg : (Set.range fun a c => f c a) = Set.range fun b c => g c b<VAR>a : α<GOAL>Set.range (List.foldl f a) = Set.range (List.foldl g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>f : α → σ → σ × β<VAR>as : List α<VAR>s : σ<GOAL>List.mapAccumr f as s = List.foldr (fun a s => let r := f a s.1; (r.1, r.2 :: s.2)) (s, []) as
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>φ : Type u_5<VAR>f : α → β → σ → σ × φ<VAR>as : List α<VAR>bs : List β<VAR>s : σ<GOAL>List.mapAccumr₂ f as bs s = List.foldr (fun ab s => let r := f ab.1 ab.2 s.1; (r.1, r.2 :: s.2)) (s, []) (as.zip bs)
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : x ∈ l<GOAL>List.Duplicate x (x :: l)
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : List.Duplicate x l<VAR>y : α<GOAL>List.Duplicate x (y :: l)
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : List.Duplicate x l<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : List.Duplicate x (x :: l)<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<GOAL>List.Duplicate x (x :: l) ↔ x ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : List.Duplicate x l<GOAL>l ≠ []
<VAR>α : Type u_1<VAR>x : α<GOAL>¬List.Duplicate x []
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : List.Duplicate x l<VAR>y : α<GOAL>l ≠ [y]
<VAR>α : Type u_1<VAR>x y : α<GOAL>¬List.Duplicate x [y]
<VAR>α : Type u_1<VAR>x : α<VAR>h : List.Duplicate x []<GOAL>False
<VAR>α : Type u_1<VAR>x y : α<VAR>h : List.Duplicate x [y]<GOAL>False
<VAR>α : Type u_1<VAR>l : List α<VAR>x y : α<GOAL>List.Duplicate x (y :: l) ↔ y = x ∧ x ∈ l ∨ List.Duplicate x l
<VAR>α : Type u_1<VAR>l : List α<VAR>x y : α<VAR>h : List.Duplicate x (y :: l)<VAR>hx : x ≠ y<GOAL>List.Duplicate x l
<VAR>α : Type u_1<VAR>l : List α<VAR>x y : α<VAR>hne : x ≠ y<GOAL>List.Duplicate x (y :: l) ↔ List.Duplicate x l
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>l' : List α<VAR>hx : List.Duplicate x l<VAR>h : l.Sublist l'<GOAL>List.Duplicate x l'
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<GOAL>List.Duplicate x l ↔ [x, x].Sublist l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (x : α), ¬List.Duplicate x l
<VAR>α : Type u_1<VAR>l : List α<GOAL>(∃ x, List.Duplicate x l) ↔ ¬l.Nodup
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>h : List.Duplicate x l<GOAL>¬l.Nodup
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>DecidableEq α<GOAL>List.Duplicate x l ↔ 2 ≤ List.count x l
<VAR>a b : ℤ<GOAL>Finset.Icc a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding a)) (Finset.range (b + 1 - a).toNat)
<VAR>a b : ℤ<GOAL>Finset.Ico a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding a)) (Finset.range (b - a).toNat)
<VAR>a b : ℤ<GOAL>Finset.Ioc a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (Finset.range (b - a).toNat)
<VAR>a b : ℤ<GOAL>Finset.Ioo a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (Finset.range (b - a - 1).toNat)
<VAR>a b : ℤ<GOAL>Finset.uIcc a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (min a b))) (Finset.range (max a b + 1 - min a b).toNat)
<VAR>a b : ℤ<GOAL>(Finset.Icc a b).card = (b + 1 - a).toNat
<VAR>a b : ℤ<GOAL>(Finset.Ico a b).card = (b - a).toNat
<VAR>a b : ℤ<GOAL>(Finset.Ioc a b).card = (b - a).toNat
<VAR>a b : ℤ<GOAL>(Finset.Ioo a b).card = (b - a - 1).toNat
<VAR>a b : ℤ<GOAL>(Finset.uIcc a b).card = (b - a).natAbs + 1
<VAR>a b : ℤ<VAR>h : a ≤ b + 1<GOAL>↑(Finset.Icc a b).card = b + 1 - a
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>↑(Finset.Ico a b).card = b - a
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>↑(Finset.Ioc a b).card = b - a
<VAR>a b : ℤ<VAR>h : a < b<GOAL>↑(Finset.Ioo a b).card = b - a - 1
<VAR>n a : ℤ<VAR>h : 0 ≤ a<GOAL>Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.Ico 0 a
<VAR>n : ℤ<VAR>a : ℤ<GOAL>a ≡ a [ZMOD n]
<VAR>n a : ℤ<GOAL>a ≡ a [ZMOD n]
<VAR>n a b : ℤ<GOAL>a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
<VAR>n a b c : ℤ<GOAL>a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]
<VAR>n a b : ℤ<GOAL>a ≡ b [ZMOD n] → a % n = b % n
<VAR>n a b : ℤ<GOAL>a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]
<VAR>a b n : ℕ<GOAL>↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
<VAR>n a : ℤ<GOAL>a ≡ 0 [ZMOD n] ↔ n ∣ a
<VAR>n a : ℤ<VAR>h : n ∣ a<GOAL>a ≡ 0 [ZMOD n]
<VAR>n a : ℤ<VAR>h : n ∣ a<GOAL>0 ≡ a [ZMOD n]
<VAR>n a b : ℤ<GOAL>a ≡ b [ZMOD n] ↔ n ∣ b - a
<VAR>a b n : ℤ<GOAL>a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
<VAR>a n : ℤ<GOAL>a % n ≡ a [ZMOD n]
<VAR>n a b : ℤ<GOAL>-a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
<VAR>n a b : ℤ<GOAL>a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
<VAR>m n a b : ℤ<VAR>d : m ∣ n<VAR>h : a ≡ b [ZMOD n]<GOAL>a ≡ b [ZMOD m]
<VAR>n a b c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>c * a ≡ c * b [ZMOD c * n]
<VAR>n a b c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>a * c ≡ b * c [ZMOD n * c]
<VAR>n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>a + c ≡ b + d [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>c + a ≡ c + b [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>a + c ≡ b + c [ZMOD n]
<VAR>n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : a + c ≡ b + d [ZMOD n]<GOAL>c ≡ d [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : c + a ≡ c + b [ZMOD n]<GOAL>a ≡ b [ZMOD n]
<VAR>n a b c d : ℤ<VAR>h₁ : c ≡ d [ZMOD n]<VAR>h₂ : a + c ≡ b + d [ZMOD n]<GOAL>a ≡ b [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a + c ≡ b + c [ZMOD n]<GOAL>a ≡ b [ZMOD n]
<VAR>n a b : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>-a ≡ -b [ZMOD n]
<VAR>n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>a - c ≡ b - d [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>c - a ≡ c - b [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>a - c ≡ b - c [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>c * a ≡ c * b [ZMOD n]
<VAR>n a b : ℤ<VAR>c : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>a * c ≡ b * c [ZMOD n]
<VAR>n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>a * c ≡ b * d [ZMOD n]
<VAR>n a b : ℤ<VAR>m : ℕ<VAR>h : a ≡ b [ZMOD n]<GOAL>a ^ m ≡ b ^ m [ZMOD n]
<VAR>n a b : ℤ<VAR>m : ℤ<VAR>h : a ≡ b [ZMOD m * n]<GOAL>a ≡ b [ZMOD n]
<VAR>n a b : ℤ<VAR>m : ℤ<GOAL>a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n]
<VAR>m a b c : ℤ<VAR>hm : 0 < m<VAR>h : a * c ≡ b * c [ZMOD m]<GOAL>a ≡ b [ZMOD m / ↑(m.gcd c)]
<VAR>m a b c : ℤ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [ZMOD m]<GOAL>a ≡ b [ZMOD m / ↑(m.gcd c)]
<VAR>m a b c : ℤ<VAR>h : a / c ≡ b / c [ZMOD m / c]<VAR>ha : c ∣ a<GOAL>c ∣ b → c ∣ m → a ≡ b [ZMOD m]
<VAR>a b : ℤ<GOAL>a ≡ b [ZMOD 1]
<VAR>a b : ℤ<GOAL>a ≡ b [ZMOD a - b]
<VAR>a b : ℤ<GOAL>a ≡ b [ZMOD 0] ↔ a = b
<VAR>n a : ℤ<GOAL>n + a ≡ a [ZMOD n]
<VAR>n a : ℤ<GOAL>a + n ≡ a [ZMOD n]
<VAR>a b m n : ℤ<VAR>hmn : m.natAbs.Coprime n.natAbs<GOAL>a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]
<VAR>a b : ℕ<GOAL>↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]
<VAR>a b n : ℤ<VAR>c : ℤ<VAR>ha : a ≡ b [ZMOD n]<GOAL>a + n * c ≡ b [ZMOD n]
<VAR>a b n : ℤ<VAR>c : ℤ<VAR>ha : a ≡ b [ZMOD n]<GOAL>a - n * c ≡ b [ZMOD n]
<VAR>a t n : ℤ<GOAL>a + n * t ≡ a [ZMOD n]
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>∃ y, ↑a * y ≡ 1 [ZMOD ↑b]
<VAR>a : ℤ<VAR>b : ℤ<VAR>hb : 0 < b<GOAL>∃ z, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]
<VAR>a : ℤ<VAR>b : ℤ<VAR>hb : 0 < b<GOAL>∃ z, ↑z < b ∧ ↑z ≡ a [ZMOD b]
<VAR>a b c : ℤ<GOAL>a % (b * c) % b = a % b
<VAR>a b c : ℤ<GOAL>a % (b * c) % c = a % c
<VAR>α : Type u<VAR>l : List α<VAR>d : α<VAR>n : ℕ<VAR>hn : n < l.length<GOAL>l.getD n d = l.get ⟨n, hn⟩
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>d : α<VAR>n : ℕ<VAR>f : α → β<GOAL>(List.map f l).getD n (f d) = f (l.getD n d)
<VAR>α : Type u<VAR>l : List α<VAR>d : α<VAR>n : ℕ<VAR>hn : l.length ≤ n<GOAL>l.getD n d = d
<VAR>α : Type u<VAR>d : α<VAR>n : ℕ<GOAL>[d][n]?.getD d = d
<VAR>α : Type u<VAR>d : α<VAR>r n : ℕ<GOAL>(List.replicate r d)[n]?.getD d = d
<VAR>α : Type u<VAR>l l' : List α<VAR>d : α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>(l ++ l').getD n d = l.getD n d
<VAR>α : Type u<VAR>l l' : List α<VAR>d : α<VAR>n : ℕ<VAR>h : l.length ≤ n<GOAL>(l ++ l').getD n d = l'.getD (n - l.length) d
<VAR>α : Type u<VAR>l : List α<VAR>d : α<VAR>n : ℕ<GOAL>l.getD n d = (l.get? n).getD d
<VAR>α : Type u<VAR>n : ℕ<VAR>Inhabited α<GOAL>[].getI n = default
<VAR>α : Type u<VAR>x : α<VAR>xs : List α<VAR>Inhabited α<GOAL>(x :: xs).getI 0 = x
<VAR>α : Type u<VAR>x : α<VAR>xs : List α<VAR>n : ℕ<VAR>Inhabited α<GOAL>(x :: xs).getI (n + 1) = xs.getI n
<VAR>α : Type u<VAR>l : List α<VAR>Inhabited α<VAR>n : ℕ<VAR>hn : n < l.length<GOAL>l.getI n = l.get ⟨n, hn⟩
<VAR>α : Type u<VAR>l : List α<VAR>Inhabited α<VAR>n : ℕ<VAR>hn : l.length ≤ n<GOAL>l.getI n = default
<VAR>α : Type u<VAR>l : List α<VAR>Inhabited α<VAR>n : ℕ<GOAL>l.getD n default = l.getI n
<VAR>α : Type u<VAR>Inhabited α<VAR>l l' : List α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>(l ++ l').getI n = l.getI n
<VAR>α : Type u<VAR>Inhabited α<VAR>l l' : List α<VAR>n : ℕ<VAR>h : l.length ≤ n<GOAL>(l ++ l').getI n = l'.getI (n - l.length)
<VAR>α : Type u<VAR>l : List α<VAR>Inhabited α<VAR>n : ℕ<GOAL>l.getI n = (l.get? n).iget
<VAR>α : Type u<VAR>l : List α<VAR>Inhabited α<GOAL>l.getI 0 = l.headI
<VAR>α : Type u<VAR>β : α → Type v<VAR>self : AList β<GOAL>self.entries.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>s t : AList β<GOAL>s.entries = t.entries → s = t
<VAR>α : Type u<VAR>β : α → Type v<VAR>s t : AList β<GOAL>s = t ↔ s.entries = t.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>s : AList β<GOAL>s.keys.Nodup
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>s : AList β<GOAL>a ∈ s ↔ a ∈ s.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>s₁ s₂ : AList β<VAR>p : s₁.entries ~ s₂.entries<GOAL>a ∈ s₁ ↔ a ∈ s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<GOAL>a ∉ ∅
<VAR>α : Type u<VAR>β : α → Type v<GOAL>∅.entries = []
<VAR>α : Type u<VAR>β : α → Type v<GOAL>∅.keys = []
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>b : β a<GOAL>(AList.singleton a b).entries = [⟨a, b⟩]
<VAR>α : Type u<VAR>β : α → Type v<VAR>a : α<VAR>b : β a<GOAL>(AList.singleton a b).keys = [a]
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<GOAL>AList.lookup a ∅ = none
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>(AList.lookup a s).isSome = true ↔ a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>AList.lookup a s = none ↔ a ∉ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>b ∈ AList.lookup a s ↔ ⟨a, b⟩ ∈ s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : AList β<VAR>p : s₁.entries ~ s₂.entries<GOAL>AList.lookup a s₁ = AList.lookup a s₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>s₁ s₂ : AList β<VAR>h : s₁.entries ⊆ s₂.entries<GOAL>s₁.keys ⊆ s₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>(AList.replace a b s).keys = s.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>s : AList β<GOAL>a' ∈ AList.replace a b s ↔ a' ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<GOAL>s₁.entries ~ s₂.entries → (AList.replace a b s₁).entries ~ (AList.replace a b s₂).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>(AList.erase a s).keys = s.keys.erase a
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>s : AList β<GOAL>a' ∈ AList.erase a s ↔ a' ≠ a ∧ a' ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s₁ s₂ : AList β<GOAL>s₁.entries ~ s₂.entries → (AList.erase a s₁).entries ~ (AList.erase a s₂).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : AList β<GOAL>AList.lookup a (AList.erase a s) = none
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>s : AList β<VAR>h : a ≠ a'<GOAL>AList.lookup a (AList.erase a' s) = AList.lookup a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>s : AList β<GOAL>AList.erase a' (AList.erase a s) = AList.erase a (AList.erase a' s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>(AList.insert a b s).entries = ⟨a, b⟩ :: List.kerase a s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<VAR>h : a ∉ s<GOAL>(AList.insert a b s).entries = ⟨a, b⟩ :: s.entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<VAR>h : a ∉ s<GOAL>AList.insert a b s = { entries := ⟨a, b⟩ :: s.entries, nodupKeys := ⋯ }
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<GOAL>AList.insert a b ∅ = AList.singleton a b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b' : β a'<VAR>s : AList β<GOAL>a ∈ AList.insert a' b' s ↔ a = a' ∨ a ∈ s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>(AList.insert a b s).keys = a :: s.keys.erase a
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s₁ s₂ : AList β<VAR>p : s₁.entries ~ s₂.entries<GOAL>(AList.insert a b s₁).entries ~ (AList.insert a b s₂).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>AList.lookup a (AList.insert a b s) = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b' : β a'<VAR>s : AList β<VAR>h : a ≠ a'<GOAL>AList.lookup a (AList.insert a' b' s) = AList.lookup a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : AList β<VAR>k k' : α<VAR>v : β k<GOAL>AList.lookup k' (AList.insert k v l) = none ↔ k' ≠ k ∧ AList.lookup k' l = none
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>s : List (Sigma β)<GOAL>AList.lookup a s.toAList = List.dlookup a s
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b b' : β a<VAR>s : AList β<GOAL>AList.insert a b' (AList.insert a b s) = AList.insert a b' s