ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin (n + 1)<GOAL>i.succ.succAbove 1 = (i.succAbove 0).succ
<VAR>n : ℕ<VAR>j : Fin n<GOAL>Fin.succAbove 1 j.succ = j.succ.succ
<VAR>n : ℕ<GOAL>Fin.succAbove 1 1 = 2
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : i ≤ p.castSucc<VAR>hi : i ≠ Fin.last n := ⋯<GOAL>p.predAbove i = i.castPred hi
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : i < p.succ<VAR>hi : i ≠ Fin.last n := ⋯<GOAL>p.predAbove i = i.castPred hi
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : p.castSucc < i<VAR>hi : i ≠ 0 := ⋯<GOAL>p.predAbove i = i.pred hi
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : p.succ ≤ i<VAR>hi : i ≠ 0 := ⋯<GOAL>p.predAbove i = i.pred hi
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : i < p<VAR>hi : i.succ ≠ Fin.last n := ⋯<GOAL>p.predAbove i.succ = i.succ.castPred hi
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : p ≤ i<GOAL>p.predAbove i.succ = i
<VAR>n : ℕ<VAR>p : Fin n<GOAL>p.predAbove p.succ = p
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : p < i<VAR>hi : i.castSucc ≠ 0 := ⋯<GOAL>p.predAbove i.castSucc = i.castSucc.pred hi
<VAR>n : ℕ<VAR>p i : Fin n<VAR>h : i ≤ p<GOAL>p.predAbove i.castSucc = i
<VAR>n : ℕ<VAR>p : Fin n<GOAL>p.predAbove p.castSucc = p
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : i < p<VAR>hp : p ≠ 0 := ⋯<VAR>hi : i ≠ Fin.last n := ⋯<GOAL>(p.pred hp).predAbove i = i.castPred hi
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : p ≤ i<VAR>hp : p ≠ 0<VAR>hi : i ≠ 0 := ⋯<GOAL>(p.pred hp).predAbove i = i.pred hi
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>hp : p ≠ 0<GOAL>(p.pred hp).predAbove p = p.pred hp
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : p < i<VAR>hp : p ≠ Fin.last n := ⋯<VAR>hi : i ≠ 0 := ⋯<GOAL>(p.castPred hp).predAbove i = i.pred hi
<VAR>n : ℕ<VAR>p i : Fin (n + 1)<VAR>h : i ≤ p<VAR>hp : p ≠ Fin.last n<VAR>hi : i ≠ Fin.last n := ⋯<GOAL>(p.castPred hp).predAbove i = i.castPred hi
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>hp : p ≠ Fin.last n<GOAL>(p.castPred hp).predAbove p = p.castPred hp
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>p.rev.predAbove i = (p.predAbove i.rev).rev
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>p.predAbove i.rev = (p.rev.predAbove i).rev
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin n<GOAL>i.predAbove 0 = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin n<GOAL>Fin.predAbove 0 i.succ = i
<VAR>n : ℕ<VAR>NeZero n<VAR>j : Fin (n + 1)<VAR>h : j ≠ 0<GOAL>(Fin.predAbove 0 j).succ = j
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>Fin.predAbove 0 i = i.pred hi
<VAR>n : ℕ<VAR>NeZero n<VAR>i : Fin (n + 1)<GOAL>Fin.predAbove 0 i = if hi : i = 0 then 0 else i.pred hi
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>i.predAbove (Fin.last (n + 1)) = Fin.last n
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(Fin.last n).predAbove i.castSucc = i
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>hi : i ≠ Fin.last (n + 1)<GOAL>(Fin.last n).predAbove i = i.castPred hi
<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>(Fin.last n).predAbove i = if hi : i = Fin.last (n + 1) then Fin.last n else i.castPred hi
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : i ≠ p.castSucc<GOAL>p.castSucc.succAbove (p.predAbove i) = i
<VAR>n : ℕ<VAR>p i : Fin n<GOAL>p.predAbove (p.castSucc.succAbove i) = i
<VAR>n : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<GOAL>a.succ.predAbove b.succ = (a.predAbove b).succ
<VAR>n : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<GOAL>a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>(p.predAbove i).rev = p.rev.predAbove i.rev
<VAR>n m : ℕ<VAR>i : Fin (m * n)<GOAL>↑i.divNat = ↑i / n
<VAR>n m : ℕ<VAR>i : Fin (m * n)<GOAL>↑i.modNat = ↑i % n
<VAR>n m : ℕ<VAR>i : Fin (m * n)<GOAL>i.rev.modNat = i.modNat.rev
<VAR>n : ℕ<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>f : Fin (n + 1) → α<GOAL>((fun x x_1 => x < x_1) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
<VAR>n : ℕ<VAR>a : Fin n<GOAL>-a = ⟨(n - ↑a) % n, ⋯⟩
<VAR>n : ℕ<VAR>a : Fin n<GOAL>↑(-a) = (n - ↑a) % n
<VAR>i : Fin 2<VAR>hi : i ≠ 0<GOAL>i = 1
<VAR>n : ℕ<GOAL>↑(-1) = n
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>Fin.last n - i = i.rev
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>h : a < b<GOAL>a + 1 ≤ b
<VAR>n : ℕ<VAR>a b : Fin n<VAR>h : a ≤ b<GOAL>∃ k ≤ b, b = a + k
<VAR>n : ℕ<VAR>a b : Fin (n + 1)<VAR>h : a < b<GOAL>∃ k < b, k + 1 ≤ b ∧ b = a + k + 1
<VAR>n : ℕ<VAR>a : Fin (n + 1)<VAR>h : a ≠ 0<GOAL>0 < a
<VAR>m n : ℕ<VAR>NeZero m<GOAL>↑↑n = n % m
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>k * 1 = k
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>1 * k = k
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>k * 0 = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>k : Fin n<GOAL>0 * k = 0
<VAR>s : Set ℕ<VAR>DecidablePred fun x => x ∈ s<VAR>h : Nonempty ↑s<GOAL>↑⊥ = Nat.find ⋯
<VAR>S : Set ℕ<GOAL>S = Set.univ ↔ 0 ∈ S ∧ ∀ k ∈ S, k + 1 ∈ S
<VAR>p : ℕ → Prop<VAR>H' : ¬p 0<VAR>H : ∃ n, p n<GOAL>∃ n, ¬p n ∧ p (n + 1)
<VAR>n : ℕ<VAR>self : n.AtLeastTwo<GOAL>n ≥ 2
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>1 < n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>n ≠ 1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>NatCast R<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>NatCast R<VAR>n.AtLeastTwo<GOAL>↑n = OfNat.ofNat n
<VAR>R : Type u_2<VAR>self : AddMonoidWithOne R<VAR>n : ℕ<GOAL>NatCast.natCast (n + 1) = NatCast.natCast n + 1
<VAR>R : Type u_2<VAR>self : AddMonoidWithOne R<GOAL>NatCast.natCast 0 = 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n : ℕ<GOAL>↑n.succ = ↑n + 1
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n : ℕ<GOAL>↑(n + 1) = ↑n + 1
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>P : Prop<VAR>Decidable P<VAR>m n : ℕ<GOAL>↑(if P then m else n) = if P then ↑m else ↑n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>m n : ℕ<GOAL>↑(m + n) = ↑m + ↑n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n : ℕ<GOAL>n.binCast = ↑n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<GOAL>↑2 = 2
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<GOAL>1 + 1 = 2
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<GOAL>2 + 1 = 3
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<GOAL>3 + 1 = 4
<VAR>a n : ℕ<GOAL>Nat.succ^[n] a = a + n
<VAR>a n : ℕ<GOAL>Nat.pred^[n] a = a - n
<VAR>m n : ℕ<GOAL>m ≤ n.succ ↔ m = n.succ ∨ m ≤ n
<VAR>P : ℕ → Prop<GOAL>(∀ (i : ℕ), i ≠ 0 → P i) ↔ ∀ (i : ℕ), P (i + 1)
<VAR>m n : ℕ<GOAL>m ⋖ n ↔ m + 1 = n
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑a ⋖ ↑b ↔ a ⋖ b
<VAR>m : ℕ<GOAL>hyperoperation 0 m = Nat.succ
<VAR>n m : ℕ<GOAL>hyperoperation (n + 3) m 0 = 1
<VAR>n m k : ℕ<GOAL>hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)
<GOAL>hyperoperation 1 = fun x x_1 => x + x_1
<GOAL>hyperoperation 2 = fun x x_1 => x * x_1
<GOAL>hyperoperation 3 = fun x x_1 => x ^ x_1
<VAR>n m : ℕ<GOAL>hyperoperation (n + 2) m 1 = m
<VAR>n : ℕ<GOAL>hyperoperation (n + 1) 2 2 = 4
<VAR>n k : ℕ<GOAL>hyperoperation (n + 3) 1 k = 1
<VAR>n k : ℕ<GOAL>hyperoperation (n + 4) 0 k = if Even k then 1 else 0
<VAR>a : ℝ≥0<GOAL>some a = ↑a
<VAR>a : ℝ≥0<GOAL>↑a = ↑a
<VAR>p q : ℝ≥0<GOAL>↑p = ↑q ↔ p = q
<VAR>p q : ℝ≥0<GOAL>↑p ≠ ↑q ↔ p ≠ q
<GOAL>Set.range ENNReal.ofNNReal = Set.Iio ⊤
<GOAL>Set.range ENNReal.ofNNReal = {⊤}ᶜ
<VAR>r : ℝ≥0<GOAL>(↑r).toNNReal = r
<VAR>a : ℝ≥0∞<GOAL>a ≠ ⊤ → ↑a.toNNReal = a
<VAR>a : ℝ≥0∞<VAR>h : a ≠ ⊤<GOAL>ENNReal.ofReal a.toReal = a
<VAR>r : ℝ<VAR>h : 0 ≤ r<GOAL>(ENNReal.ofReal r).toReal = r
<VAR>r : ℝ<GOAL>(ENNReal.ofReal r).toReal = max r 0
<VAR>a : ℝ≥0∞<GOAL>↑a.toNNReal ≤ a
<VAR>r : ℝ≥0<GOAL>↑r = ENNReal.ofReal ↑r
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>ENNReal.ofReal x = ↑⟨x, h⟩
<VAR>p : ℝ≥0<GOAL>ENNReal.ofReal ↑p = ↑p
<VAR>a : ℝ≥0∞<GOAL>0 ≤ a.toReal
<VAR>r : ℝ≥0<GOAL>(↑r).toReal = ↑r
<VAR>a : ℝ≥0∞<GOAL>ENNReal.ofReal a.toReal ≤ a
<VAR>p : ℝ≥0∞ → Prop<GOAL>(∀ (a : ℝ≥0∞), p a) ↔ (∀ (r : ℝ≥0), p ↑r) ∧ p ⊤
<VAR>p : ℝ≥0∞ → Prop<GOAL>(∀ (a : ℝ≥0∞), a ≠ ⊤ → p a) ↔ ∀ (r : ℝ≥0), p ↑r
<VAR>p : ℝ≥0∞ → Prop<GOAL>(∃ a, a ≠ ⊤ ∧ p a) ↔ ∃ r, p ↑r
<VAR>x : ℝ≥0∞<GOAL>x.toNNReal = 0 ↔ x = 0 ∨ x = ⊤
<VAR>x : ℝ≥0∞<GOAL>x.toReal = 0 ↔ x = 0 ∨ x = ⊤
<VAR>a : ℝ≥0∞<GOAL>a.toNNReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤
<VAR>a : ℝ≥0∞<GOAL>a.toReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤
<VAR>x : ℝ≥0∞<GOAL>x.toNNReal = 1 ↔ x = 1
<VAR>x : ℝ≥0∞<GOAL>x.toReal = 1 ↔ x = 1
<VAR>a : ℝ≥0∞<GOAL>a.toNNReal ≠ 1 ↔ a ≠ 1
<VAR>a : ℝ≥0∞<GOAL>a.toReal ≠ 1 ↔ a ≠ 1
<VAR>r : ℝ≥0<GOAL>↑r ≠ ⊤
<VAR>r : ℝ≥0<GOAL>⊤ ≠ ↑r
<VAR>r : ℝ≥0<GOAL>↑r < ⊤
<VAR>r : ℝ<GOAL>ENNReal.ofReal r ≠ ⊤
<VAR>r : ℝ<GOAL>ENNReal.ofReal r < ⊤
<VAR>r : ℝ<GOAL>⊤ ≠ ENNReal.ofReal r
<VAR>a : ℝ≥0∞<GOAL>ENNReal.ofReal a.toReal = a ↔ a ≠ ⊤
<VAR>a : ℝ<GOAL>(ENNReal.ofReal a).toReal = a ↔ 0 ≤ a
<VAR>r q : ℝ≥0<GOAL>↑r ≤ ↑q ↔ r ≤ q
<VAR>r q : ℝ≥0<GOAL>↑r < ↑q ↔ r < q
<VAR>r : ℝ≥0<GOAL>↑r = 0 ↔ r = 0
<VAR>r : ℝ≥0<GOAL>0 = ↑r ↔ 0 = r
<VAR>r : ℝ≥0<GOAL>↑r = 1 ↔ r = 1
<VAR>r : ℝ≥0<GOAL>1 = ↑r ↔ 1 = r
<VAR>r : ℝ≥0<GOAL>0 < ↑r ↔ 0 < r
<VAR>r : ℝ≥0<GOAL>↑r ≠ 0 ↔ r ≠ 0
<VAR>r : ℝ≥0<GOAL>↑r ≠ 1 ↔ r ≠ 1
<VAR>x y : ℝ≥0<GOAL>↑(x + y) = ↑x + ↑y
<VAR>x y : ℝ≥0<GOAL>↑(x * y) = ↑x * ↑y
<VAR>n : ℕ<VAR>x : ℝ≥0<GOAL>↑(n • x) = n • ↑x
<VAR>x : ℝ≥0<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>x y : ℝ≥0∞<GOAL>x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
<VAR>x y : ℝ≥0∞<GOAL>x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
<VAR>x y : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<GOAL>x.toNNReal = y.toNNReal ↔ x = y
<VAR>x y : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<GOAL>x.toReal = y.toReal ↔ x = y
<VAR>α : Type u_1<VAR>InfSet α<VAR>f : ℝ≥0∞ → α<GOAL>⨅ x, f ↑x = ⨅ x, f ↑x
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℝ≥0∞ → α<GOAL>⨅ x, ⨅ (_ : x ≠ ⊤), f x = ⨅ x, f ↑x
<VAR>α : Type u_1<VAR>SupSet α<VAR>f : ℝ≥0∞ → α<GOAL>⨆ x, f ↑x = ⨆ x, f ↑x
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℝ≥0∞ → α<GOAL>⨆ x, ⨆ (_ : x ≠ ⊤), f x = ⨆ x, f ↑x
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>f : ℝ≥0∞ → α<GOAL>⨅ n, f n = (⨅ n, f ↑n) ⊓ f ⊤
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>f : ℝ≥0∞ → α<GOAL>⨆ n, f n = (⨆ n, f ↑n) ⊔ f ⊤
<VAR>α : Type u_2<VAR>s : Set α<VAR>f : α → ℝ≥0<VAR>a : α<GOAL>↑(s.indicator f a) = s.indicator (fun x => ↑(f x)) a
<VAR>r : ℝ≥0<GOAL>¬⊤ ≤ ↑r
<VAR>r : ℝ≥0<GOAL>1 ≤ ↑r ↔ 1 ≤ r
<VAR>r : ℝ≥0<GOAL>↑r ≤ 1 ↔ r ≤ 1
<VAR>p : ℝ≥0<GOAL>↑p < 1 ↔ p < 1
<VAR>p : ℝ≥0<GOAL>1 < ↑p ↔ 1 < p
<VAR>n : ℕ<GOAL>ENNReal.ofReal ↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>ENNReal.ofReal (OfNat.ofNat n) = OfNat.ofNat n
<VAR>n : ℕ<GOAL>↑n ≠ ⊤
<VAR>n : ℕ<GOAL>⊤ ≠ ↑n
<VAR>n : ℕ<GOAL>(↑n).toNNReal = ↑n
<VAR>n : ℕ<GOAL>(↑n).toReal = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).toReal = OfNat.ofNat n
<VAR>a : ℝ≥0∞<VAR>r : ℝ≥0<GOAL>a ≤ ↑r ↔ ∃ p, a = ↑p ∧ p ≤ r
<VAR>a : ℝ≥0∞<VAR>r : ℝ≥0<GOAL>↑r ≤ a ↔ ∀ (p : ℝ≥0), a = ↑p → r ≤ p
<VAR>a b : ℝ≥0∞<GOAL>a < b ↔ ∃ p, a = ↑p ∧ ↑p < b
<VAR>a : ℝ≥0∞<VAR>b : ℝ≥0<VAR>h : a ≤ ↑b<GOAL>a.toReal ≤ ↑b
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0<GOAL>↑(s.sup f) = s.sup fun x => ↑(f x)
<VAR>a b : ℝ≥0∞<GOAL>max a b = 0 ↔ a = 0 ∧ b = 0
<VAR>a : ℝ≥0∞<GOAL>max 0 a = a
<VAR>a : ℝ≥0∞<GOAL>max a 0 = a
<VAR>a b : ℝ≥0∞<GOAL>a ⊔ b = max a b
<VAR>a b : ℝ≥0∞<GOAL>a < b ↔ ∃ q, 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
<VAR>a b : ℝ≥0∞<GOAL>a < b ↔ ∃ r, 0 ≤ r ∧ a < ENNReal.ofReal r ∧ ENNReal.ofReal r < b
<VAR>a b : ℝ≥0∞<GOAL>a < b ↔ ∃ r, a < ↑r ∧ ↑r < b
<VAR>a b : ℝ≥0∞<GOAL>a < b ↔ ∃ r, 0 < r ∧ a + ↑r < b
<VAR>a b : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0), 0 < ε → b < ⊤ → a ≤ b + ↑ε<GOAL>a ≤ b
<VAR>r : ℝ≥0<VAR>n : ℕ<GOAL>↑n < ↑r ↔ ↑n < r
<VAR>r : ℝ≥0<VAR>n : ℕ<GOAL>↑r < ↑n ↔ r < ↑n
<VAR>r : ℝ≥0∞<VAR>h : r ≠ ⊤<GOAL>∃ n, r < ↑n
<GOAL>⋃ n, Set.Iio ↑n = {⊤}ᶜ
<GOAL>⋃ n, Set.Iic ↑n = {⊤}ᶜ
<VAR>a : ℝ≥0∞<GOAL>⋃ n, Set.Ioc a ↑n = Set.Ioi a \ {⊤}
<VAR>a : ℝ≥0∞<GOAL>⋃ n, Set.Ioo a ↑n = Set.Ioi a \ {⊤}
<VAR>a : ℝ≥0∞<GOAL>⋃ n, Set.Icc a ↑n = Set.Ici a \ {⊤}
<VAR>a : ℝ≥0∞<GOAL>⋃ n, Set.Ico a ↑n = Set.Ici a \ {⊤}
<GOAL>⋂ n, Set.Ici ↑n = {⊤}
<GOAL>⋂ n, Set.Ioi ↑n = {⊤}
<VAR>r p : ℝ≥0<GOAL>↑(min r p) = min ↑r ↑p
<VAR>r p : ℝ≥0<GOAL>↑(max r p) = max ↑r ↑p
<VAR>a b : ℝ≥0∞<VAR>h : a = ⊤ → b = ⊤<VAR>h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal<GOAL>a ≤ b
<VAR>x : ℝ≥0∞<GOAL>|x.toReal| = x.toReal
<VAR>s : Set ℝ≥0<GOAL>BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
<VAR>s : Set ℝ≥0<VAR>hs : s.Nonempty<GOAL>↑(sInf s) = ⨅ a ∈ s, ↑a
<VAR>ι : Sort u_3<VAR>f : ι → ℝ≥0<VAR>hf : BddAbove (Set.range f)<GOAL>↑(iSup f) = ⨆ a, ↑(f a)
<VAR>ι : Sort u_3<VAR>Nonempty ι<VAR>f : ι → ℝ≥0<GOAL>↑(iInf f) = ⨅ a, ↑(f a)
<VAR>r : ℝ≥0<VAR>s : Set ℝ≥0<GOAL>↑r ∈ upperBounds (ENNReal.ofNNReal '' s) ↔ r ∈ upperBounds s
<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0<GOAL>⨆ i, ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)
<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0<GOAL>⨆ i, ↑(f i) < ⊤ ↔ BddAbove (Set.range f)
<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0<GOAL>⨅ i, ↑(f i) = ⊤ ↔ IsEmpty ι
<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0<GOAL>⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
<VAR>u : Set ℝ≥0∞<VAR>h : u.OrdConnected<GOAL>(ENNReal.ofNNReal ⁻¹' u).OrdConnected
<VAR>t : Set ℝ≥0<VAR>h : t.OrdConnected<GOAL>(ENNReal.ofNNReal '' t).OrdConnected
<VAR>u : Set ℝ≥0∞<VAR>h : u.OrdConnected<GOAL>(ENNReal.ofReal ⁻¹' u).OrdConnected
<VAR>s : Set ℝ<VAR>h : s.OrdConnected<GOAL>(ENNReal.ofReal '' s).OrdConnected
<VAR>k p n : ℕ<GOAL>Nat.maxPowDiv.go (k + 1) p n = Nat.maxPowDiv.go k p n + 1
<VAR>n : ℕ<GOAL>Nat.maxPowDiv 0 n = 0
<VAR>p : ℕ<GOAL>p.maxPowDiv 0 = 0
<VAR>p n exp : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<GOAL>p.maxPowDiv (p ^ exp * n) = p.maxPowDiv n + exp
<VAR>p n : ℕ<GOAL>p ^ p.maxPowDiv n ∣ n
<VAR>p n pow : ℕ<VAR>hp : 1 < p<VAR>hn : 0 < n<VAR>h : p ^ pow ∣ n<GOAL>pow ≤ p.maxPowDiv n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>H : ∃ n, p n<GOAL>p (Nat.find H)
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>H : ∃ n, p n<VAR>m : ℕ<GOAL>m < Nat.find H → ¬p m
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>H : ∃ n, p n<VAR>m : ℕ<VAR>h : p m<GOAL>Nat.find H ≤ m
<VAR>m : ℕ<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>Nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ<GOAL>Nat.find h < n ↔ ∃ m, m < n ∧ p m
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ<GOAL>Nat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ<GOAL>n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>n : ℕ<GOAL>n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>Nat.find h = 0 ↔ p 0
<VAR>p q : ℕ → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>h : ∀ (n : ℕ), q n → p n<VAR>hp : ∃ n, p n<VAR>hq : ∃ n, q n<GOAL>Nat.find hp ≤ Nat.find hq
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<VAR>hn : p n<GOAL>Nat.find h ≤ n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h₁ : ∃ n, p n<VAR>h₂ : ∃ n, p (n + 1)<VAR>h0 : ¬p 0<GOAL>Nat.find h₁ = Nat.find h₂ + 1
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>0 < Nat.find h ↔ ¬p 0
<VAR>n : ℕ<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hₘ : ∃ m, p (m + n)<VAR>hₙ : ∃ n, p n<VAR>hn : n ≤ Nat.find hₙ<GOAL>Nat.find hₘ + n = Nat.find hₙ
<VAR>P : ℕ → Prop<VAR>DecidablePred P<GOAL>Nat.findGreatest P 0 = 0
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<GOAL>Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<GOAL>P n → Nat.findGreatest P n = n
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>h : ¬P (n + 1)<GOAL>Nat.findGreatest P (n + 1) = Nat.findGreatest P n
<VAR>m k : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<GOAL>Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
<VAR>k : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<GOAL>Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n
<VAR>k : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<GOAL>0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
<VAR>m : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>hmb : m ≤ n<VAR>hm : P m<GOAL>P (Nat.findGreatest P n)
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<GOAL>Nat.findGreatest P n ≤ n
<VAR>m : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>hmb : m ≤ n<VAR>hm : P m<GOAL>m ≤ Nat.findGreatest P n
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>Nat.findGreatest P m ≤ Nat.findGreatest P n
<VAR>P Q : ℕ → Prop<VAR>DecidablePred P<VAR>DecidablePred Q<VAR>hPQ : ∀ (n : ℕ), P n → Q n<VAR>n : ℕ<GOAL>Nat.findGreatest P n ≤ Nat.findGreatest Q n
<VAR>m : ℕ<VAR>P Q : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>DecidablePred Q<VAR>hPQ : ∀ (n : ℕ), P n → Q n<VAR>hmn : m ≤ n<GOAL>Nat.findGreatest P m ≤ Nat.findGreatest Q n
<VAR>k : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>hk : Nat.findGreatest P n < k<VAR>hkb : k ≤ n<GOAL>¬P k
<VAR>m : ℕ<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>h : Nat.findGreatest P n = m<VAR>h0 : m ≠ 0<GOAL>P m
<VAR>n m : ℕ<VAR>h : n.dist m = 0<GOAL>n = m
<VAR>n : ℕ<GOAL>n.dist 0 = n
<VAR>n : ℕ<GOAL>Nat.dist 0 n = n
<VAR>n k m : ℕ<GOAL>(n + k).dist (m + k) = n.dist m
<VAR>n m k l : ℕ<VAR>h : n + m = k + l<GOAL>n.dist k = l.dist m
<VAR>n m k : ℕ<GOAL>n.dist k ≤ n.dist m + m.dist k
<VAR>i j : ℕ<GOAL>i.dist j = max i j - min i j
<VAR>i j : ℕ<GOAL>i ≠ j → 0 < i.dist j
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>(a + b).toReal = a.toReal + b.toReal
<VAR>a b : ℝ≥0∞<VAR>h : b ≤ a<VAR>ha : a ≠ ⊤<GOAL>(a - b).toReal = a.toReal - b.toReal
<VAR>a b : ℝ≥0∞<VAR>hb : b ≠ ⊤<GOAL>a.toReal - b.toReal ≤ (a - b).toReal
<VAR>a b : ℝ≥0∞<GOAL>(a + b).toReal ≤ a.toReal + b.toReal
<VAR>p q : ℝ<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
<VAR>p q : ℝ<GOAL>ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a.toReal ≤ b.toReal ↔ a ≤ b
<VAR>a b : ℝ≥0∞<VAR>hb : b ≠ ⊤<VAR>h : a ≤ b<GOAL>a.toReal ≤ b.toReal
<VAR>a b : ℝ≥0∞<VAR>h : a ≤ b<VAR>ht : b = ⊤ → a = ⊤<GOAL>a.toReal ≤ b.toReal
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a.toReal < b.toReal ↔ a < b
<VAR>a b : ℝ≥0∞<VAR>hb : b ≠ ⊤<VAR>h : a < b<GOAL>a.toReal < b.toReal
<VAR>a b : ℝ≥0∞<VAR>hb : b ≠ ⊤<VAR>h : a ≤ b<GOAL>a.toNNReal ≤ b.toNNReal
<VAR>a : ℝ≥0∞<VAR>p : ℝ≥0<VAR>h : ↑p ≤ a<VAR>ha : a ≠ ⊤<GOAL>p ≤ a.toNNReal
<VAR>a b c : ℝ≥0∞<VAR>hle : a ≤ b + c<VAR>hb : b = ⊤ → a = ⊤<VAR>hc : c = ⊤ → a = ⊤<GOAL>a.toReal ≤ b.toReal + c.toReal
<VAR>a b c : ℝ≥0∞<VAR>hle : a ≤ b + c<VAR>hb : b ≠ ⊤<VAR>hc : c ≠ ⊤<GOAL>a.toReal ≤ b.toReal + c.toReal
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a.toNNReal ≤ b.toNNReal ↔ a ≤ b
<VAR>a b : ℝ≥0∞<VAR>hb : b ≠ ⊤<VAR>h : a < b<GOAL>a.toNNReal < b.toNNReal
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a.toNNReal < b.toNNReal ↔ a < b
<VAR>a : ℝ≥0∞<VAR>p : ℝ≥0<VAR>h : a < ↑p<GOAL>a.toNNReal < p
<VAR>a b : ℝ≥0∞<VAR>hr : a ≠ ⊤<VAR>hp : b ≠ ⊤<GOAL>(max a b).toReal = max a.toReal b.toReal
<VAR>a b : ℝ≥0∞<VAR>hr : a ≠ ⊤<VAR>hp : b ≠ ⊤<GOAL>(min a b).toReal = min a.toReal b.toReal
<VAR>a b : ℝ≥0∞<GOAL>a ≠ ⊤ → b ≠ ⊤ → (a ⊔ b).toReal = a.toReal ⊔ b.toReal
<VAR>a b : ℝ≥0∞<GOAL>a ≠ ⊤ → b ≠ ⊤ → (a ⊓ b).toReal = a.toReal ⊓ b.toReal
<VAR>a : ℝ≥0∞<GOAL>0 < a.toNNReal ↔ 0 < a ∧ a < ⊤
<VAR>a : ℝ≥0∞<VAR>ha₀ : a ≠ 0<VAR>ha_top : a ≠ ⊤<GOAL>0 < a.toNNReal
<VAR>a : ℝ≥0∞<GOAL>0 < a.toReal ↔ 0 < a ∧ a < ⊤
<VAR>a : ℝ≥0∞<VAR>ha₀ : a ≠ 0<VAR>ha_top : a ≠ ⊤<GOAL>0 < a.toReal
<VAR>p q : ℝ<VAR>h : p ≤ q<GOAL>ENNReal.ofReal p ≤ ENNReal.ofReal q
<VAR>a : ℝ<VAR>b : ℝ≥0∞<VAR>h : a ≤ b.toReal<GOAL>ENNReal.ofReal a ≤ b
<VAR>p q : ℝ<VAR>h : 0 ≤ q<GOAL>ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
<VAR>p q : ℝ<GOAL>ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0
<VAR>p q : ℝ<GOAL>ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q
<VAR>p q : ℝ<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
<VAR>p q : ℝ<VAR>h : 0 < q<GOAL>ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
<VAR>p q : ℝ<VAR>hp : 0 ≤ p<GOAL>ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
<VAR>p : ℝ<GOAL>0 < ENNReal.ofReal p ↔ 0 < p
<VAR>p : ℝ<GOAL>ENNReal.ofReal p = 0 ↔ p ≤ 0
<VAR>p : ℝ<GOAL>0 = ENNReal.ofReal p ↔ p ≤ 0
<VAR>p : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>ENNReal.ofReal p < ↑n ↔ p < ↑n
<VAR>p : ℝ<GOAL>ENNReal.ofReal p < 1 ↔ p < 1
<VAR>p : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n
<VAR>n : ℕ<VAR>p : ℝ<VAR>hn : n ≠ 0<GOAL>↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p
<VAR>p : ℝ<GOAL>1 ≤ ENNReal.ofReal p ↔ 1 ≤ p
<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>p : ℝ<GOAL>OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p
<VAR>r : ℝ<VAR>n : ℕ<GOAL>ENNReal.ofReal r ≤ ↑n ↔ r ≤ ↑n
<VAR>r : ℝ<GOAL>ENNReal.ofReal r ≤ 1 ↔ r ≤ 1
<VAR>r : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n
<VAR>n : ℕ<VAR>r : ℝ<GOAL>↑n < ENNReal.ofReal r ↔ ↑n < r
<VAR>r : ℝ<GOAL>1 < ENNReal.ofReal r ↔ 1 < r
<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>r : ℝ<GOAL>OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r
<VAR>r : ℝ<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>ENNReal.ofReal r = ↑n ↔ r = ↑n
<VAR>r : ℝ<GOAL>ENNReal.ofReal r = 1 ↔ r = 1
<VAR>r : ℝ<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n
<VAR>p : ℝ<VAR>q : ℝ<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
<VAR>a : ℝ<VAR>b : ℝ≥0∞<VAR>hb : b ≠ ⊤<GOAL>ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal
<VAR>a : ℝ<VAR>b : ℝ≥0∞<VAR>ha : 0 ≤ a<VAR>hb : b ≠ ⊤<GOAL>ENNReal.ofReal a < b ↔ a < b.toReal
<VAR>a : ℝ<VAR>b : ℝ≥0<VAR>ha : 0 ≤ a<GOAL>ENNReal.ofReal a < ↑b ↔ a < ↑b
<VAR>a : ℝ≥0∞<VAR>b : ℝ<VAR>ha : a ≠ ⊤<VAR>hb : 0 ≤ b<GOAL>a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b
<VAR>a : ℝ≥0∞<VAR>b : ℝ<VAR>hb : 0 ≤ b<VAR>h : a ≤ ENNReal.ofReal b<GOAL>a.toReal ≤ b
<VAR>a : ℝ≥0∞<VAR>b : ℝ<VAR>ha : a ≠ ⊤<GOAL>a < ENNReal.ofReal b ↔ a.toReal < b
<VAR>a : ℝ≥0∞<VAR>b : ℝ<VAR>h : a < ENNReal.ofReal b<GOAL>a.toReal < b
<VAR>p q : ℝ<VAR>hp : 0 ≤ p<GOAL>ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
<VAR>p q : ℝ<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
<VAR>p : ℝ<VAR>hp : 0 ≤ p<VAR>n : ℕ<GOAL>ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
<VAR>x : ℝ<VAR>n : ℕ<GOAL>ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
<VAR>a b : ℝ≥0∞<GOAL>(a * b).toNNReal = a.toNNReal * b.toNNReal
<VAR>a : ℝ≥0∞<GOAL>(a * ⊤).toNNReal = 0
<VAR>a : ℝ≥0∞<GOAL>(⊤ * a).toNNReal = 0
<VAR>a : ℝ≥0<VAR>b : ℝ≥0∞<GOAL>(a • b).toNNReal = a * b.toNNReal
<VAR>a : ℝ≥0∞<VAR>n : ℕ<GOAL>(a ^ n).toNNReal = a.toNNReal ^ n
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ≥0∞<GOAL>(∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal
<VAR>a b : ℝ≥0∞<GOAL>(a * b).toReal = a.toReal * b.toReal
<VAR>a : ℝ≥0∞<VAR>n : ℕ<GOAL>(n • a).toReal = n • a.toReal
<VAR>a : ℝ≥0∞<VAR>n : ℕ<GOAL>(a ^ n).toReal = a.toReal ^ n
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ≥0∞<GOAL>(∏ i ∈ s, f i).toReal = ∏ i ∈ s, (f i).toReal
<VAR>c : ℝ<VAR>a : ℝ≥0∞<VAR>h : 0 ≤ c<GOAL>(ENNReal.ofReal c * a).toReal = c * a.toReal
<VAR>a : ℝ≥0∞<GOAL>(a * ⊤).toReal = 0
<VAR>a : ℝ≥0∞<GOAL>(⊤ * a).toReal = 0
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<GOAL>a.toReal = b.toReal ↔ a = b
<VAR>r : ℝ≥0<VAR>s : ℝ≥0∞<GOAL>(r • s).toReal = r • s.toReal
<VAR>p : ℝ≥0∞<GOAL>p = 0 ∨ p = ⊤ ∨ 0 < p.toReal
<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<GOAL>p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<GOAL>p = ⊤ ∨ 1 ≤ p.toReal
<VAR>p : ℝ≥0∞<VAR>Fact (1 ≤ p)<GOAL>0 < p.toReal ↔ p ≠ ⊤
<VAR>a : ℝ≥0∞<GOAL>a⁻¹.toNNReal = a.toNNReal⁻¹
<VAR>a b : ℝ≥0∞<GOAL>(a / b).toNNReal = a.toNNReal / b.toNNReal
<VAR>a : ℝ≥0∞<GOAL>a⁻¹.toReal = a.toReal⁻¹
<VAR>a b : ℝ≥0∞<GOAL>(a / b).toReal = a.toReal / b.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>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iInf f).toNNReal = ⨅ i, (f i).toNNReal
<VAR>s : Set ℝ≥0∞<VAR>hs : ∀ r ∈ s, r ≠ ⊤<GOAL>(sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iSup f).toNNReal = ⨆ i, (f i).toNNReal
<VAR>s : Set ℝ≥0∞<VAR>hs : ∀ r ∈ s, r ≠ ⊤<GOAL>(sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iInf f).toReal = ⨅ i, (f i).toReal
<VAR>s : Set ℝ≥0∞<VAR>hf : ∀ r ∈ s, r ≠ ⊤<GOAL>(sInf s).toReal = sInf (ENNReal.toReal '' s)
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iSup f).toReal = ⨆ i, (f i).toReal
<VAR>s : Set ℝ≥0∞<VAR>hf : ∀ r ∈ s, r ≠ ⊤<GOAL>(sSup s).toReal = sSup (ENNReal.toReal '' s)
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>iInf f + a = ⨅ i, f i + a