ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : IsModularLattice α<VAR>inst✝¹ : ComplementedLattice α<VAR>inst✝ : IsAtomic α<VAR>a b : α<VAR>hab : a < b<VAR>a' : α<VAR>ha'b : a' ≤ b<VAR>ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩<VAR>d : α<VAR>hd : IsAtom d ∧ d ≤ a'<GOAL>a ⊓ d ≤ a ⊓ a'
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>f : M →ₗ[R] N<VAR>h : SameRay R x y<VAR>hx : x = 0<GOAL>f x = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>f : M →ₗ[R] N<VAR>h : SameRay R x y<VAR>hy : y = 0<GOAL>f y = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>f : M →ₗ[R] N<VAR>h✝ : SameRay R x y<VAR>x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y<VAR>r₁ r₂ : R<VAR>hr₁ : 0 < r₁<VAR>hr₂ : 0 < r₂<VAR>h : r₁ • x = r₂ • y<GOAL>r₁ • f x = r₂ • f y
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>x : E<GOAL>edist x 1 = ↑‖x‖₊
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>ρ : Measure (α × β)<VAR>inst✝ : IsProbabilityMeasure μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν).snd s = ν s
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p ≠ 0<GOAL>p.degree = ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p ≠ 0<VAR>n : ℕ<VAR>hn : ¬n ∉ p.degree<GOAL>p.degree = ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p ≠ 0<VAR>n : ℕ<VAR>hn✝ : ¬n ∉ p.degree<VAR>hn : p.degree = Option.some n<GOAL>p.degree = ↑p.natDegree
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<GOAL>∃ π, v.valuation π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>hr : v.intValuationDef r = ↑(ofAdd (-1))<GOAL>∃ π, v.valuation π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>hr : v.intValuationDef r = ↑(ofAdd (-1))<GOAL>v.valuation ((algebraMap R K) r) = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>hr : v.intValuationDef r = ↑(ofAdd (-1))<GOAL>v.intValuation r = ↑(ofAdd (-1))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : SemilatticeInf γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsGLB s b<GOAL>IsGLB (insert a s) (a ⊓ b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : SemilatticeInf γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsGLB s b<GOAL>IsGLB ({a} ∪ s) (a ⊓ b)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<GOAL>atTop = ⨅ x, 𝓟 (Ici {x})
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<GOAL>⨅ x, 𝓟 (Ici {x}) ≤ atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<GOAL>⋂ i, Ici {↑i} ⊆ Ici s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Finset α<GOAL>∀ (x : Finset α), (∀ x_1 ∈ ↑s, x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m✝ : Multiset ι<VAR>f g : ι → α<VAR>m : Multiset α<GOAL>(0 • m).prod = m.prod ^ 0
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m✝ : Multiset ι<VAR>f g : ι → α<VAR>m : Multiset α<GOAL>prod 0 = 1
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m✝ : Multiset ι<VAR>f g : ι → α<VAR>m : Multiset α<VAR>n : ℕ<GOAL>((n + 1) • m).prod = m.prod ^ (n + 1)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p q : Submodule R M<VAR>x : M<GOAL>x ∈ p ⊔ q ↔ x ∈ range (p.subtype.coprod q.subtype)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g✝ : α → Multiset β<VAR>f : α → β<VAR>g : α → Multiset β<GOAL>∀ (a : α) (s : Multiset α), (s.bind fun a => f a ::ₘ g a) = map f s + s.bind g → ((a ::ₘ s).bind fun a => f a ::ₘ g a) = map f (a ::ₘ s) + (a ::ₘ s).bind g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G H : D ⥤ E<VAR>α : G ⟶ H<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(F ⋙ G).map f ≫ (fun X => α.app (F.obj X)) Y = (fun X => α.app (F.obj X)) X ≫ (F ⋙ H).map f
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : SecondCountableTopology α<VAR>hclosed : IsClosed C<VAR>hunc : ¬C.Countable<GOAL>∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : SecondCountableTopology α<VAR>hclosed : IsClosed C<VAR>hunc : ¬C.Countable<VAR>V D : Set α<VAR>Vct : V.Countable<VAR>Dperf : Perfect D<VAR>VD : C = V ∪ D<GOAL>∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : SecondCountableTopology α<VAR>hclosed : IsClosed C<VAR>hunc : ¬C.Countable<VAR>V D : Set α<VAR>Vct : V.Countable<VAR>Dperf : Perfect D<VAR>VD : C = V ∪ D<GOAL>D ⊆ V ∪ D
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>t : IsSeparatedFor P R<GOAL>(∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) → IsSheafFor P R
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>t : IsSeparatedFor P R<GOAL>(∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) → IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<GOAL>factorThruImageSubobject f ≫ (imageSubobject f).arrow = f
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<VAR>x : α<VAR>h : x ∈ s<GOAL>map f (s.erase x) = (map f s).erase (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>x : α<VAR>h : x ∈ 0<GOAL>map f (erase 0 x) = (map f 0).erase (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>x y : α<VAR>s : Multiset α<VAR>ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)<VAR>h : x ∈ y ::ₘ s<GOAL>map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>y : α<VAR>s : Multiset α<VAR>ih : y ∈ s → map f (s.erase y) = (map f s).erase (f y)<VAR>h : y ∈ y ::ₘ s<GOAL>map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>x y : α<VAR>s : Multiset α<VAR>ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)<VAR>h : x ∈ y ::ₘ s<VAR>hxy : y ≠ x<GOAL>map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>x y : α<VAR>s : Multiset α<VAR>ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)<VAR>hxy : y ≠ x<VAR>h : x ∈ s<GOAL>map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>T : Type u_4<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>(map σ f) ((monomial R n) a) = (monomial S n) (f a)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>m n✝ n : ℕ<GOAL>1 ^ (n + 1) = 1
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x ⧏ y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>((¬∀ (i : y.LeftMoves), y.moveLeft i ⧏ x) ∨ ¬∀ (j : x.RightMoves), y ⧏ x.moveRight j) ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y
<VAR>s r : ℝ<VAR>hs : s < 0<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 1<GOAL>x ∈ {x | (fun x => ((fun x => log x ^ r) ∘ fun x => x⁻¹) x = (fun x => |log x| ^ r) x) x}
<VAR>s r : ℝ<VAR>hs : s < 0<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioi 0<GOAL>((fun x => x ^ (-s)) ∘ fun x => x⁻¹) x = (fun x => x ^ s) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>h1 : a < 0<VAR>h2 : -1 < a<VAR>this : 1 / a < 1 / -1<GOAL>1 / a < -1
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Finset α<GOAL>⋯.toFinset = s
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K✝ H K : Subgroup G<VAR>h : H ≤ K<VAR>val✝ : G<VAR>property✝ : val✝ ∈ H<GOAL>↑((inclusion h) ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<GOAL>filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>f✝ g✝ : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : TopologicalSpace γ<VAR>f : α →ᵇ β<VAR>g : C(γ, α)<GOAL>↑1 * dist f 0 ≤ ‖f‖
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁷ : SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace M₁<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module 𝕜₁ M₁<VAR>inst✝¹ : Module 𝕜₂ M₂<VAR>inst✝ : ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : IsVonNBounded 𝕜₁ S<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))<GOAL>⇑f '' S ⊆ σ₁₂ c • K
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁷ : SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁶ : TopologicalSpace M₁<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module 𝕜₁ M₁<VAR>inst✝¹ : Module 𝕜₂ M₂<VAR>inst✝ : ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : IsVonNBounded 𝕜₁ S<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : ⇑f ⁻¹' K ∈ 𝓝 0<VAR>r : ℝ<VAR>hr : r > 0<VAR>hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K<VAR>c : 𝕜₁<VAR>hc : r < ‖c‖<VAR>this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))<GOAL>S ⊆ c • ⇑f ⁻¹' K
<VAR>f g : ℍ → ℂ<VAR>hf : IsBoundedAtImInfty f<VAR>hg : IsBoundedAtImInfty g<GOAL>IsBoundedAtImInfty (f * g)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).Ψ n = Polynomial.map (mapRingHom f) (W.Ψ n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(C ((mapRingHom f) (W.preΨ n)) * if Even n then (mapRingHom (mapRingHom f)) W.ψ₂ else 1) = (mapRingHom (mapRingHom f)) (C (W.preΨ n) * if Even n then W.ψ₂ else 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<GOAL>(⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<GOAL>(lsub f).cof ≤ #ι
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<GOAL>sInf {a | ∃ ι_1 f_1, lsub f_1 = lsub f ∧ #ι_1 = a} ≤ #ι
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g • t = t<VAR>hts : μ (t ∩ s) = 0<GOAL>μ t = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g • t = t<VAR>hts : μ (t ∩ s) = 0<GOAL>∑' (g : G), μ (g • t ∩ s) = 0
<VAR>b m n : ℕ<VAR>h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0<VAR>hbn : ¬(1 < b ∧ n ≠ 0)<GOAL>log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
<VAR>b m n : ℕ<VAR>h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0<VAR>hbn : ¬(1 < b ∧ n ≠ 0)<VAR>hm : m ≠ 0<GOAL>log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
<VAR>b m n : ℕ<VAR>h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0<VAR>hbn : b ≤ 1 ∨ n = 0<VAR>hm : m ≠ 0<GOAL>log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>Ico a b ∪ Ico b c = Ico a c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset ℕ<VAR>n : ℕ<GOAL>∀ {a b : ℕ}, { toFun := fun n => { ofColex := equivBitIndices n }, invFun := fun s => equivBitIndices.symm s.ofColex, left_inv := ⋯, right_inv := ⋯ } a ≤ { toFun := fun n => { ofColex := equivBitIndices n }, invFun := fun s => equivBitIndices.symm s.ofColex, left_inv := ⋯, right_inv := ⋯ } b ↔ a ≤ b
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>i j : J<GOAL>Continuous fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>i j : J<GOAL>Continuous fun x => ⟨↑↑x, ⋯⟩
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>i j : J<GOAL>Continuous fun x => ↑↑x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>hf : IsField R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>∃! y, x * y = 1
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>hf : IsField R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>∃ x_1, x * x_1 = 1
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>hf : IsField R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b : α<VAR>n : ℕ<VAR>a : α<GOAL>mabs (a ^ n) = mabs a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b : α<VAR>n : ℕ<VAR>a : α<VAR>ha : a ≤ 1<GOAL>mabs (a ^ n) = mabs a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b : α<VAR>n : ℕ<VAR>a : α<VAR>ha : 1 ≤ a<GOAL>mabs (a ^ n) = mabs a ^ n
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>hg : ∀ {x : β}, g x = 1 ↔ x = 1<GOAL>HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : upperCrossingTime a b f N (n + 1) ω < N<GOAL>upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧ lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : upperCrossingTime a b f N (n + 1) ω < N<VAR>this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω<GOAL>upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧ lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : upperCrossingTime a b f N (n + 1) ω < N<VAR>this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω<GOAL>upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : upperCrossingTime a b f N (n + 1) ω < N<VAR>this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω<GOAL>hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) M ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : upperCrossingTime a b f N (n + 1) ω < N<VAR>this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω<GOAL>∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : ∃ j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b<VAR>this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω<GOAL>∃ j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N, f j ω ∈ Set.Ici b
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N<VAR>this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω<GOAL>N ≤ N
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<GOAL>ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (addBottom L) = L
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<GOAL>ListBlank.cons L.head (ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) = L
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<GOAL>ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) = L.tail
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L L' : ListBlank ((k : K) → Option (Γ k))<GOAL>ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L') = L'
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L L' : ListBlank ((k : K) → Option (Γ k))<VAR>l : List ((k : K) → Option (Γ k))<GOAL>ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.mk l)) = ListBlank.mk l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝¹ l₁ l₂ : List M<VAR>a✝ : M<VAR>l✝ : List ι<VAR>r : M → N → Prop<VAR>f : ι → M<VAR>g : ι → N<VAR>h₁ : r 1 1<VAR>h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)<VAR>a : ι<VAR>l : List ι<VAR>hl : r (map f l).prod (map g l).prod<GOAL>r (map f (a :: l)).prod (map g (a :: l)).prod
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<VAR>this : ∀ x ∈ K, ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι : Sort u_2<VAR>U : ι → Set α<VAR>hK : IsCompact K<VAR>hopen : ∀ (i : ι), IsOpen (U i)<VAR>hcover : K ⊆ ⋃ i, U i<VAR>ind : (x : α) → x ∈ K → ι<VAR>W : (x : α) → x ∈ K → Set (α × α)<VAR>hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α<VAR>hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i