ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑n / x) ↔ n ≠ 0 ∧ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x
<VAR>x y : ℝ<VAR>h : x < y<GOAL>∃ r, Irrational r ∧ x < r ∧ r < y
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x y : α<GOAL>Quotient.mk' x = Quotient.mk' y ↔ r.Rel x y
<VAR>α : Type u_1<VAR>r s : Setoid α<VAR>H : ∀ (a b : α), r.Rel a b ↔ s.Rel a b<GOAL>r = s
<VAR>α : Type u_1<VAR>r s : Setoid α<GOAL>r = s ↔ ∀ (a b : α), r.Rel a b ↔ s.Rel a b
<VAR>α : Type u_1<VAR>r₁ r₂ : Setoid α<GOAL>r₁ = r₂ ↔ r₁.Rel = r₂.Rel
<VAR>α : Type u_1<VAR>r s : Setoid α<GOAL>r ≤ s ↔ ∀ {x y : α}, r.Rel x y → s.Rel x y
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x : α<GOAL>r.Rel x x
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x y : α<GOAL>r.Rel x y → r.Rel y x
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>x y z : α<GOAL>r.Rel x y → r.Rel y z → r.Rel x z
<VAR>α : Type u_1<VAR>s : Setoid α<VAR>x y : α<GOAL>s.Rel x y ↔ s.Rel y x
<VAR>α : Type u_1<VAR>r : Setoid α<GOAL>Setoid.ker Quotient.mk'' = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>f ⟦a⟧.out = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>f ⟦a⟧.out' = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x y : α<GOAL>(Setoid.ker f).Rel x y ↔ f x = f y
<VAR>α : Type u_1<VAR>r s : Setoid α<GOAL>(r ⊓ s).Rel = r.Rel ⊓ s.Rel
<VAR>α : Type u_1<VAR>r s : Setoid α<VAR>x y : α<GOAL>(r ⊓ s).Rel x y ↔ r.Rel x y ∧ s.Rel x y
<VAR>α : Type u_1<VAR>s : Set (Setoid α)<GOAL>(sInf s).Rel = sInf (Setoid.Rel '' s)
<VAR>α : Type u_1<GOAL>⊤.Rel = ⊤
<VAR>α : Type u_1<GOAL>⊥.Rel = fun x x_1 => x = x_1
<VAR>α : Type u_1<VAR>s : Setoid α<GOAL>s = ⊤ ↔ ∀ (x y : α), s.Rel x y
<VAR>α : Type u_1<VAR>S : Set (Setoid α)<VAR>x y : α<GOAL>x ≈ y ↔ ∀ s ∈ S, s.Rel x y
<VAR>α : Type u_1<VAR>S : Set (Setoid α)<VAR>x y : α<GOAL>⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, s.Rel x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>EqvGen.Setoid r = sInf {s | ∀ ⦃x y : α⦄, r x y → s.Rel x y}
<VAR>α : Type u_1<VAR>r s : Setoid α<GOAL>r ⊔ s = EqvGen.Setoid fun x y => r.Rel x y ∨ s.Rel x y
<VAR>α : Type u_1<VAR>r s : Setoid α<GOAL>r ⊔ s = EqvGen.Setoid (r.Rel ⊔ s.Rel)
<VAR>α : Type u_1<VAR>S : Set (Setoid α)<GOAL>sSup S = EqvGen.Setoid fun x y => ∃ r ∈ S, r.Rel x y
<VAR>α : Type u_1<VAR>s : Set (Setoid α)<GOAL>sSup s = EqvGen.Setoid (sSup (Setoid.Rel '' s))
<VAR>α : Type u_1<VAR>r : Setoid α<GOAL>EqvGen.Setoid Setoid.r = r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>EqvGen.Setoid (EqvGen.Setoid r).Rel = EqvGen.Setoid r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Setoid α<VAR>h : ∀ (x y : α), r x y → s.Rel x y<GOAL>EqvGen.Setoid r ≤ s
<VAR>α : Type u_1<VAR>r s : α → α → Prop<VAR>h : ∀ (x y : α), r x y → s x y<GOAL>EqvGen.Setoid r ≤ EqvGen.Setoid s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Injective f ↔ Setoid.ker f = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x y : α<GOAL>(Setoid.ker f).Rel x y ↔ x ∈ f ⁻¹' {f y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>H : r ≤ Setoid.ker f<VAR>g : Quotient r → β<VAR>Hg : f = g ∘ Quotient.mk''<GOAL>Quotient.lift f H = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Injective (Quotient.lift f ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>H : ∀ (x y : α), r.Rel x y → f x = f y<VAR>h : Function.Injective (Quotient.lift f H)<GOAL>Setoid.ker f = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>hf : Function.RightInverse g f<VAR>a : Quotient (Setoid.ker f)<GOAL>(Setoid.quotientKerEquivOfRightInverse f g hf) a = a.liftOn' f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>hf : Function.RightInverse g f<VAR>b : β<GOAL>(Setoid.quotientKerEquivOfRightInverse f g hf).symm b = Quotient.mk'' (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>h : Setoid.ker f ≤ r<VAR>hf : Function.Surjective f<GOAL>r.map f = r.mapOfSurjective f h hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : Setoid β<VAR>x y : α<GOAL>(Setoid.comap f r).Rel x y ↔ r.Rel (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : Setoid β<GOAL>Setoid.comap f r = Setoid.ker (Quotient.mk'' ∘ f)
<VAR>α : Type u_1<VAR>s : Setoid α<GOAL>Subsingleton (Quotient s) ↔ s = ⊤
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Subsingleton (Quot r) ↔ EqvGen r = ⊤
<VAR>k : ℕ<GOAL>Real.Wallis.W (k + 1) = Real.Wallis.W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
<VAR>k : ℕ<GOAL>0 < Real.Wallis.W k
<VAR>n : ℕ<GOAL>Real.Wallis.W n = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
<VAR>k : ℕ<GOAL>(π / 2)⁻¹ * Real.Wallis.W k = (∫ (x : ℝ) in 0 ..π, Real.sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0 ..π, Real.sin x ^ (2 * k)
<VAR>k : ℕ<GOAL>Real.Wallis.W k ≤ π / 2
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ Real.Wallis.W k
<GOAL>Filter.Tendsto Real.Wallis.W Filter.atTop (𝓝 (π / 2))
<GOAL>Filter.Tendsto (fun k => ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))) Filter.atTop (𝓝 (π / 2))
<VAR>n : ℕ<GOAL>φ ^ (n + 2) - φ ^ (n + 1) = φ ^ n
<VAR>β : Type u_2<VAR>CommRing β<GOAL>fibRec.charPoly = Polynomial.X ^ 2 - (Polynomial.X + 1)
<VAR>α : Type u_1<VAR>CommSemiring α<GOAL>fibRec.IsSolution fun x => ↑(Nat.fib x)
<VAR>n : ℕ<GOAL>↑(Nat.fib n) = (φ ^ n - ψ ^ n) / √5
<VAR>c : ℝ<VAR>f : ℕ → Bool<VAR>n : ℕ<VAR>h : f n = true<GOAL>Cardinal.cantorFunctionAux c f n = c ^ n
<VAR>c : ℝ<VAR>f : ℕ → Bool<VAR>n : ℕ<VAR>h : f n = false<GOAL>Cardinal.cantorFunctionAux c f n = 0
<VAR>c : ℝ<VAR>f : ℕ → Bool<VAR>n : ℕ<VAR>h : 0 ≤ c<GOAL>0 ≤ Cardinal.cantorFunctionAux c f n
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>h : f n = g n<GOAL>Cardinal.cantorFunctionAux c f n = Cardinal.cantorFunctionAux c g n
<VAR>c : ℝ<VAR>f : ℕ → Bool<GOAL>Cardinal.cantorFunctionAux c f 0 = bif f 0 then 1 else 0
<VAR>c : ℝ<VAR>f : ℕ → Bool<GOAL>(fun n => Cardinal.cantorFunctionAux c f (n + 1)) = fun n => c * Cardinal.cantorFunctionAux c (fun n => f (n + 1)) n
<VAR>c : ℝ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>Summable (Cardinal.cantorFunctionAux c f)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<VAR>h3 : ∀ (n : ℕ), f n = true → g n = true<GOAL>Cardinal.cantorFunction c f ≤ Cardinal.cantorFunction c g
<VAR>c : ℝ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>Cardinal.cantorFunction c f = (bif f 0 then 1 else 0) + c * Cardinal.cantorFunction c fun n => f (n + 1)
<VAR>c : ℝ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<VAR>n : ℕ<VAR>f g : ℕ → Bool<VAR>hn : ∀ k < n, f k = g k<VAR>fn : f n = false<VAR>gn : g n = true<GOAL>Cardinal.cantorFunction c f < Cardinal.cantorFunction c g
<VAR>c : ℝ<VAR>h1 : 0 < c<VAR>h2 : c < 1 / 2<GOAL>Function.Injective (Cardinal.cantorFunction c)
<VAR>a : ℝ<GOAL>#↑(Set.Ioi a) = 𝔠
<VAR>a : ℝ<GOAL>#↑(Set.Ici a) = 𝔠
<VAR>a : ℝ<GOAL>#↑(Set.Iio a) = 𝔠
<VAR>a : ℝ<GOAL>#↑(Set.Iic a) = 𝔠
<VAR>a b : ℝ<VAR>h : a < b<GOAL>#↑(Set.Ioo a b) = 𝔠
<VAR>a b : ℝ<VAR>h : a < b<GOAL>#↑(Set.Ico a b) = 𝔠
<VAR>a b : ℝ<VAR>h : a < b<GOAL>#↑(Set.Icc a b) = 𝔠
<VAR>a b : ℝ<VAR>h : a < b<GOAL>#↑(Set.Ioc a b) = 𝔠
<VAR>b : ℕ<VAR>h : 2 ≤ b<GOAL>b.digitsAux h 0 = []
<VAR>b : ℕ<VAR>h : 2 ≤ b<VAR>n : ℕ<VAR>w : 0 < n<GOAL>b.digitsAux h n = n % b :: b.digitsAux h (n / b)
<VAR>b : ℕ<GOAL>b.digits 0 = []
<VAR>n : ℕ<GOAL>Nat.digits 0 n.succ = [n + 1]
<VAR>n : ℕ<GOAL>n ≠ 0 → Nat.digits 0 n = [n]
<VAR>n : ℕ<GOAL>Nat.digits 1 n = List.replicate n 1
<VAR>n : ℕ<GOAL>Nat.digits 1 (n + 1) = 1 :: Nat.digits 1 n
<VAR>b n : ℕ<GOAL>(b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
<VAR>b : ℕ<GOAL>1 < b → ∀ {n : ℕ}, 0 < n → b.digits n = n % b :: b.digits (n / b)
<VAR>b x : ℕ<VAR>hx : x ≠ 0<VAR>hxb : x < b<GOAL>b.digits x = [x]
<VAR>b : ℕ<VAR>h : 1 < b<VAR>x y : ℕ<VAR>hxb : x < b<VAR>hxy : x ≠ 0 ∨ y ≠ 0<GOAL>b.digits (x + b * y) = x :: b.digits y
<VAR>α : Type u_1<VAR>Semiring α<VAR>b : α<VAR>L : List ℕ<GOAL>Nat.ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
<VAR>b : ℕ<VAR>l : List ℕ<GOAL>(List.zipWith (fun i a => a * b ^ (i + 1)) (List.range l.length) l).sum = b * (List.zipWith (fun i a => a * b ^ i) (List.range l.length) l).sum
<VAR>b : ℕ<VAR>L : List ℕ<GOAL>Nat.ofDigits b L = (List.mapIdx (fun i a => a * b ^ i) L).sum
<VAR>b : ℕ<GOAL>Nat.ofDigits b [] = 0
<VAR>b n : ℕ<GOAL>Nat.ofDigits b [n] = n
<VAR>α : Type u_1<VAR>Semiring α<VAR>h : ℕ<VAR>L : List ℕ<GOAL>Nat.ofDigits 1 (h :: L) = ↑h + Nat.ofDigits 1 L
<VAR>b hd : ℕ<VAR>tl : List ℕ<GOAL>Nat.ofDigits b (hd :: tl) = hd + b * Nat.ofDigits b tl
<VAR>b : ℕ<VAR>l1 l2 : List ℕ<GOAL>Nat.ofDigits b (l1 ++ l2) = Nat.ofDigits b l1 + b ^ l1.length * Nat.ofDigits b l2
<VAR>α : Type u_1<VAR>Semiring α<VAR>b : ℕ<VAR>L : List ℕ<GOAL>↑(Nat.ofDigits b L) = Nat.ofDigits (↑b) L
<VAR>b : ℕ<VAR>L : List ℕ<GOAL>↑(Nat.ofDigits b L) = Nat.ofDigits (↑b) L
<VAR>b : ℕ<VAR>h : b ≠ 0<VAR>L : List ℕ<GOAL>Nat.ofDigits b L = 0 → ∀ l ∈ L, l = 0
<VAR>b : ℕ<VAR>h : 1 < b<VAR>L : List ℕ<VAR>w₁ : ∀ l ∈ L, l < b<VAR>w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0<GOAL>b.digits (Nat.ofDigits b L) = L
<VAR>b n : ℕ<GOAL>Nat.ofDigits b (b.digits n) = n
<VAR>L : List ℕ<GOAL>Nat.ofDigits 1 L = L.sum
<VAR>b n : ℕ<GOAL>b.digits n = [] ↔ n = 0
<VAR>b n : ℕ<GOAL>b.digits n ≠ [] ↔ n ≠ 0
<VAR>b n : ℕ<VAR>h : 1 < b<VAR>w : n ≠ 0<GOAL>b.digits n = n % b :: b.digits (n / b)
<VAR>b : ℕ<VAR>m : ℕ<VAR>h : 1 < b<VAR>p : b.digits m ≠ []<VAR>q : b.digits (m / b) ≠ []<GOAL>(b.digits m).getLast p = (b.digits (m / b)).getLast q
<VAR>b : ℕ<GOAL>Function.Injective b.digits
<VAR>b n m : ℕ<GOAL>b.digits n = b.digits m ↔ n = m
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : n ≠ 0<GOAL>(b.digits n).length = Nat.log b n + 1
<VAR>b : ℕ<VAR>m : ℕ<VAR>hm : m ≠ 0<GOAL>(b.digits m).getLast ⋯ ≠ 0
<VAR>n : ℕ<VAR>b : ℕ<VAR>l : List ℕ<GOAL>n * Nat.ofDigits b l = Nat.ofDigits b (List.map (fun x => n * x) l)
<VAR>b : ℕ<VAR>l1 l2 : List ℕ<VAR>h : l1.length = l2.length<GOAL>Nat.ofDigits b l1 + Nat.ofDigits b l2 = Nat.ofDigits b (List.zipWith (fun x x_1 => x + x_1) l1 l2)
<VAR>b m d : ℕ<GOAL>d ∈ (b + 2).digits m → d < b + 2
<VAR>b m d : ℕ<VAR>hb : 1 < b<VAR>hd : d ∈ b.digits m<GOAL>d < b
<VAR>b : ℕ<VAR>l : List ℕ<VAR>hl : ∀ x ∈ l, x < b + 2<GOAL>Nat.ofDigits (b + 2) l < (b + 2) ^ l.length
<VAR>b : ℕ<VAR>l : List ℕ<VAR>hb : 1 < b<VAR>hl : ∀ x ∈ l, x < b<GOAL>Nat.ofDigits b l < b ^ l.length
<VAR>b m : ℕ<GOAL>m < (b + 2) ^ ((b + 2).digits m).length
<VAR>b m : ℕ<VAR>hb : 1 < b<GOAL>m < b ^ (b.digits m).length
<VAR>b m n : ℕ<GOAL>Nat.ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
<VAR>b m n : ℕ<VAR>hb : 0 < b<GOAL>b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
<VAR>b n : ℕ<GOAL>(b.digits n).length ≤ (b.digits (n + 1)).length
<VAR>b n m : ℕ<VAR>h : n ≤ m<GOAL>(b.digits n).length ≤ (b.digits m).length
<VAR>p q : ℕ<VAR>L : List ℕ<VAR>h : p ≤ q<GOAL>Nat.ofDigits p L ≤ Nat.ofDigits q L
<VAR>p : ℕ<VAR>L : List ℕ<VAR>h : 1 ≤ p<GOAL>L.sum ≤ Nat.ofDigits p L
<VAR>p n : ℕ<GOAL>(p.digits n).sum ≤ n
<VAR>b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<GOAL>(b + 2) ^ l.length ≤ (b + 2) * Nat.ofDigits (b + 2) l
<VAR>b m : ℕ<VAR>hm : m ≠ 0<GOAL>(b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
<VAR>b m : ℕ<VAR>hb : 1 < b<GOAL>m ≠ 0 → b ^ (b.digits m).length ≤ b * m
<VAR>p : ℕ<VAR>hpos : 0 < p<VAR>digits : List ℕ<VAR>w₁ : ∀ l ∈ digits, l < p<GOAL>Nat.ofDigits p digits / p = Nat.ofDigits p digits.tail
<VAR>p : ℕ<VAR>i : ℕ<VAR>hpos : 0 < p<VAR>digits : List ℕ<VAR>w₁ : ∀ l ∈ digits, l < p<GOAL>Nat.ofDigits p digits / p ^ i = Nat.ofDigits p (List.drop i digits)
<VAR>p : ℕ<VAR>i n : ℕ<VAR>h : 2 ≤ p<GOAL>n / p ^ i = Nat.ofDigits p (List.drop i (p.digits n))
<VAR>p : ℕ<VAR>L : List ℕ<VAR>h_nonempty : L ≠ []<VAR>h_ne_zero : L.getLast h_nonempty ≠ 0<VAR>h_lt : ∀ l ∈ L, l < p<GOAL>(p - 1) * ∑ i ∈ Finset.range L.length, Nat.ofDigits p L / p ^ i.succ = Nat.ofDigits p L - L.sum
<VAR>p : ℕ<VAR>n : ℕ<GOAL>(p - 1) * ∑ i ∈ Finset.range (Nat.log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
<VAR>n : ℕ<GOAL>Nat.digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits
<VAR>α : Type u_1<VAR>CommRing α<VAR>a b k : α<VAR>h : k ∣ a - b<VAR>L : List ℕ<GOAL>k ∣ Nat.ofDigits a L - Nat.ofDigits b L
<VAR>b b' k : ℕ<VAR>h : b ≡ b' [MOD k]<VAR>L : List ℕ<GOAL>Nat.ofDigits b L ≡ Nat.ofDigits b' L [MOD k]
<VAR>b k : ℕ<VAR>L : List ℕ<GOAL>Nat.ofDigits b L ≡ Nat.ofDigits (b % k) L [MOD k]
<VAR>b k : ℕ<VAR>L : List ℕ<GOAL>Nat.ofDigits b L % k = Nat.ofDigits (b % k) L % k
<VAR>b : ℕ<VAR>l : List ℕ<GOAL>Nat.ofDigits b l % b = l.head! % b
<VAR>b n : ℕ<VAR>h : b ≠ 1<GOAL>(b.digits n).head! = n % b
<VAR>b b' : ℤ<VAR>k : ℕ<VAR>h : b ≡ b' [ZMOD ↑k]<VAR>L : List ℕ<GOAL>Nat.ofDigits b L ≡ Nat.ofDigits b' L [ZMOD ↑k]
<VAR>b : ℤ<VAR>k : ℕ<VAR>L : List ℕ<GOAL>Nat.ofDigits b L ≡ Nat.ofDigits (b % ↑k) L [ZMOD ↑k]
<VAR>b : ℤ<VAR>k : ℕ<VAR>L : List ℕ<GOAL>Nat.ofDigits b L % ↑k = Nat.ofDigits (b % ↑k) L % ↑k
<VAR>b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>n ≡ (b'.digits n).sum [MOD b]
<VAR>n : ℕ<GOAL>n ≡ (Nat.digits 10 n).sum [MOD 3]
<VAR>n : ℕ<GOAL>n ≡ (Nat.digits 10 n).sum [MOD 9]
<VAR>b b' : ℕ<VAR>c : ℤ<VAR>h : ↑b' ≡ c [ZMOD ↑b]<VAR>n : ℕ<GOAL>↑n ≡ Nat.ofDigits c (b'.digits n) [ZMOD ↑b]
<VAR>L : List ℕ<GOAL>Nat.ofDigits (-1) L = (List.map (fun n => ↑n) L).alternatingSum
<VAR>n : ℕ<GOAL>↑n ≡ (List.map (fun n => ↑n) (Nat.digits 10 n)).alternatingSum [ZMOD 11]
<VAR>b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>b ∣ n ↔ b ∣ (b'.digits n).sum
<VAR>n : ℕ<GOAL>3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum
<VAR>n : ℕ<GOAL>9 ∣ n ↔ 9 ∣ (Nat.digits 10 n).sum
<VAR>b b' : ℕ<VAR>c : ℤ<VAR>h : ↑b ∣ ↑b' - c<VAR>n : ℕ<GOAL>b ∣ n ↔ ↑b ∣ Nat.ofDigits c (b'.digits n)
<VAR>n : ℕ<GOAL>11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (Nat.digits 10 n)).alternatingSum
<VAR>n : ℕ<VAR>p : (Nat.digits 10 n).Palindrome<VAR>h : Even (Nat.digits 10 n).length<GOAL>11 ∣ n
<VAR>b f n : ℕ<VAR>l1 l2 : List Char<GOAL>l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
<VAR>b f n : ℕ<VAR>c : Char<VAR>tl : List Char<GOAL>(b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
<VAR>n b e : ℕ<VAR>h_b_pos : 0 < b<GOAL>n < b ^ e.succ → n / b < b ^ e
<VAR>b : ℕ<VAR>h : 2 ≤ b<VAR>f n e : ℕ<VAR>hlt : n < b ^ e<VAR>h_e_pos : 0 < e<GOAL>(b.toDigitsCore f n []).length ≤ e
<VAR>n e : ℕ<GOAL>0 < e → n < 10 ^ e → n.repr.length ≤ e
<VAR>b n m r : ℕ<VAR>l : List ℕ<VAR>e : r + b * m = n<VAR>hr : r < b<VAR>h : b.digits m = l ∧ 1 < b ∧ 0 < m<GOAL>b.digits n = r :: l ∧ 1 < b ∧ 0 < n
<VAR>b n : ℕ<VAR>n0 : 0 < n<VAR>nb : n < b<GOAL>b.digits n = [n] ∧ 1 < b ∧ 0 < n
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x ^ 2 = x
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt (x ^ 2) = x
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x * NNReal.sqrt x = x
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt (x * x) = x
<VAR>x y : ℝ≥0<GOAL>NNReal.sqrt x ≤ NNReal.sqrt y ↔ x ≤ y
<VAR>x y : ℝ≥0<GOAL>NNReal.sqrt x < NNReal.sqrt y ↔ x < y
<VAR>x y : ℝ≥0<GOAL>NNReal.sqrt x = y ↔ x = y ^ 2
<VAR>x y : ℝ≥0<GOAL>NNReal.sqrt x ≤ y ↔ x ≤ y ^ 2
<VAR>x y : ℝ≥0<GOAL>x ≤ NNReal.sqrt y ↔ x ^ 2 ≤ y
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x = 0 ↔ x = 0
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x = 1 ↔ x = 1
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x ≤ 1 ↔ x ≤ 1
<VAR>x : ℝ≥0<GOAL>1 ≤ NNReal.sqrt x ↔ 1 ≤ x
<VAR>x y : ℝ≥0<GOAL>NNReal.sqrt (x * y) = NNReal.sqrt x * NNReal.sqrt y
<VAR>x : ℝ≥0<GOAL>NNReal.sqrt x⁻¹ = (NNReal.sqrt x)⁻¹
<VAR>x y : ℝ≥0<GOAL>NNReal.sqrt (x / y) = NNReal.sqrt x / NNReal.sqrt y
<VAR>x : ℝ≥0<GOAL>0 < NNReal.sqrt x ↔ 0 < x
<VAR>x : ℝ≥0<GOAL>↑(NNReal.sqrt x) = √↑x
<VAR>x : ℝ<VAR>h : x ≤ 0<GOAL>√x = 0
<VAR>x : ℝ<GOAL>0 ≤ √x
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>√x * √x = x
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>√(x * x) = x
<VAR>x y : ℝ<GOAL>√x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>√x = y ↔ y * y = x
<VAR>x : ℝ<GOAL>√x = 1 ↔ x = 1
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>√x ^ 2 = x
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>√(x ^ 2) = x
<VAR>x : ℝ<GOAL>√(x * x) = |x|
<VAR>x : ℝ<GOAL>√(x ^ 2) = |x|
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>√x < √y ↔ x < y
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>h : x < y<GOAL>√x < √y
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>x ≤ √y ↔ x ^ 2 ≤ y
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>x ≤ √y ↔ x ^ 2 ≤ y
<VAR>x y : ℝ<VAR>h : 0 ≤ y<GOAL>x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y
<VAR>x y : ℝ<VAR>h : x ^ 2 ≤ y<GOAL>-√y ≤ x
<VAR>x y : ℝ<VAR>h : x ^ 2 ≤ y<GOAL>x ≤ √y
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>√x = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>√x = 0 ↔ x ≤ 0
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>√x ≠ 0 ↔ x ≠ 0
<VAR>x : ℝ<GOAL>√x ≠ 0 ↔ 0 < x
<VAR>x : ℝ<GOAL>0 < √x ↔ 0 < x
<VAR>x : ℝ<GOAL>1 ≤ √x ↔ 1 ≤ x
<VAR>x : ℝ<GOAL>√x ≤ 1 ↔ x ≤ 1
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>√(x * y) = √x * √y
<VAR>x : ℝ<VAR>y : ℝ<VAR>hy : 0 ≤ y<GOAL>√(x * y) = √x * √y
<VAR>x : ℝ<GOAL>√x⁻¹ = (√x)⁻¹
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>√(x / y) = √x / √y
<VAR>x : ℝ<VAR>y : ℝ<VAR>hy : 0 ≤ y<GOAL>√(x / y) = √x / √y
<VAR>x : ℝ<GOAL>x / √x = √x
<VAR>x : ℝ<GOAL>√x / x = 1 / √x
<VAR>x : ℝ<GOAL>√x / x = (√x)⁻¹
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>x < √y ↔ x ^ 2 < y
<VAR>x y : ℝ<GOAL>x ^ 2 < y ↔ -√y < x ∧ x < √y
<VAR>x y : ℝ<VAR>h : x ^ 2 < y<GOAL>-√y < x
<VAR>x y : ℝ<VAR>h : x ^ 2 < y<GOAL>x < √y
<VAR>x y : ℝ<VAR>h : √x < y<GOAL>x < y ^ 2
<VAR>a : ℕ<GOAL>↑a.sqrt ≤ √↑a
<VAR>a : ℕ<GOAL>√↑a < ↑a.sqrt + 1
<VAR>a : ℕ<GOAL>√↑a ≤ ↑a.sqrt + 1
<VAR>a : ℕ<GOAL>⌊√↑a⌋ = ↑a.sqrt
<VAR>a : ℕ<GOAL>⌊√↑a⌋₊ = a.sqrt
<VAR>x : ℝ<VAR>h : -1 ≤ x<GOAL>√(1 + x) ≤ 1 + x / 2
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>l : Filter α<VAR>x : ℝ<VAR>h : Filter.Tendsto f l (𝓝 x)<GOAL>Filter.Tendsto (fun x => √(f x)) l (𝓝 √x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (fun x => √(f x)) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>x : α<VAR>h : ContinuousAt f x<GOAL>ContinuousAt (fun x => √(f x)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => √(f x)) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>h : Continuous f<GOAL>Continuous fun x => √(f x)
<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<GOAL>∑ i ∈ s, f i * g i ≤ NNReal.sqrt (∑ i ∈ s, f i ^ 2) * NNReal.sqrt (∑ i ∈ s, g i ^ 2)
<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<GOAL>∑ i ∈ s, NNReal.sqrt (f i) * NNReal.sqrt (g i) ≤ NNReal.sqrt (∑ i ∈ s, f i) * NNReal.sqrt (∑ i ∈ s, g i)
<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → ℝ<GOAL>∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2)
<VAR>ι : Type u_2<VAR>f g : ι → ℝ<VAR>s : Finset ι<VAR>hf : ∀ (i : ι), 0 ≤ f i<VAR>hg : ∀ (i : ι), 0 ≤ g i<GOAL>∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)
<VAR>x y : ℝ<GOAL>↑x = ↑y ↔ x = y
<VAR>x y : ℝ<GOAL>↑x ≠ ↑y ↔ x ≠ y
<VAR>x : ℝ<GOAL>↑x = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>↑x = 1 ↔ x = 1
<VAR>x : ℝ<GOAL>↑x ≠ 0 ↔ x ≠ 0
<VAR>x : ℝ<GOAL>↑x ≠ 1 ↔ x ≠ 1
<VAR>x : ℝ<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>x y : ℝ<GOAL>↑(x * y) = ↑x * ↑y
<VAR>x y : ℝ<GOAL>↑(x / y) = ↑x / ↑y
<VAR>x y : ℝ<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>x : ℝ<GOAL>0 ≤ ↑x ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>0 < ↑x ↔ 0 < x
<VAR>x : ℝ<GOAL>↑|x| = |↑x|
<VAR>x y : ℝ<GOAL>↑(max x y) = max ↑x ↑y
<VAR>x y : ℝ<GOAL>↑(min x y) = min ↑x ↑y
<VAR>f g : ℕ → ℝ<GOAL>Hyperreal.ofSeq f < Hyperreal.ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n < g n
<GOAL>Hyperreal.omega⁻¹ = Hyperreal.epsilon
<GOAL>Hyperreal.epsilon⁻¹ = Hyperreal.omega
<VAR>f : ℕ → ℝ<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>r : ℝ<GOAL>0 < r → Hyperreal.ofSeq f < ↑r
<VAR>f : ℕ → ℝ<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>r : ℝ<GOAL>0 < r → -↑r < Hyperreal.ofSeq f
<VAR>f : ℕ → ℝ<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>r : ℝ<GOAL>r < 0 → ↑r < Hyperreal.ofSeq f
<VAR>x : ℝ<GOAL>0 < x → Hyperreal.epsilon < ↑x
<VAR>f : ℕ → ℝ<VAR>r : ℝ<GOAL>(Hyperreal.ofSeq f).IsSt r ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (𝓝 r)
<VAR>x : ℝ*<VAR>r : ℝ<GOAL>x.IsSt r ↔ Filter.Germ.Tendsto x (𝓝 r)
<VAR>f : ℕ → ℝ<VAR>r : ℝ<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 r)<GOAL>(Hyperreal.ofSeq f).IsSt r
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<GOAL>x.st = r
<VAR>x : ℝ*<VAR>r : ℝ<VAR>h : x.IsSt r<GOAL>¬x.Infinite
<VAR>x : ℝ*<GOAL>(∃ r, x.IsSt r) → ¬x.Infinite
<VAR>x : ℝ*<VAR>hi : x.Infinite<GOAL>x.st = 0
<VAR>x : ℝ*<VAR>hni : ¬x.Infinite<GOAL>x.IsSt (sSup {y | ↑y < x})
<VAR>x : ℝ*<VAR>hni : ¬x.Infinite<GOAL>∃ r, x.IsSt r
<VAR>x : ℝ*<GOAL>x.st = sSup {y | ↑y < x}
<VAR>x : ℝ*<GOAL>(∃ r, x.IsSt r) ↔ ¬x.Infinite
<VAR>x : ℝ*<GOAL>x.Infinite ↔ ¬∃ r, x.IsSt r
<VAR>x : ℝ*<VAR>hx : ∃ r, x.IsSt r<GOAL>x.IsSt x.st
<VAR>x : ℝ*<VAR>hx : ¬x.Infinite<GOAL>x.IsSt x.st
<VAR>x : ℝ*<VAR>hx : x.st ≠ 0<GOAL>x.IsSt x.st
<VAR>r : ℝ<GOAL>(↑r).IsSt r
<VAR>r : ℝ<GOAL>(↑r).st = r
<VAR>r s : ℝ<GOAL>(↑r).IsSt s → r = s
<VAR>r s : ℝ<GOAL>(↑r).IsSt s ↔ r = s
<VAR>r₁ r₂ s : ℝ<VAR>h1 : (↑r₁).IsSt s<VAR>h2 : (↑r₂).IsSt s<GOAL>r₁ = r₂
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<VAR>f : ℝ → ℝ<VAR>hf : ContinuousAt f r<GOAL>Hyperreal.IsSt (Filter.Germ.map f x) (f r)
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hxr : x.IsSt r<VAR>hys : y.IsSt s<VAR>f : ℝ → ℝ → ℝ<VAR>hf : ContinuousAt (Function.uncurry f) (r, s)<GOAL>Hyperreal.IsSt (Filter.Germ.map₂ f x y) (f r s)
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hxr : x.IsSt r<VAR>hys : y.IsSt s<GOAL>(x + y).IsSt (r + s)
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<GOAL>(-x).IsSt (-r)
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hxr : x.IsSt r<VAR>hys : y.IsSt s<GOAL>(x - y).IsSt (r - s)
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hrx : x.IsSt r<VAR>hsy : y.IsSt s<VAR>hxy : x ≤ y<GOAL>r ≤ s
<VAR>x y : ℝ*<VAR>hix : ¬x.Infinite<VAR>hiy : ¬y.Infinite<GOAL>x ≤ y → x.st ≤ y.st
<VAR>x y : ℝ*<VAR>hix : ¬x.Infinite<VAR>hiy : ¬y.Infinite<GOAL>x.st < y.st → x < y
<VAR>x : ℝ*<GOAL>x.InfinitePos ↔ ∀ (r : ℝ), ↑r < x
<VAR>x : ℝ*<GOAL>x.InfiniteNeg ↔ ∀ (r : ℝ), x < ↑r
<VAR>x : ℝ*<VAR>hip : x.InfinitePos<GOAL>0 < x
<VAR>x : ℝ*<GOAL>x.InfiniteNeg → x < 0
<VAR>x : ℝ*<VAR>hI : x.Infinite<GOAL>x ≠ 0
<VAR>x : ℝ*<GOAL>x.InfiniteNeg → ¬x.InfinitePos
<VAR>x : ℝ*<VAR>hp : x.InfinitePos<GOAL>¬x.InfiniteNeg
<VAR>x : ℝ*<GOAL>x.InfinitePos → (-x).InfiniteNeg
<VAR>x : ℝ*<GOAL>x.InfiniteNeg → (-x).InfinitePos
<VAR>x : ℝ*<GOAL>(-x).InfiniteNeg ↔ x.InfinitePos
<VAR>x : ℝ*<GOAL>(-x).InfinitePos ↔ x.InfiniteNeg
<VAR>x : ℝ*<GOAL>(-x).Infinite ↔ x.Infinite
<VAR>x : ℝ*<VAR>h : x.Infinitesimal<GOAL>¬x.Infinite
<VAR>x : ℝ*<VAR>h : x.Infinite<GOAL>¬x.Infinitesimal
<VAR>x : ℝ*<VAR>h : x.InfinitePos<GOAL>¬x.Infinitesimal
<VAR>x : ℝ*<VAR>h : x.InfiniteNeg<GOAL>¬x.Infinitesimal
<VAR>x : ℝ*<GOAL>x.InfinitePos ↔ x.Infinite ∧ 0 < x
<VAR>x : ℝ*<GOAL>x.InfiniteNeg ↔ x.Infinite ∧ x < 0
<VAR>x : ℝ*<VAR>hp : 0 ≤ x<GOAL>x.InfinitePos ↔ x.Infinite
<VAR>x : ℝ*<VAR>hp : 0 < x<GOAL>x.InfinitePos ↔ x.Infinite
<VAR>x : ℝ*<VAR>hn : x < 0<GOAL>x.InfiniteNeg ↔ x.Infinite
<VAR>x : ℝ*<GOAL>|x|.InfinitePos ↔ |x|.Infinite
<VAR>x : ℝ*<GOAL>|x|.InfinitePos ↔ x.Infinite
<VAR>x : ℝ*<GOAL>x.Infinite ↔ ∀ (r : ℝ), |↑r| < |x|
<VAR>x y : ℝ*<GOAL>x.InfinitePos → ¬y.InfiniteNeg → (x + y).InfinitePos
<VAR>x y : ℝ*<GOAL>¬x.InfiniteNeg → y.InfinitePos → (x + y).InfinitePos
<VAR>x y : ℝ*<GOAL>¬x.InfinitePos → y.InfiniteNeg → (x + y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.InfinitePos → y.InfinitePos → (x + y).InfinitePos
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → y.InfiniteNeg → (x + y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>x.InfinitePos → ¬y.Infinite → (x + y).InfinitePos
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → ¬y.Infinite → (x + y).InfiniteNeg
<VAR>f : ℕ → ℝ<VAR>hf : Filter.Tendsto f Filter.atTop Filter.atTop<GOAL>(Hyperreal.ofSeq f).InfinitePos
<VAR>f : ℕ → ℝ<VAR>hf : Filter.Tendsto f Filter.atTop Filter.atBot<GOAL>(Hyperreal.ofSeq f).InfiniteNeg
<VAR>x : ℝ*<GOAL>¬x.Infinite → ¬(-x).Infinite
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinite<VAR>hy : ¬y.Infinite<GOAL>¬(x + y).Infinite
<VAR>x : ℝ*<GOAL>¬x.Infinite ↔ ∃ r s, ↑r < x ∧ x < ↑s
<VAR>x : ℝ*<GOAL>x.Infinite → ∀ (r : ℝ), x ≠ ↑r
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hxr : x.IsSt r<VAR>hys : y.IsSt s<GOAL>(x * y).IsSt (r * s)
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinite<VAR>hy : ¬y.Infinite<GOAL>¬(x * y).Infinite
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinite<VAR>hy : ¬y.Infinite<GOAL>(x + y).st = x.st + y.st
<VAR>x : ℝ*<GOAL>(-x).st = -x.st
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinite<VAR>hy : ¬y.Infinite<GOAL>(x * y).st = x.st * y.st
<VAR>x : ℝ*<GOAL>x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r
<VAR>x : ℝ*<GOAL>x.Infinitesimal → ∀ (r : ℝ), 0 < r → x < ↑r
<VAR>x : ℝ*<GOAL>x.Infinitesimal → ∀ (r : ℝ), 0 < r → -↑r < x
<VAR>x : ℝ*<VAR>hi : x.Infinitesimal<VAR>r : ℝ<VAR>hr : r < 0<GOAL>↑r < x
<VAR>x : ℝ*<GOAL>x.Infinitesimal ↔ ∀ (r : ℝ), r ≠ 0 → |x| < |↑r|
<VAR>r : ℝ<GOAL>(↑r).Infinitesimal → r = 0