ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝ : AddCommGroup G<VAR>B : AddGroupFilterBasis G<VAR>F : Filter G<VAR>this✝ : UniformSpace G := B.uniformSpace<VAR>this : UniformAddGroup G<GOAL>Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
<VAR>G : Type u_1<VAR>inst✝ : AddCommGroup G<VAR>B : AddGroupFilterBasis G<VAR>F : Filter G<VAR>this✝ : UniformSpace G := B.uniformSpace<VAR>this : UniformAddGroup G<GOAL>F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
<VAR>G : Type u_1<VAR>inst✝ : AddCommGroup G<VAR>B : AddGroupFilterBasis G<VAR>F : Filter G<VAR>this✝ : UniformSpace G := B.uniformSpace<VAR>this : UniformAddGroup G<GOAL>map (fun x => x.2 - x.1) (F ×ˢ F) ≤ nhds 0 ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
<VAR>G : Type u_1<VAR>inst✝ : AddCommGroup G<VAR>B : AddGroupFilterBasis G<VAR>F : Filter G<VAR>this✝ : UniformSpace G := B.uniformSpace<VAR>this : UniformAddGroup G<GOAL>Tendsto (fun x => x.2 - x.1) (F ×ˢ F) (nhds 0) ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<GOAL>(a + b) / 2 < b ↔ a < b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>⋃ n, Icc (a + ↑n) (a + ↑n + 1) = univ
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x z d : R<VAR>h : IsCoprime (x * d) z<GOAL>IsCoprime x z
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>cond : f ≫ g = 0<VAR>x : ↑Y<GOAL>(explicitCokernelπ f ≫ explicitCokernelDesc cond) x = g x
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝² : Group α✝<VAR>α : Type u<VAR>inst✝¹ : Group α<VAR>inst✝ : Fintype α<VAR>hp : Fact (Nat.Prime (Fintype.card α))<GOAL>IsSimpleGroup α
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝² : Group α✝<VAR>α : Type u<VAR>inst✝¹ : Group α<VAR>inst✝ : Fintype α<VAR>hp : Fact (Nat.Prime (Fintype.card α))<VAR>this : Nontrivial α<GOAL>IsSimpleGroup α
<VAR>x : ℝ<GOAL>sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * π ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a : α<GOAL>∀ (a : List α), (∀ x ∈ ⟦a⟧, 1 ≤ x) → prod ⟦a⟧ = 1 → ∀ x ∈ ⟦a⟧, x = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a : α<GOAL>∀ (a : List α), (∀ x ∈ a, 1 ≤ x) → a.prod = 1 → ∀ x ∈ a, x = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>P : Sort u_5<VAR>x y x' y' : α<VAR>ltc : x < y ↔ x' < y'<VAR>gtc : y < x ↔ y' < x'<GOAL>x = y ↔ x' = y'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : SemilatticeSup δ<VAR>g : γ → δ<VAR>h : (image₂ f s t).Nonempty<GOAL>(image₂ f s t).sup' h g = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : SemilatticeSup δ<VAR>g : γ → δ<VAR>h : (image₂ f s t).Nonempty<GOAL>(s.sup' ⋯ fun i => t.sup' ⋯ fun i' => (g ∘ uncurry f) (i, i')) = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝³ : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : NonUnitalNonAssocSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).order = x.order + y.order
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝³ : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : NonUnitalNonAssocSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).order ≤ x.order + y.order
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝³ : OrderedCancelAddCommMonoid Γ✝<VAR>Γ : Type u_5<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : NonUnitalNonAssocSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x.order + y.order ≤ (x * y).order
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a = b / c ↔ a * c = b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : P<VAR>h : ∑ i ∈ s, w i = 1<GOAL>(affineCombination k s fun x => p) w = p
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>sb : Bornology.IsBounded s<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<GOAL>μ s = 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>sb : Bornology.IsBounded s<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<VAR>h : ¬μ s = 0<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>sb : Bornology.IsBounded s<VAR>hu : Bornology.IsBounded (range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<VAR>h : ¬μ s = 0<GOAL>⊤ < ⊤
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a / b
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a * b⁻¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module R N<VAR>inst✝¹⁰ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : AddCommGroup P'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N'<VAR>inst✝² : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<VAR>S : Type u_9<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>h : Surjective ⇑(algebraMap R S)<GOAL>Surjective ⇑((mk R S M) 1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module R N<VAR>inst✝¹⁰ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : AddCommGroup P'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N'<VAR>inst✝² : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<VAR>S : Type u_9<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>h : Surjective ⇑(algebraMap R S)<GOAL>{t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑(range ((mk R S M) 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module R N<VAR>inst✝¹⁰ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : AddCommGroup P'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N'<VAR>inst✝² : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<VAR>S : Type u_9<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>h : Surjective ⇑(algebraMap R S)<VAR>y : M<VAR>x : R<GOAL>(algebraMap R S) x ⊗ₜ[R] y ∈ ↑(range ((mk R S M) 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup P<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : Module R N<VAR>inst✝¹⁰ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : AddCommGroup P'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N'<VAR>inst✝² : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<VAR>S : Type u_9<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>h : Surjective ⇑(algebraMap R S)<VAR>y : M<VAR>x : R<GOAL>1 ⊗ₜ[R] (x • y) ∈ ↑(range ((mk R S M) 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : NeZero μ<VAR>c : ℝ≥0∞<GOAL>⨍⁻ (_x : α), c ∂μ = c
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>X : J<VAR>hX : IsTerminal X<VAR>F : J ⥤ C<VAR>inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>𝟙 (F.obj X) ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝² : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>δ : Type u_4<VAR>π : δ → Type u_5<VAR>inst✝¹ : (x : δ) → MeasurableSpace (π x)<VAR>l : List δ<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝ : ∀ (i : δ), SigmaFinite (μ i)<VAR>s : (i : δ) → Set (π i)<GOAL>(Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
<GOAL>¬Summable fun p => 1 / ↑↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set β<VAR>h : Codisjoint s t<GOAL>Codisjoint (f ⁻¹' s) (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set β<VAR>h : s ∪ t = ⊤<GOAL>f ⁻¹' (s ∪ t) = ⊤
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>f : α → γ → δ<VAR>g : β → γ<GOAL>image2 f (↑s) (g '' ↑t) = image2 (fun a b => f a (g b)) ↑s ↑t
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR<GOAL>(lsub fun i => (xL i).birthday) = lsub fun i => (yL i).birthday
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR<GOAL>(lsub fun i => (xR i).birthday) = lsub fun i => (yR i).birthday
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR<VAR>i : Ordinal.{u}<GOAL>(i ∈ Set.range fun i => (xL i).birthday) → i ∈ Set.range fun i => (yL i).birthday
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR<VAR>i : Ordinal.{u}<GOAL>(i ∈ Set.range fun i => (yL i).birthday) → i ∈ Set.range fun i => (xL i).birthday
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR<VAR>i : Ordinal.{u}<GOAL>(i ∈ Set.range fun i => (xR i).birthday) → i ∈ Set.range fun i => (yR i).birthday
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR<VAR>i : Ordinal.{u}<GOAL>(i ∈ Set.range fun i => (yR i).birthday) → i ∈ Set.range fun i => (xR i).birthday
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>f : ι → α<VAR>a : α<GOAL>⋃ i, Ioc a (f i) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x < x + z<GOAL>τ f < z
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x < x + z<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x<GOAL>τ f < z
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x < x + z<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x<GOAL>τ f ≤ f x - x
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x < x + z<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x<GOAL>∀ (x_1 : ℝ), f x_1 ≤ x_1 + (f x - x)
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x < x + z<VAR>x : ℝ<VAR>hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x<GOAL>∀ (x_1 : ℝ), f x_1 - x_1 ≤ f x - x
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>A : Type u_2<VAR>inst✝ : AddGroup A<VAR>K : Subgroup G<GOAL>Nat.card ↥⊥ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>C0 : 0 < C<GOAL>dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>C0 : 0 < C<GOAL>(∀ (x : α), dist ((mkOfCompact f) x) ((mkOfCompact g) x) < C) ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>s : Set G<GOAL>s * ↑(stabilizer G s) = s
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommGroup β<VAR>inst✝ : DecidableEq α<VAR>h : s₁ ⊆ s₂<GOAL>∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m0 m0' : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hm0 : m0 ≤ m0'<VAR>μ : Measure α<VAR>f g : α → β<VAR>hg_meas : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae (μ.trim hm0)] g<GOAL>AEStronglyMeasurable' m f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝² : One β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : MetrizableSpace β<VAR>hf : StronglyMeasurable f<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>MeasurableSet (mulSupport f)
<VAR>α✝ : Type u<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<GOAL>↑(Int.ofNat n) * ⅟↑d = ↑n / ↑d
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.10991, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : IsZero S.X₂<GOAL>S.Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.10991, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : IsZero S.X₂<GOAL>IsZero (HomologyData.ofZeros S ⋯ ⋯).left.H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : R1Space α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : R1Space α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>K : Set α<VAR>hKA : K ⊆ A<VAR>hKco : IsCompact K<VAR>hKcl : IsClosed K<VAR>hK : μ A < μ K + ε<GOAL>∃ K ⊆ A, IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : α → β<VAR>inst✝ : One β<VAR>s : Set α<VAR>c : β<GOAL>EventuallyConst (s.mulIndicator fun x => c) l ↔ c = 1 ∨ EventuallyConst s l
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>(o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>x : E<VAR>s t : Set E<GOAL>StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>x : E<VAR>s t : Set E<GOAL>StarConvex 𝕜 x s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<GOAL>QuasilinearOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<GOAL>(Convex 𝕜 s ∧ (∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>f g : E → β<GOAL>((∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x✝ y a : G<VAR>m n : ℕ<VAR>x : G<VAR>h : ¬IsOfFinOrder x<VAR>s : Set G := (fun n => x ^ n) '' {n | 0 < n}<GOAL>{y | ¬IsOfFinOrder y}.Infinite
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x✝ y a : G<VAR>m n : ℕ<VAR>x : G<VAR>h : ¬IsOfFinOrder x<VAR>s : Set G := (fun n => x ^ n) '' {n | 0 < n}<VAR>hs : s ⊆ {y | ¬IsOfFinOrder y}<GOAL>{y | ¬IsOfFinOrder y}.Infinite
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x✝ y a : G<VAR>m n : ℕ<VAR>x : G<VAR>h : ¬IsOfFinOrder x<VAR>s : Set G := (fun n => x ^ n) '' {n | 0 < n}<VAR>hs : s ⊆ {y | ¬IsOfFinOrder y}<GOAL>s.Infinite
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x✝ y a : G<VAR>m n : ℕ<VAR>x : G<VAR>s : Set G := (fun n => x ^ n) '' {n | 0 < n}<VAR>hs : s ⊆ {y | ¬IsOfFinOrder y}<VAR>h : ¬s.Infinite<GOAL>IsOfFinOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x✝ y a : G<VAR>m n : ℕ<VAR>x : G<VAR>s : Set G := (fun n => x ^ n) '' {n | 0 < n}<VAR>hs : s ⊆ {y | ¬IsOfFinOrder y}<VAR>h : ¬s.Infinite<VAR>this : ¬Injective fun n => x ^ n<GOAL>IsOfFinOrder x
<VAR>F : Type u_1<VAR>inst✝ : CommSemiring F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf✝ : HasSeparableContraction q f<VAR>g : F[X]<VAR>hf : IsSeparableContraction q f g<GOAL>∃ m, g.natDegree * q ^ m = f.natDegree
<VAR>F : Type u_1<VAR>inst✝ : CommSemiring F<VAR>q : ℕ<VAR>g : F[X]<VAR>m : ℕ<VAR>hf✝ : HasSeparableContraction q ((expand F (q ^ m)) g)<VAR>hf : IsSeparableContraction q ((expand F (q ^ m)) g) g<GOAL>∃ m_1, g.natDegree * q ^ m_1 = ((expand F (q ^ m)) g).natDegree
<VAR>F : Type u_1<VAR>inst✝ : CommSemiring F<VAR>q : ℕ<VAR>g : F[X]<VAR>m : ℕ<VAR>hf✝ : HasSeparableContraction q ((expand F (q ^ m)) g)<VAR>hf : IsSeparableContraction q ((expand F (q ^ m)) g) g<GOAL>g.natDegree * q ^ m = ((expand F (q ^ m)) g).natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>↑(toSimpleFunc 0) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>a✝¹ : α<VAR>h₁ : ↑(toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹<VAR>a✝ : ↑↑0 a✝¹ = 0 a✝¹<GOAL>↑(toSimpleFunc 0) a✝¹ = 0 a✝¹