ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>(⨆ i, f i) - a = ⨆ i, f i - a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>a - ⨅ i, f i = ⨆ i, a - f i
<VAR>a : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>sInf s + a = ⨅ b ∈ s, b + a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>a + iInf f = ⨅ b, a + f b
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j<GOAL>iInf f + iInf g = ⨅ a, f a + g a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → α → ℝ≥0∞<VAR>s : Finset α<VAR>Nonempty ι<VAR>h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a<GOAL>⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0∞<VAR>x : ℝ≥0∞<VAR>h0 : x ≠ 0<VAR>h : x ≠ ⊤<GOAL>iInf f * x = ⨅ i, f i * x
<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>f : ι → ℝ≥0∞<VAR>x : ℝ≥0∞<VAR>h : x ≠ ⊤<GOAL>iInf f * x = ⨅ i, f i * x
<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>f : ι → ℝ≥0∞<VAR>x : ℝ≥0∞<VAR>h : x ≠ ⊤<GOAL>x * iInf f = ⨅ i, x * f i
<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0∞<VAR>x : ℝ≥0∞<VAR>h0 : x ≠ 0<VAR>h : x ≠ ⊤<GOAL>x * iInf f = ⨅ i, x * f i
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<GOAL>⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
<VAR>ι : Sort u_1<GOAL>⨆ x, 0 = 0
<VAR>a b : ℝ≥0∞<GOAL>a ⊔ b = 0 ↔ a = 0 ∧ b = 0
<VAR>l : List ℕ<VAR>k : ℕ<GOAL>l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
<VAR>k : ℕ<VAR>l : List ℕ<GOAL>k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n
<VAR>m : Multiset ℕ<VAR>k : ℕ<GOAL>m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k
<VAR>k : ℕ<VAR>m : Multiset ℕ<GOAL>k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : ι → ℕ<VAR>x : ℕ<GOAL>(∏ i : ι, s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>x : ℕ<VAR>s : ι → ℕ<GOAL>x.Coprime (∏ i : ι, s i) ↔ ∀ (i : ι), x.Coprime (s i)
<VAR>p a b : ℕ<VAR>hp : Nat.Prime p<VAR>hap : a < p<VAR>hbp : b < p<VAR>h : p ≤ a + b<GOAL>p ∣ (a + b).choose a
<VAR>p a b : ℕ<VAR>hp : Nat.Prime p<VAR>ha : a < p<VAR>hab : b - a < p<VAR>h : p ≤ b<GOAL>p ∣ b.choose a
<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<VAR>hkp : k < p<GOAL>p ∣ p.choose k
<VAR>a b c d : ℝ≥0∞<VAR>ac : a < c<VAR>bd : b < d<GOAL>a * b < c * d
<VAR>a : ℝ≥0∞<GOAL>Monotone fun x => a * x
<VAR>a : ℝ≥0∞<GOAL>Monotone fun x => x * a
<VAR>n : ℕ<GOAL>n ≠ 0 → StrictMono fun x => x ^ n
<VAR>a b : ℝ≥0∞<VAR>h : a < b<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n < b ^ n
<VAR>a b c : ℝ≥0∞<GOAL>max a b * c = max (a * c) (b * c)
<VAR>a b c : ℝ≥0∞<GOAL>a * max b c = max (a * b) (a * c)
<VAR>a : ℝ≥0∞<VAR>h0 : a ≠ 0<VAR>hinf : a ≠ ⊤<GOAL>StrictMono fun x => a * x
<VAR>a b c : ℝ≥0∞<VAR>h0 : a ≠ 0<VAR>hinf : a ≠ ⊤<VAR>bc : b < c<GOAL>a * b < a * c
<VAR>a b c : ℝ≥0∞<VAR>h0 : a ≠ 0<VAR>hinf : a ≠ ⊤<VAR>bc : b < c<GOAL>b * a < c * a
<VAR>a b c : ℝ≥0∞<VAR>h0 : a ≠ 0<VAR>hinf : a ≠ ⊤<GOAL>a * b = a * c ↔ b = c
<VAR>a b c : ℝ≥0∞<GOAL>c ≠ 0 → c ≠ ⊤ → (a * c = b * c ↔ a = b)
<VAR>a b c : ℝ≥0∞<VAR>h0 : a ≠ 0<VAR>hinf : a ≠ ⊤<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>a b c : ℝ≥0∞<GOAL>c ≠ 0 → c ≠ ⊤ → (a * c ≤ b * c ↔ a ≤ b)
<VAR>a b c : ℝ≥0∞<VAR>h0 : a ≠ 0<VAR>hinf : a ≠ ⊤<GOAL>a * b < a * c ↔ b < c
<VAR>a b c : ℝ≥0∞<GOAL>c ≠ 0 → c ≠ ⊤ → (a * c < b * c ↔ a < b)
<VAR>a : ℝ≥0∞<GOAL>0 < a → ∀ (n : ℕ), 0 < a ^ n
<VAR>a : ℝ≥0∞<GOAL>a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0
<VAR>a : ℝ≥0∞<GOAL>¬a < 0
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → a + b ≤ a + c → b ≤ c
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → b + a ≤ c + a → b ≤ c
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → b < c → a + b < a + c
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → b < c → b + a < c + a
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → (a + b < a + c ↔ b < c)
<VAR>a b c : ℝ≥0∞<GOAL>a ≠ ⊤ → (b + a < c + a ↔ b < c)
<VAR>a b c d : ℝ≥0∞<GOAL>a ≠ ⊤ → a ≤ b → c < d → a + c < b + d
<VAR>a b c d : ℝ≥0∞<GOAL>c ≠ ⊤ → a < b → c ≤ d → a + c < b + d
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<GOAL>a < a + b
<VAR>a b : ℝ≥0∞<GOAL>a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>a b : ℝ≥0∞<GOAL>a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
<VAR>r₁ r₂ : ℝ≥0∞<VAR>h₁ : r₁ ≠ ⊤<VAR>h₂ : r₂ ≠ ⊤<GOAL>(r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal
<VAR>x : ℝ≥0∞<GOAL>¬x < ⊤ ↔ x = ⊤
<VAR>a b : ℝ≥0∞<GOAL>a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
<VAR>a : ℝ≥0∞<GOAL>a * ⊤ = if a = 0 then 0 else ⊤
<VAR>a : ℝ≥0∞<VAR>h : a ≠ 0<GOAL>a * ⊤ = ⊤
<VAR>a : ℝ≥0∞<GOAL>⊤ * a = if a = 0 then 0 else ⊤
<VAR>a : ℝ≥0∞<VAR>h : a ≠ 0<GOAL>⊤ * a = ⊤
<VAR>a b : ℝ≥0∞<GOAL>a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
<VAR>a b : ℝ≥0∞<GOAL>a ≠ ⊤ → b ≠ ⊤ → a * b < ⊤
<VAR>a b : ℝ≥0∞<GOAL>a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤
<VAR>a b : ℝ≥0∞<VAR>h : a * b ≠ ⊤<VAR>hb : b ≠ 0<GOAL>a < ⊤
<VAR>a b : ℝ≥0∞<VAR>h : a * b ≠ ⊤<VAR>ha : a ≠ 0<GOAL>b < ⊤
<VAR>a b : ℝ≥0∞<GOAL>a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
<VAR>a : ℝ≥0∞<GOAL>a * a < ⊤ ↔ a < ⊤
<VAR>a b : ℝ≥0∞<GOAL>0 < a * b ↔ 0 < a ∧ 0 < b
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>0 < a * b
<VAR>a : ℝ≥0∞<VAR>n : ℕ<GOAL>a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
<VAR>a : ℝ≥0∞<VAR>n : ℕ<VAR>h : a ^ n = ⊤<GOAL>a = ⊤
<VAR>a : ℝ≥0∞<VAR>h : a ≠ ⊤<VAR>n : ℕ<GOAL>a ^ n ≠ ⊤
<VAR>a : ℝ≥0∞<GOAL>a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0<GOAL>↑(∑ a ∈ s, f a) = ∑ a ∈ s, ↑(f a)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0<GOAL>↑(∏ a ∈ s, f a) = ∏ a ∈ s, ↑(f a)
<VAR>a b c d : ℝ≥0∞<VAR>ac : a < c<VAR>bd : b < d<GOAL>a + b < c + d
<VAR>a : ℝ≥0∞<GOAL>AddLECancellable a ↔ a ≠ ⊤
<VAR>a : ℝ≥0∞<VAR>h : a ≠ ⊤<GOAL>AddLECancellable a
<VAR>a : ℝ≥0∞<VAR>h : a < ⊤<GOAL>AddLECancellable a
<VAR>a b : ℝ≥0∞<VAR>h : a < b<GOAL>AddLECancellable a
<VAR>a : ℝ≥0<GOAL>AddLECancellable ↑a
<VAR>a b c : ℝ≥0∞<VAR>h : a ≠ ⊤<GOAL>a + b = a + c ↔ b = c
<VAR>a b c : ℝ≥0∞<VAR>h : a ≠ ⊤<GOAL>b + a = c + a ↔ b = c
<VAR>a b : ℝ≥0∞<GOAL>a - b = sInf {d | a ≤ d + b}
<VAR>r p : ℝ≥0<GOAL>↑(r - p) = ↑r - ↑p
<VAR>r : ℝ≥0<GOAL>⊤ - ↑r = ⊤
<VAR>a : ℝ≥0∞<GOAL>a - ⊤ = 0
<VAR>a b : ℝ≥0∞<GOAL>a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>a - b ≠ ⊤
<VAR>a b c : ℝ≥0∞<VAR>hb : b ≠ ⊤<GOAL>a = c + b → a - b = c
<VAR>a b c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>a + c = b → a = b - c
<VAR>a b c : ℝ≥0∞<VAR>hb : b ≠ ⊤<GOAL>a = b + c → a - b = c
<VAR>a b c : ℝ≥0∞<VAR>hb : b ≠ ⊤<VAR>hc : a + b = c<GOAL>c - b = a
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>a + b - a = b
<VAR>a b : ℝ≥0∞<VAR>hb : b ≠ ⊤<GOAL>a + b - b = a
<VAR>a b c : ℝ≥0∞<VAR>h : a ≠ ⊤ ∨ b ≠ ⊤<GOAL>a - b < c → a < b + c
<VAR>a b c : ℝ≥0∞<VAR>h : a ≠ ⊤ ∨ c ≠ ⊤<GOAL>a - c < b → a < b + c
<VAR>a b c : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>a + b ≤ c → b ≤ c - a
<VAR>a b c : ℝ≥0∞<VAR>hb : b ≠ ⊤<GOAL>a + b ≤ c → a ≤ c - b
<VAR>a b c : ℝ≥0∞<VAR>hac : c ≤ a<VAR>h : a < b + c<GOAL>a - c < b
<VAR>a b c : ℝ≥0∞<VAR>hb : b ≠ ⊤<VAR>hab : b ≤ a<GOAL>a - b < c ↔ a < c + b
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>ha₀ : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a - b < a
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>a - b < a ↔ 0 < a ∧ 0 < b
<VAR>a b c : ℝ≥0∞<VAR>h₂ : c ≤ a<VAR>h₃ : a ≠ ⊤ ∨ b ≠ ⊤<VAR>h₁ : a - b < c<GOAL>a - c < b
<VAR>a b : ℝ≥0∞<VAR>h : a ≠ ⊤<VAR>h2 : b ≤ a<GOAL>a - (a - b) = b
<VAR>a b c : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≤ a<VAR>hc : c ≤ a<GOAL>a - b = a - c ↔ b = c
<VAR>a b c : ℝ≥0∞<VAR>h : 0 < b → b < a → c ≠ ⊤<GOAL>(a - b) * c = a * c - b * c
<VAR>a b c : ℝ≥0∞<VAR>h : 0 < c → c < b → a ≠ ⊤<GOAL>a * (b - c) = a * b - a * c
<VAR>a b c : ℝ≥0∞<VAR>h : c ≤ a<VAR>h' : a ≠ ⊤<GOAL>a - b ≤ a - c ↔ c ≤ b
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ a ∈ s, f a ≠ ⊤<GOAL>∏ a ∈ s, f a < ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ a ∈ s, f a ≠ ⊤<GOAL>∑ a ∈ s, f a < ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<GOAL>∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<GOAL>∑ x ∈ s, f x = ⊤ ↔ ∃ a ∈ s, f a = ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>h : ∑ x ∈ s, f x ≠ ⊤<VAR>a : α<VAR>ha : a ∈ s<GOAL>f a < ⊤
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>(∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>f g : α → ℝ≥0∞<VAR>Hlt : ∀ i ∈ s, f i < g i<GOAL>∑ i ∈ s, f i < ∑ i ∈ s, g i
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>f g : α → ℝ≥0∞<VAR>Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i<GOAL>∃ i ∈ s, f i ≤ g i
<VAR>y : ℝ≥0∞<GOAL>Set.Ico 0 y = Set.Iio y
<VAR>x ε : ℝ≥0∞<GOAL>x ≠ ⊤ → ε ≠ 0 → x ∈ Set.Iio (x + ε)
<VAR>x ε₁ ε₂ : ℝ≥0∞<GOAL>x ≠ ⊤ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Set.Ioo (x - ε₁) (x + ε₂)
<VAR>M : Type u_1<VAR>MulAction ℝ≥0∞ M<VAR>c : ℝ≥0<VAR>x : M<GOAL>c • x = ↑c • x
<VAR>R : Type u_1<VAR>r : R<VAR>s : ℝ≥0<VAR>SMul R ℝ≥0<VAR>SMul R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0 ℝ≥0<VAR>IsScalarTower R ℝ≥0 ℝ≥0∞<GOAL>↑(r • s) = r • ↑s
<VAR>R : Type u_1<VAR>Zero R<VAR>SMulWithZero R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>NoZeroSMulDivisors R ℝ≥0∞<VAR>DecidableEq R<VAR>c : R<GOAL>c • ⊤ = if c = 0 then 0 else ⊤
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>CharZero K<VAR>a b : ℕ<VAR>h : a ≤ b<GOAL>↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>CharZero K<VAR>a b : ℕ<GOAL>↑((a + b).choose a) = ↑(a + b)! / (↑a ! * ↑b !)
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>CharZero K<VAR>a b : ℕ<GOAL>↑(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b !
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>CharZero K<VAR>a : ℕ<GOAL>↑(a.choose 2) = ↑a * (↑a - 1) / 2
<VAR>m n k : ℕ<GOAL>(m + n).choose k = ∑ ij ∈ Finset.antidiagonal k, m.choose ij.1 * n.choose ij.2
<VAR>a b d : ℕ<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<VAR>hd : ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d<GOAL>d = a.gcd b
<VAR>m n : ℕ<GOAL>m.gcd (n + m) = m.gcd n
<VAR>m n : ℕ<GOAL>m.lcm n ∣ m * n
<VAR>m n k : ℕ<GOAL>m.lcm n ∣ k ↔ m ∣ k ∧ n ∣ k
<VAR>m n k : ℕ<VAR>H : k.Coprime n<GOAL>k ∣ m * n ↔ k ∣ m
<VAR>m n k : ℕ<VAR>H : k.Coprime m<GOAL>k ∣ m * n ↔ k ∣ n
<VAR>m n k : ℕ<GOAL>(m + k * n).Coprime n ↔ m.Coprime n
<VAR>n : ℕ<GOAL>Nat.Coprime 1 n ↔ True
<VAR>n : ℕ<GOAL>n.Coprime 1 ↔ True
<VAR>m n : ℕ<VAR>h : m.Coprime n<VAR>hmn : m * n = 0<GOAL>m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
<VAR>x m n : ℕ<GOAL>x ∣ m * n ↔ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x
<VAR>a b k : ℕ<VAR>h_ab_coprime : a.Coprime b<VAR>hka : k ∣ a<VAR>hkb : k ∣ b<GOAL>k = 1
<VAR>m n a b : ℕ<VAR>cop : m.Coprime n<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a * m + b * n ≠ m * n
<VAR>x n m : ℕ<GOAL>x ∣ x.gcd n * m ↔ x ∣ n * m
<VAR>x n m : ℕ<VAR>hcop : n.Coprime m<GOAL>x.gcd n * x.gcd m = x ↔ x ∣ n * m
<VAR>a : ℕ<GOAL>Function.Periodic a.gcd a
<VAR>a : ℕ<GOAL>Function.Periodic a.Coprime a
<VAR>a : ℕ<GOAL>Function.Periodic (fun n => n % a) a
<VAR>α : Type u_1<VAR>f : ℕ → α<VAR>a : ℕ<VAR>hf : Function.Periodic f a<VAR>n : ℕ<GOAL>f (n % a) = f n
<VAR>n a : ℕ<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>pp : Function.Periodic p a<GOAL>Multiset.card (Multiset.filter p (Multiset.Ico n (n + a))) = Nat.count p a
<VAR>n a : ℕ<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>pp : Function.Periodic p a<GOAL>(Finset.filter p (Finset.Ico n (n + a))).card = Nat.count p a
<VAR>p n k : ℕ<GOAL>(n.choose k).factorization p ≤ Nat.log p n
<VAR>p n k : ℕ<VAR>hn : 0 < n<GOAL>p ^ (n.choose k).factorization p ≤ n
<VAR>p n : ℕ<VAR>n_big : 2 < n<VAR>p_le_n : p ≤ n<VAR>big : 2 * n < 3 * p<GOAL>n.centralBinom.factorization p = 0
<VAR>p n : ℕ<VAR>h : n < p<GOAL>n.factorial.factorization p = 0
<VAR>p n k : ℕ<VAR>h : n < p<GOAL>(n.choose k).factorization p = 0
<VAR>p n : ℕ<VAR>h : 2 * n < p<GOAL>n.centralBinom.factorization p = 0
<VAR>p n : ℕ<VAR>h_pos : 0 < n.centralBinom.factorization p<GOAL>p ≤ 2 * n
<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k
<VAR>n : ℕ<GOAL>∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>↑(n.choose r) ≤ ↑n ^ r / ↑r !
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>↑(n + 1 - r) ^ r / ↑r ! ≤ ↑(n.choose r)
<VAR>s : Set ℕ<VAR>h : s.Nonempty<GOAL>sInf s = Nat.find h
<VAR>s : Set ℕ<VAR>h : ∃ n, ∀ a ∈ s, a ≤ n<GOAL>sSup s = Nat.find h
<VAR>s : Set ℕ<VAR>h : s.Infinite<GOAL>sSup s = 0
<VAR>ι : Sort u_1<VAR>IsEmpty ι<VAR>f : ι → ℕ<GOAL>iInf f = 0
<VAR>ι : Sort u_1<GOAL>⨅ i, 0 = 0
<VAR>s : Set ℕ<VAR>h : 0 < sInf s<GOAL>s.Nonempty
<VAR>s : Set ℕ<VAR>k : ℕ<VAR>h : sInf s = k + 1<GOAL>s.Nonempty
<VAR>s : Set ℕ<VAR>hs : s.Nonempty<VAR>hs' : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s<GOAL>s = Set.Ici (sInf s)
<VAR>s : Set ℕ<VAR>hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s<VAR>k : ℕ<GOAL>sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
<VAR>s : Set ℕ<VAR>h₁ : s.Nonempty<VAR>h₂ : BddAbove s<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨅ k, ⨅ (_ : k < n + 1), u k = (⨅ k, ⨅ (_ : k < n), u k) ⊓ u n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨅ k, ⨅ (_ : k < n + 1), u k = u 0 ⊓ ⨅ k, ⨅ (_ : k < n), u (k + 1)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k ≤ n + 1), u k = (⨆ k, ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨅ k, ⨅ (_ : k ≤ n + 1), u k = (⨅ k, ⨅ (_ : k ≤ n), u k) ⊓ u (n + 1)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨅ k, ⨅ (_ : k ≤ n + 1), u k = u 0 ⊓ ⨅ k, ⨅ (_ : k ≤ n), u (k + 1)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋃ k, ⋃ (_ : k < n + 1), u k = (⋃ k, ⋃ (_ : k < n), u k) ∪ u n
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋃ k, ⋃ (_ : k < n + 1), u k = u 0 ∪ ⋃ k, ⋃ (_ : k < n), u (k + 1)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋂ k, ⋂ (_ : k < n + 1), u k = (⋂ k, ⋂ (_ : k < n), u k) ∩ u n
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋂ k, ⋂ (_ : k < n + 1), u k = u 0 ∩ ⋂ k, ⋂ (_ : k < n), u (k + 1)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋃ k, ⋃ (_ : k ≤ n + 1), u k = (⋃ k, ⋃ (_ : k ≤ n), u k) ∪ u (n + 1)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋃ k, ⋃ (_ : k ≤ n + 1), u k = u 0 ∪ ⋃ k, ⋃ (_ : k ≤ n), u (k + 1)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋂ k, ⋂ (_ : k ≤ n + 1), u k = (⋂ k, ⋂ (_ : k ≤ n), u k) ∩ u (n + 1)
<VAR>α : Type u_1<VAR>u : ℕ → Set α<VAR>n : ℕ<GOAL>⋂ k, ⋂ (_ : k ≤ n + 1), u k = u 0 ∩ ⋂ k, ⋂ (_ : k ≤ n), u (k + 1)
<VAR>n : ℕ<GOAL>n.centralBinom = (2 * n).choose n
<VAR>n : ℕ<GOAL>0 < n.centralBinom
<VAR>n : ℕ<GOAL>n.centralBinom ≠ 0
<VAR>r n : ℕ<GOAL>(2 * n).choose r ≤ n.centralBinom
<VAR>n : ℕ<VAR>n_pos : 0 < n<GOAL>2 ≤ n.centralBinom
<VAR>n : ℕ<GOAL>(n + 1) * (n + 1).centralBinom = 2 * (2 * n + 1) * n.centralBinom
<VAR>n : ℕ<GOAL>0 < n → 4 ^ n ≤ 2 * n * n.centralBinom
<VAR>n p : ℕ<GOAL>p ∈ n.primeFactorsList → Nat.Prime p
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactorsList<GOAL>0 < p
<VAR>n : ℕ<GOAL>n ≠ 0 → n.primeFactorsList.prod = n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p.primeFactorsList = [p]
<VAR>n a : ℕ<GOAL>(∀ (p : ℕ), Nat.Prime p → p ∣ n → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a n.primeFactorsList
<VAR>n : ℕ<GOAL>List.Chain (fun x x_1 => x ≤ x_1) 2 n.primeFactorsList
<VAR>n : ℕ<GOAL>List.Chain' (fun x x_1 => x ≤ x_1) n.primeFactorsList
<VAR>n : ℕ<GOAL>List.Sorted (fun x x_1 => x ≤ x_1) n.primeFactorsList
<VAR>n : ℕ<GOAL>(n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList
<VAR>n : ℕ<GOAL>n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : a.primeFactorsList.Perm b.primeFactorsList<GOAL>a = b
<VAR>n p : ℕ<VAR>hn : n ≠ 0<VAR>hp : Nat.Prime p<GOAL>p ∈ n.primeFactorsList ↔ p ∣ n
<VAR>n p : ℕ<VAR>hn : n ≠ 0<GOAL>p ∈ n.primeFactorsList ↔ Nat.Prime p ∧ p ∣ n
<VAR>n p : ℕ<GOAL>p ∈ n.primeFactorsList ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
<VAR>n : ℕ<VAR>l : List ℕ<VAR>h₁ : l.prod = n<VAR>h₂ : ∀ p ∈ l, Nat.Prime p<GOAL>l.Perm n.primeFactorsList
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n : ℕ<GOAL>(p ^ n).primeFactorsList = List.replicate n p
<VAR>n p : ℕ<VAR>hpos : n ≠ 0<VAR>h : ∀ {d : ℕ}, Nat.Prime d → d ∣ n → d = p<GOAL>n = p ^ n.primeFactorsList.length
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>(a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)
<VAR>n k : ℕ<VAR>h : k ≠ 0<GOAL>n.primeFactorsList.Sublist (n * k).primeFactorsList
<VAR>n k : ℕ<VAR>h : n ∣ k<VAR>h' : k ≠ 0<GOAL>n.primeFactorsList.Sublist k.primeFactorsList
<VAR>n k : ℕ<VAR>h : k ≠ 0<GOAL>n.primeFactorsList ⊆ (n * k).primeFactorsList
<VAR>n k : ℕ<VAR>h : n ∣ k<VAR>h' : k ≠ 0<GOAL>n.primeFactorsList ⊆ k.primeFactorsList
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>h : a.primeFactorsList.Subperm b.primeFactorsList<GOAL>a ∣ b
<VAR>a b n : ℕ<VAR>ha : Nat.Prime a<VAR>hb : b ≠ 0<GOAL>(List.replicate n a).Subperm b.primeFactorsList ↔ a ^ n ∣ b
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>a.primeFactorsList.Disjoint b.primeFactorsList
<VAR>n : ℕ<GOAL>(∃ k, n = 2 ^ k) ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
<VAR>n : ℕ<VAR>n2 : 2 < n<GOAL>4 ∣ n ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
<VAR>a b : ENNReal<GOAL>a / b = b⁻¹ * a
<VAR>r : ℝ≥0<GOAL>↑r⁻¹ ≤ (↑r)⁻¹
<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>↑r⁻¹ = (↑r)⁻¹
<GOAL>↑2⁻¹ = 2⁻¹
<VAR>r p : ℝ≥0<VAR>hr : r ≠ 0<GOAL>↑(p / r) = ↑p / ↑r
<VAR>r p : ℝ≥0<GOAL>↑(p / r) ≤ ↑p / ↑r
<VAR>a : ENNReal<VAR>h : a ≠ 0<GOAL>a / 0 = ⊤
<VAR>a : ENNReal<VAR>n : ℕ<GOAL>(a ^ n)⁻¹ = a⁻¹ ^ n
<VAR>a : ENNReal<VAR>h0 : a ≠ 0<VAR>ht : a ≠ ⊤<GOAL>a * a⁻¹ = 1
<VAR>a : ENNReal<VAR>h0 : a ≠ 0<VAR>ht : a ≠ ⊤<GOAL>a⁻¹ * a = 1
<VAR>a b : ENNReal<VAR>h0 : a ≠ 0<VAR>hI : a ≠ ⊤<GOAL>b / a * a = b
<VAR>a b : ENNReal<VAR>h0 : a ≠ 0<VAR>hI : a ≠ ⊤<GOAL>a * (b / a) = b
<VAR>a b c : ENNReal<GOAL>a / b * c = a * (c / b)
<VAR>a b c : ENNReal<GOAL>a * b / c = a / c * b
<VAR>a : ENNReal<GOAL>a⁻¹ = 1 ↔ a = 1
<VAR>a : ENNReal<GOAL>a⁻¹ = ⊤ ↔ a = 0
<VAR>a : ENNReal<GOAL>a⁻¹ ≠ ⊤ ↔ a ≠ 0
<VAR>x : ENNReal<GOAL>x⁻¹ < ⊤ ↔ 0 < x
<VAR>x y : ENNReal<VAR>h1 : x ≠ ⊤<VAR>h2 : y ≠ 0<GOAL>x / y < ⊤
<VAR>a : ENNReal<GOAL>a⁻¹ = 0 ↔ a = ⊤
<VAR>a : ENNReal<GOAL>a⁻¹ ≠ 0 ↔ a ≠ ⊤
<VAR>a b : ENNReal<VAR>ha : a ≠ 0<VAR>hb : b ≠ ⊤<GOAL>0 < a / b
<VAR>x y z : ENNReal<VAR>h1 : x ≠ 0<VAR>h2 : x ≠ ⊤<GOAL>x⁻¹ * y ≤ z ↔ y ≤ x * z
<VAR>x y z : ENNReal<VAR>h1 : y ≠ 0<VAR>h2 : y ≠ ⊤<GOAL>x * y⁻¹ ≤ z ↔ x ≤ z * y
<VAR>x y z : ENNReal<VAR>h1 : y ≠ 0<VAR>h2 : y ≠ ⊤<GOAL>x / y ≤ z ↔ x ≤ z * y
<VAR>x y z : ENNReal<VAR>h1 : y ≠ 0<VAR>h2 : y ≠ ⊤<GOAL>x / y ≤ z ↔ x ≤ y * z
<VAR>a b : ENNReal<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<VAR>hb : a ≠ ⊤ ∨ b ≠ 0<GOAL>(a * b)⁻¹ = a⁻¹ * b⁻¹
<VAR>c : ENNReal<VAR>a b : ENNReal<VAR>hc : c ≠ 0<VAR>hc' : c ≠ ⊤<GOAL>c * a / (c * b) = a / b
<VAR>c : ENNReal<VAR>a b : ENNReal<VAR>hc : c ≠ 0<VAR>hc' : c ≠ ⊤<GOAL>a * c / (b * c) = a / b
<VAR>a b c : ENNReal<VAR>h : 0 < b → b < a → c ≠ 0<GOAL>(a - b) / c = a / c - b / c
<VAR>a : ENNReal<GOAL>0 < a⁻¹ ↔ a ≠ ⊤
<VAR>a b : ENNReal<GOAL>a⁻¹ < b⁻¹ ↔ b < a
<VAR>a b : ENNReal<GOAL>a⁻¹ < b ↔ b⁻¹ < a
<VAR>a b : ENNReal<GOAL>a < b⁻¹ ↔ b < a⁻¹
<VAR>a b : ENNReal<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>a b : ENNReal<GOAL>a⁻¹ ≤ b ↔ b⁻¹ ≤ a
<VAR>a b : ENNReal<GOAL>a ≤ b⁻¹ ↔ b ≤ a⁻¹
<VAR>a b : ENNReal<VAR>h : a ≤ b<GOAL>b⁻¹ ≤ a⁻¹
<VAR>a b : ENNReal<VAR>h : a < b<GOAL>b⁻¹ < a⁻¹
<VAR>a : ENNReal<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>a : ENNReal<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>a : ENNReal<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>a : ENNReal<GOAL>1 < a⁻¹ ↔ a < 1
<GOAL>∀ (a : ENNReal), OrderIso.invENNReal a = (OrderDual.toDual a)⁻¹
<VAR>a : ENNRealᵒᵈ<GOAL>OrderIso.invENNReal.symm a = (OrderDual.ofDual a)⁻¹
<VAR>a : ENNReal<GOAL>a / ⊤ = 0
<VAR>a : ENNReal<GOAL>⊤ / a = if a = ⊤ then 0 else ⊤
<VAR>a : ENNReal<VAR>h : a ≠ ⊤<GOAL>⊤ / a = ⊤
<VAR>p : ℝ≥0<GOAL>⊤ / ↑p = ⊤
<VAR>a : ENNReal<VAR>h : a < ⊤<GOAL>⊤ / a = ⊤
<VAR>a b : ENNReal<GOAL>a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤
<VAR>a b c : ENNReal<VAR>h0 : b ≠ 0 ∨ c ≠ 0<VAR>ht : b ≠ ⊤ ∨ c ≠ ⊤<GOAL>a ≤ c / b ↔ a * b ≤ c
<VAR>a b c : ENNReal<VAR>hb0 : b ≠ 0 ∨ c ≠ ⊤<VAR>hbt : b ≠ ⊤ ∨ c ≠ 0<GOAL>a / b ≤ c ↔ a ≤ c * b
<VAR>a b c : ENNReal<VAR>hb0 : b ≠ 0 ∨ c ≠ ⊤<VAR>hbt : b ≠ ⊤ ∨ c ≠ 0<GOAL>c < a / b ↔ c * b < a
<VAR>a b c : ENNReal<VAR>h : a ≤ b * c<GOAL>a / c ≤ b
<VAR>a b c : ENNReal<VAR>h : a ≤ b * c<GOAL>a / b ≤ c
<VAR>a : ENNReal<GOAL>a / a ≤ 1
<VAR>a : ENNReal<GOAL>a * a⁻¹ ≤ 1
<VAR>a : ENNReal<GOAL>a⁻¹ * a ≤ 1
<VAR>a : ENNReal<GOAL>a * a⁻¹ ≠ ⊤
<VAR>a : ENNReal<GOAL>a⁻¹ * a ≠ ⊤
<VAR>a b c : ENNReal<VAR>h : a ≤ b / c<GOAL>a * c ≤ b
<VAR>a b c : ENNReal<VAR>h : a ≤ b / c<GOAL>c * a ≤ b
<VAR>a b c : ENNReal<VAR>h0 : b ≠ 0 ∨ c ≠ 0<VAR>ht : b ≠ ⊤ ∨ c ≠ ⊤<GOAL>c / b < a ↔ c < a * b
<VAR>a b c : ENNReal<VAR>h : a < b / c<GOAL>a * c < b
<VAR>a b c : ENNReal<VAR>h : a < b / c<GOAL>c * a < b
<VAR>a b c : ENNReal<VAR>h : a < b * c<GOAL>a / c < b
<VAR>a b c : ENNReal<VAR>h : a < b * c<GOAL>a / b < c
<VAR>a b : ENNReal<VAR>h₁ : b = ⊤ → a ≠ 0<VAR>h₂ : a = ⊤ → b ≠ 0<GOAL>a⁻¹ ≤ b ↔ 1 ≤ a * b
<VAR>a b : ENNReal<GOAL>a ≤ b⁻¹ ↔ a * b ≤ 1
<VAR>a b c d : ENNReal<VAR>hab : a ≤ b<VAR>hdc : d ≤ c<GOAL>a / c ≤ b / d
<VAR>a b : ENNReal<VAR>h : a ≤ b<VAR>c : ENNReal<GOAL>c / b ≤ c / a
<VAR>a b : ENNReal<VAR>h : a ≤ b<VAR>c : ENNReal<GOAL>a / c ≤ b / c
<VAR>a b : ENNReal<VAR>h : a * b = 1<GOAL>a = b⁻¹
<VAR>a b r : ENNReal<VAR>hr₀ : r ≠ 0<VAR>hr₁ : r ≠ ⊤<GOAL>r * a ≤ b ↔ a ≤ r⁻¹ * b
<VAR>x y : ENNReal<VAR>h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y<GOAL>x ≤ y
<VAR>x y : ENNReal<VAR>h : ∀ (r : ℝ≥0), 0 < r → ↑r < x → ↑r ≤ y<GOAL>x ≤ y
<VAR>x : ENNReal<VAR>h : ∀ (r : ℝ≥0), ↑r ≤ x<GOAL>x = ⊤
<VAR>a b c : ENNReal<GOAL>(a + b) / c = a / c + b / c
<VAR>a b c : ENNReal<GOAL>a / c + b / c = (a + b) / c
<VAR>a : ENNReal<VAR>h0 : a ≠ 0<VAR>hI : a ≠ ⊤<GOAL>a / a = 1
<VAR>a b : ENNReal<GOAL>a * (b / a) ≤ b
<VAR>a b c : ENNReal<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<GOAL>b = c / a ↔ a * b = c
<VAR>a b c d : ENNReal<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>hb' : b ≠ ⊤<GOAL>c / b = d / a ↔ a * c = b * d
<VAR>a b : ENNReal<VAR>hb₀ : b ≠ 0<VAR>hb₁ : b ≠ ⊤<GOAL>a / b = 1 ↔ a = b
<GOAL>2⁻¹ + 2⁻¹ = 1
<GOAL>3⁻¹ + 3⁻¹ + 3⁻¹ = 1
<VAR>a : ENNReal<GOAL>a / 2 + a / 2 = a
<VAR>a : ENNReal<GOAL>a / 3 + a / 3 + a / 3 = a
<VAR>a b : ENNReal<GOAL>a / b = 0 ↔ a = 0 ∨ b = ⊤
<VAR>a b : ENNReal<GOAL>0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤
<VAR>a b : ENNReal<GOAL>a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ⊤
<VAR>a : ENNReal<VAR>h : a ≠ 0<GOAL>0 < a / 2
<VAR>a : ENNReal<VAR>hz : a ≠ 0<VAR>ht : a ≠ ⊤<GOAL>a / 2 < a
<VAR>a : ENNReal<GOAL>a / 2 ≤ a
<VAR>a : ENNReal<VAR>h : a ≠ ⊤<GOAL>a - a / 2 = a / 2
<GOAL>1 - 2⁻¹ = 2⁻¹
<VAR>x : ENNReal<GOAL>↑(ENNReal.orderIsoIicOneBirational x) = (x⁻¹ + 1)⁻¹
<VAR>x : ↑(Set.Iic 1)<GOAL>ENNReal.orderIsoIicOneBirational.symm x = ((↑x)⁻¹ - 1)⁻¹
<VAR>a : ℝ≥0<GOAL>∀ (a_1 : ↑(Set.Iic ↑a)), ↑((ENNReal.orderIsoIicCoe a) a_1) = (↑a_1).toNNReal
<VAR>a : ℝ≥0<VAR>b : ↑(Set.Iic a)<GOAL>↑((ENNReal.orderIsoIicCoe a).symm b) = ↑↑b
<VAR>x : ENNReal<GOAL>↑(ENNReal.orderIsoUnitIntervalBirational x) = (x⁻¹ + 1)⁻¹.toReal
<VAR>a : ENNReal<VAR>h : a ≠ 0<GOAL>∃ n, (↑n)⁻¹ < a
<VAR>a b : ENNReal<VAR>ha : a ≠ 0<VAR>hb : b ≠ ⊤<GOAL>∃ n > 0, b < ↑n * a
<VAR>a b : ENNReal<VAR>ha : a ≠ 0<VAR>hb : b ≠ ⊤<GOAL>∃ n, b < ↑n * a
<VAR>a b : ENNReal<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<GOAL>∃ n > 0, (↑n)⁻¹ * a < b
<VAR>a b : ENNReal<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<GOAL>∃ n > 0, ↑n * a < b
<VAR>a : ENNReal<VAR>ha : a ≠ 0<GOAL>∃ n, 2⁻¹ ^ n < a
<VAR>r : ℝ≥0<VAR>hr : r ≠ 0<VAR>n : ℤ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>a : ENNReal<VAR>ha : a ≠ 0<VAR>h'a : a ≠ ⊤<VAR>n : ℤ<GOAL>0 < a ^ n
<VAR>a : ENNReal<VAR>ha : a ≠ 0<VAR>h'a : a ≠ ⊤<VAR>n : ℤ<GOAL>a ^ n < ⊤
<VAR>x y : ENNReal<VAR>hx : x ≠ 0<VAR>h'x : x ≠ ⊤<VAR>hy : 1 < y<VAR>h'y : y ≠ ⊤<GOAL>∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
<VAR>x y : ENNReal<VAR>hx : x ≠ 0<VAR>h'x : x ≠ ⊤<VAR>hy : 1 < y<VAR>h'y : y ≠ ⊤<GOAL>∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
<VAR>y : ENNReal<VAR>hy : 1 < y<VAR>h'y : y ≠ ⊤<GOAL>Set.Ioo 0 ⊤ = ⋃ n, Set.Ico (y ^ n) (y ^ (n + 1))
<VAR>x : ENNReal<VAR>hx : 1 ≤ x<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>x ^ a ≤ x ^ b
<VAR>x : ENNReal<VAR>hx : 1 ≤ x<GOAL>Monotone fun x_1 => x ^ x_1
<VAR>x : ENNReal<VAR>hx : x ≠ 0<VAR>h'x : x ≠ ⊤<VAR>m n : ℤ<GOAL>x ^ (m + n) = x ^ m * x ^ n