ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∃ (x : b ∈ adjoin R s), p ⟨b, x⟩
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ x ∈ s, ∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (r : R), ∃ (x : (_root_.algebraMap R A) r ∈ adjoin R s), p ⟨(_root_.algebraMap R A) r, x⟩
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (x y : A), (∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩) → (∃ (x : y ∈ adjoin R s), p ⟨y, x⟩) → ∃ (x_1 : x + y ∈ adjoin R s), p ⟨x + y, x_1⟩
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (x y : A), (∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩) → (∃ (x : y ∈ adjoin R s), p ⟨y, x⟩) → ∃ (x_1 : x * y ∈ adjoin R s), p ⟨x * y, x_1⟩
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (x : A), (∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩) → ∃ (x_1 : Star.star x ∈ adjoin R s), p ⟨Star.star x, x_1⟩
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>f ◁ (ρ_ g).hom = (α_ f g (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<GOAL>RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<GOAL>(↑(hHT.equiv g).1)⁻¹ * g * g⁻¹ ∈ H
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<GOAL>¬IsRightRegular 0 ↔ Nontrivial R
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<GOAL>r z * ‖x‖ ≤ Complex.abs (↑(x 0) * ↑z + ↑(x 1))
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<VAR>hn0 : ‖x‖ ≠ 0<GOAL>r z * ‖x‖ ≤ Complex.abs (↑(x 0) * ↑z + ↑(x 1))
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<VAR>hn0 : ‖x‖ ≠ 0<VAR>h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖<GOAL>r z * ‖x‖ ≤ Complex.abs (↑(x 0) * ↑z + ↑(x 1))
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<VAR>hn0 : ‖x‖ ≠ 0<VAR>h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖<GOAL>r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ Complex.abs (↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)) * ↑(max (x 0).natAbs (x 1).natAbs)
<VAR>R : Type u<VAR>ι : Type v<VAR>n : ℕ<VAR>M✝ : Fin n.succ → Type w<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>M₄ : Type w₄<VAR>M : Type u_1<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ContinuousMul R<VAR>inst✝ : ContinuousSMul R M<VAR>z : M<GOAL>ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<GOAL>CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0<GOAL>CharZero R
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0<VAR>p : ℕ := ringChar R<GOAL>CharZero R
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ<GOAL>Supermartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ<GOAL>Supermartingale (- -f) 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ<GOAL>∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, (-f) i ω ∂μ ≤ ∫ (ω : Ω) in s, (-f) (i + 1) ω ∂μ
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<GOAL>ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>x.num * q = p * x.denom ↔ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) (x.num * q) = (algebraMap K[X] (RatFunc K)) (p * x.denom) ↔ x * (algebraMap K[X] (RatFunc K)) q = (algebraMap K[X] (RatFunc K)) p
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) (x.num * q) = (algebraMap K[X] (RatFunc K)) (p * x.denom) ↔ (algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom * (algebraMap K[X] (RatFunc K)) q = (algebraMap K[X] (RatFunc K)) p
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) x.denom ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I : Box ι<GOAL>(volume ↑I).toReal = ∏ i : ι, (I.upper i - I.lower i)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>(o.oangle x (-y)).sign = -(o.oangle x y).sign
<GOAL>Tendsto stirlingSeq atTop (𝓝 √π)
<VAR>a : ℝ<VAR>hapos : 0 < a<VAR>halimit : Tendsto stirlingSeq atTop (𝓝 a)<GOAL>Tendsto stirlingSeq atTop (𝓝 √π)
<VAR>a : ℝ<VAR>hapos : 0 < a<VAR>halimit : Tendsto stirlingSeq atTop (𝓝 a)<VAR>hπ : π / 2 = a ^ 2 / 2<GOAL>Tendsto stirlingSeq atTop (𝓝 √π)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<GOAL>iteratedDeriv (n + 1) f x = deriv (iteratedDeriv n f) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<GOAL>iteratedDerivWithin (n + 1) f univ x = derivWithin (iteratedDerivWithin n f univ) univ x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>U : Over X<VAR>S : Sieve U<VAR>hS : S ∈ (J.over X).sieves U<GOAL>Sieve.functorPushforward (Over.map f) S ∈ (J.over Y).sieves ((Over.map f).obj U)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>U : Over X<VAR>S : Sieve U.left<VAR>hS : (Sieve.overEquiv U).symm S ∈ (J.over X).sieves U<GOAL>Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv U).symm S) ∈ (J.over Y).sieves ((Over.map f).obj U)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>U : Over X<VAR>S : Sieve U.left<VAR>hS : (Sieve.overEquiv U).symm S ∈ (J.over X).sieves U<GOAL>(Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y).sieves ((Over.map f).obj U)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>U : Over X<VAR>S : Sieve U.left<VAR>hS : (Sieve.overEquiv U).symm S ∈ (J.over X).sieves U<GOAL>S ∈ J.sieves ((Over.map f).obj U).left
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>κ : Type u_6<VAR>inst✝ : Fintype κ<VAR>f : Matrix ι ι R<GOAL>LinearMap.det (toLin' f) = f.det
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>eLpNorm f_lim ⊤ μ = essSup (fun x => liminf (fun m => ↑‖f m x‖₊) atTop) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>essSup (fun x => ↑‖f_lim x‖₊) μ = essSup (fun x => liminf (fun m => ↑‖f m x‖₊) atTop) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>x : α<VAR>hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>(fun x => ↑‖f_lim x‖₊) x = (fun x => liminf (fun m => ↑‖f m x‖₊) atTop) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>x : α<VAR>hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>↑‖f_lim x‖₊ = liminf (fun m => ↑‖f m x‖₊) atTop
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>x : α<VAR>hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>Tendsto (fun m => ↑‖f m x‖₊) atTop (𝓝 ↑‖f_lim x‖₊)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>x : α<VAR>hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>Tendsto (fun m => ‖f m x‖₊) atTop (𝓝 ‖f_lim x‖₊)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>h : Disjoint (support f) (support g)<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<GOAL>Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>h : Disjoint (support f) (support g)<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>hfg : Integrable (f + g) μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>h : Disjoint (support f) (support g)<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>hfg : Integrable (f + g) μ<GOAL>Integrable g μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a ≤ 1 / b ↔ b ≤ a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>inst✝ : Nonempty α<VAR>f : ↥(lp E ⊤)<VAR>C : ℝ<VAR>hCf : ∀ (i : α), ‖↑f i‖ ≤ C<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>inst✝ : Nonempty α<VAR>f : ↥(lp E ⊤)<VAR>C : ℝ<VAR>hCf : ∀ (i : α), ‖↑f i‖ ≤ C<GOAL>C ∈ upperBounds (Set.range fun i => ‖↑f i‖)
<VAR>X : TopCat<VAR>U : Opens ↑X<VAR>R : Presieve U<VAR>hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U<GOAL>iSup (coveringOfPresieve U R) = U
<VAR>X : TopCat<VAR>U : Opens ↑X<VAR>R : Presieve U<VAR>hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U<GOAL>iSup (coveringOfPresieve U R) ≤ U
<VAR>X : TopCat<VAR>U : Opens ↑X<VAR>R : Presieve U<VAR>hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U<GOAL>U ≤ iSup (coveringOfPresieve U R)
<VAR>X : TopCat<VAR>U : Opens ↑X<VAR>R : Presieve U<VAR>hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U<VAR>x : ↑X<VAR>hxU : x ∈ ↑U<GOAL>x ∈ ↑(iSup (coveringOfPresieve U R))
<VAR>X : TopCat<VAR>U : Opens ↑X<VAR>R : Presieve U<VAR>hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U<VAR>x : ↑X<VAR>hxU : x ∈ ↑U<GOAL>∃ i, x ∈ ↑(coveringOfPresieve U R i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ioc a b = ∅ ↔ ¬a < b
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0<GOAL>(∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x y z : α<GOAL>y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X X' Y Y' Z Z' : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : X ⟶ Y ⊗ Z<VAR>g : X' ⟶ Z'<GOAL>(tensorLeftHomEquiv (X ⊗ X') Y Y' (Z ⊗ Z')).symm ((f ⊗ g) ≫ (α_ Y Z Z').hom) = (α_ Y' X X').inv ≫ ((tensorLeftHomEquiv X Y Y' Z).symm f ⊗ g)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<GOAL>ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr
<VAR>P : MorphismProperty Scheme<VAR>inst✝¹ : IsLocalAtSource P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : X.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → X.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P ((U i).ι ≫ f)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>inst✝¹ : IsLocalAtSource P<VAR>X Y U✝ V : Scheme<VAR>f : X ⟶ Y<VAR>g : U✝ ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : X.OpenCover<VAR>ι : Sort u_1<VAR>U : ι → X.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P ((U i).ι ≫ f)<VAR>i : (X.openCoverOfISupEqTop Subtype.val ⋯).J<GOAL>P ((X.openCoverOfISupEqTop Subtype.val ⋯).map i ≫ f)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>R : D ⥤ C<VAR>inst✝¹ : Reflective R<VAR>inst✝ : HasColimitsOfShape J C<VAR>F : J ⥤ D<VAR>c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))<VAR>this : PreservesColimitsOfShape J (monadicLeftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape<VAR>t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit (F ⋙ R))<GOAL>HasColimit F
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>R : D ⥤ C<VAR>inst✝¹ : Reflective R<VAR>inst✝ : HasColimitsOfShape J C<VAR>F : J ⥤ D<VAR>c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))<VAR>this : PreservesColimitsOfShape J (monadicLeftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape<VAR>t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit (F ⋙ R))<GOAL>(F ⋙ R) ⋙ monadicLeftAdjoint R ≅ F
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝ : Fintype ↑M.verts<VAR>h : M.IsMatching<GOAL>Even M.verts.toFinset.card
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<GOAL>(↑↑l).head! = term I ho
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<GOAL>ord I (↑↑l).head! = o
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<VAR>hm : term I ho ∈ ↑↑l<GOAL>ord I (↑↑l).head! = o
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<VAR>hm : term I ho ∈ ↑↑l<VAR>this : ord I (↑↑l).head! < Order.succ o<GOAL>ord I (↑↑l).head! = o
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<VAR>hm : term I ho ∈ ↑↑l<VAR>this : ord I (↑↑l).head! ≤ o<GOAL>ord I (↑↑l).head! = o
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<VAR>hm : term I ho ∈ ↑↑l<VAR>this : ord I (↑↑l).head! ≤ o<GOAL>o ≤ ord I (↑↑l).head!
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : ↑(MaxProducts C ho)<VAR>hm : term I ho ∈ ↑↑l<VAR>this : ord I (↑↑l).head! ≤ o<VAR>h : ord I (term I ho) ≤ ord I (↑↑l).head!<GOAL>o ≤ ord I (↑↑l).head!
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>k : ℕ<VAR>x : α<GOAL>x ≤ succ^[k] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>k : ℕ<VAR>x : α<GOAL>id^[k] x ≤ succ^[k] x
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>h₁ : x ≤ y<VAR>h₂ : y ≤ x<GOAL>x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>h₁ : x ≤ y<VAR>h₂ : x ⧏ y<GOAL>x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y