ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : Cardinal.{u_2}<VAR>ha : ℵ₀ ≤ a<VAR>b1 : 1 < b<VAR>b0 : b ≠ 0<GOAL>b ^ a < (b ^ a) ^ (b ^ a).ord.cof
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hcd : IntervalIntegrable f μ c d<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in a..d, f x ∂μ + ∫ (x : ℝ) in c..b, f x ∂μ
<VAR>k : Type u<VAR>inst✝³ : Field k<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>V : FDRep k G<GOAL>⅟↑(Fintype.card G) • ∑ g : G, V.character g = ↑(finrank k ↥(invariants V.ρ))
<VAR>k : Type u<VAR>inst✝³ : Field k<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>V : FDRep k G<GOAL>⅟↑(Fintype.card G) • ∑ g : G, V.character g = (trace k (CoeSort.coe V)) (averageMap V.ρ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>I : Set ι<VAR>t : ι → Set α<VAR>h : I.PairwiseDisjoint t<VAR>hI : I.Finite<VAR>ht : ∀ i ∈ I, (t i).Finite<VAR>this : Fintype ↑I<GOAL>∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>I : Set ι<VAR>t : ι → Set α<VAR>h : I.PairwiseDisjoint t<VAR>hI : I.Finite<VAR>ht : ∀ i ∈ I, (t i).Finite<VAR>this : Fintype ↑I<GOAL>Pairwise (Disjoint on fun x => t ↑x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t✝ : Set α<VAR>I : Set ι<VAR>t : ι → Set α<VAR>h : I.PairwiseDisjoint t<VAR>hI : I.Finite<VAR>ht : ∀ i ∈ I, (t i).Finite<VAR>this : Fintype ↑I<GOAL>∀ (i : ↑I), (t ↑i).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s t : Set α<VAR>f : α → β<GOAL>LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s t : Set α<VAR>f : α → β<GOAL>(∀ (x : ↑s), ∃ K, ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) ↔ ∀ (x : ↑s), ∃ K t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>c : ℝ≥0<VAR>hc : 0 < c<GOAL>∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>this : ∀ᶠ (x : E × E) in 𝓝 (a, a), ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ ≤ (fun a => ↑a) c * ‖x.1 - x.2‖<GOAL>∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>this : ∃ t ∈ 𝓝 a, t ×ˢ t ⊆ {x | ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ ≤ (fun a => ↑a) c * ‖x.1 - x.2‖}<GOAL>∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>s : Set E<VAR>has : s ∈ 𝓝 a<VAR>hs : s ×ˢ s ⊆ {x | ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ ≤ (fun a => ↑a) c * ‖x.1 - x.2‖}<GOAL>∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
<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 ν<GOAL>∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, 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>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>m : ∀ {α : Type ?u.28006} {β : Type ?u.28005} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, 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>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>m : ∀ {α : Type ?u.28006} {β : Type ?u.28005} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄, MeasurableSet s → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (s.indicator fun x => c)
<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>m : ∀ {α : Type ?u.28006} {β : Type ?u.28005} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ ⦃f g : α × β → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) f → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) g → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f + g)
<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>m : ∀ {α : Type ?u.28006} {β : Type ?u.28005} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)) → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) fun x => ⨆ n, f n x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<GOAL>(Matrix.map 1 fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<GOAL>((diagonal fun x => 1).map fun x => X * (algebraMap R R[X]) x) = diagonal fun x => X
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<VAR>l : List α<GOAL>(l.erase a).erase b = (l.erase b).erase a
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<VAR>l : List α<VAR>ab : ¬(a == b) = true<GOAL>(l.erase a).erase b = (l.erase b).erase a
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<VAR>l : List α<VAR>ab : ¬(a == b) = true<VAR>ha : a ∈ l<GOAL>(l.erase a).erase b = (l.erase b).erase a
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<VAR>l : List α<VAR>ab : ¬(a == b) = true<VAR>ha : a ∈ l<VAR>hb : b ∈ l<GOAL>(l.erase a).erase b = (l.erase b).erase a
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Flat R S<VAR>inst✝ : Flat S M<GOAL>Flat R M
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Flat R S<VAR>inst✝ : Flat S M<GOAL>∀ (I : Ideal R), Function.Injective ⇑(lTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Flat R S<VAR>inst✝ : Flat S M<VAR>I : Ideal R<GOAL>Function.Injective ⇑(lTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Flat R S<VAR>inst✝ : Flat S M<VAR>I : Ideal R<GOAL>Function.Injective (⇑(TensorProduct.rid R M) ∘ ⇑(lTensor M (Submodule.subtype I)))
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Flat R S<VAR>inst✝ : Flat S M<VAR>I : Ideal R<VAR>h : ⇑(TensorProduct.rid R M) ∘ ⇑(lTensor M (Submodule.subtype I)) = ⇑(↑(TensorProduct.rid R M) ∘ₗ lTensor M (Submodule.subtype I))<GOAL>Function.Injective (⇑(TensorProduct.rid R M) ∘ ⇑(lTensor M (Submodule.subtype I)))
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : Flat R S<VAR>inst✝ : Flat S M<VAR>I : Ideal R<VAR>h : ⇑(TensorProduct.rid R M) ∘ ⇑(lTensor M (Submodule.subtype I)) = ⇑(↑(TensorProduct.rid R M) ∘ₗ lTensor M (Submodule.subtype I))<GOAL>Function.Injective ⇑(lTensor M (Submodule.subtype (Module.Flat.J R S I)))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>μ {x | v.limRatioMeas hρ x = ⊤} = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<GOAL>∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<GOAL>∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<GOAL>∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<GOAL>μ s ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<VAR>ρs : ρ s ≠ ⊤<GOAL>μ s ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<VAR>ρs : ρ s ≠ ⊤<VAR>A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s<GOAL>μ s ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<VAR>ρs : ρ s ≠ ⊤<VAR>A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s<VAR>B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 (⊤⁻¹ * ρ s))<GOAL>μ s ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<VAR>ρs : ρ s ≠ ⊤<VAR>A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s<VAR>B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 0)<GOAL>μ s ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>x✝ : x ∈ {x | v.limRatioMeas hρ x = ⊤}<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : ρ o < ⊤<VAR>s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o<VAR>ρs : ρ s ≠ ⊤<VAR>A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s<VAR>B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 0)<GOAL>∀ᶠ (c : ℝ≥0) in atTop, μ s ≤ (↑c)⁻¹ * ρ s
<VAR>l : Type u_1<VAR>m✝ : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype n<VAR>v : n → α<VAR>x y : Matrix m✝ n α<VAR>m : m✝<GOAL>{ toFun := fun M => M *ᵥ v, map_zero' := ⋯ }.toFun (x + y) m = ({ toFun := fun M => M *ᵥ v, map_zero' := ⋯ }.toFun x + { toFun := fun M => M *ᵥ v, map_zero' := ⋯ }.toFun y) m
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<GOAL>k + 0 = k
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>x : α<VAR>E : Set α<GOAL>0 < infEdist x (closure E) ↔ x ∉ closure E
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasEqualizers C<VAR>X Y : C<VAR>inst✝¹ : Simple Y<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<VAR>w : f ≠ 0<GOAL>Epi f
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasEqualizers C<VAR>X Y : C<VAR>inst✝¹ : Simple Y<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<VAR>w : f ≠ 0<GOAL>Epi (factorThruImage f ≫ image.ι f)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasEqualizers C<VAR>X Y : C<VAR>inst✝¹ : Simple Y<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<VAR>w : f ≠ 0<VAR>this : IsIso (image.ι f)<GOAL>Epi (factorThruImage f ≫ image.ι f)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(Function.support fun a => AddOpposite.unop (x.coeff a)).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(Function.support fun a => AddOpposite.unop (x.coeff a)) = x.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(Function.support fun a => AddOpposite.op ((AddOpposite.unop x).coeff a)).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(Function.support fun a => AddOpposite.op ((AddOpposite.unop x).coeff a)) = (AddOpposite.unop x).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }) ((fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }) x) = x
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>AddOpposite.unop ((fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }) ((fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }) x)) = AddOpposite.unop x
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x y : HahnSeries Γ Rᵃᵒᵖ<GOAL>{ toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }, invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }, invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }, invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun y
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x y : HahnSeries Γ Rᵃᵒᵖ<GOAL>AddOpposite.unop ({ toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }, invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y)) = AddOpposite.unop ({ toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }, invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun x => AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }, invFun := fun x => { coeff := fun a => AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M + 1 < t.card<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M + 1 < t.card<VAR>x₀ : M<VAR>x₀_mem : x₀ ∈ t<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0