ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>h : affineSpan ℝ s = ⊤<VAR>t : Set V<VAR>hts : t ⊆ s<VAR>b : AffineBasis ↑t ℝ V<VAR>hb : ⇑b = Subtype.val<GOAL>(interior ((convexHull ℝ) (range ⇑b))).Nonempty
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>h : affineSpan ℝ s = ⊤<VAR>t : Finset V<VAR>hts : ↑t ⊆ s<VAR>b : AffineBasis ↑↑t ℝ V<VAR>hb : ⇑b = Subtype.val<GOAL>(interior ((convexHull ℝ) (range ⇑b))).Nonempty
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>F : ℂ → E := fun z => (z - c) • f z<GOAL>DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>F : ℂ → E := fun z => (z - c) • f z<GOAL>DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>F : ℂ → E := fun z => (z - c) • f z<GOAL>ContinuousAt F c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>F : ℂ → E := fun z => (z - c) • f z<GOAL>ContinuousWithinAt F {c}ᶜ c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>F : ℂ → E := fun z => (z - c) • f z<VAR>H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)<GOAL>ContinuousWithinAt F {c}ᶜ c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>c : ℂ<VAR>hc : s ∈ 𝓝 c<VAR>hd : DifferentiableOn ℂ f (s \ {c})<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>F : ℂ → E := fun z => (z - c) • f z<VAR>H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)<VAR>H' : Tendsto (fun z => (z - c) • f c) (𝓝[≠] c) (𝓝 (F c))<GOAL>ContinuousWithinAt F {c}ᶜ c
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>y : ↥f.inverse.domain<VAR>x : ↥f.domain<VAR>hxy : ↑f x = ↑y<GOAL>↑f.inverse y = ↑x
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>y : ↥f.inverse.domain<VAR>x : ↥f.domain<VAR>hxy : ↑f x = ↑y<VAR>this : (↑f x, ↑x) ∈ f.inverse.graph<GOAL>↑f.inverse y = ↑x
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>y : ↥f.inverse.domain<VAR>x : ↥f.domain<VAR>hxy : ↑f x = ↑y<VAR>this : ∃ (x_1 : ↑f x ∈ f.inverse.domain), ↑f.inverse ⟨↑f x, ⋯⟩ = ↑x<GOAL>↑f.inverse y = ↑x
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>y : ↥f.inverse.domain<VAR>x : ↥f.domain<VAR>hxy : ↑f x = ↑y<VAR>hx : ↑f x ∈ f.inverse.domain<VAR>h : ↑f.inverse ⟨↑f x, ⋯⟩ = ↑x<GOAL>y = ⟨↑f x, ⋯⟩
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>inst✝ : K.Normal<VAR>hK : K ≤ N<GOAL>K = ⊥ ∨ K = N
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>inst✝ : K.Normal<VAR>hK : K ≤ N<VAR>this : Function.Surjective ⇑(QuotientGroup.mk' K)<GOAL>K = ⊥ ∨ K = N
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>inst✝ : K.Normal<VAR>hK : K ≤ N<VAR>this : Function.Surjective ⇑(QuotientGroup.mk' K)<VAR>h4 : ∀ (K : Subgroup G), K ⊔ N = ⊤ → K = ⊤<GOAL>K = ⊥ ∨ K = N
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>inst✝ : K.Normal<VAR>hK : K ≤ N<VAR>this : Function.Surjective ⇑(QuotientGroup.mk' K)<VAR>h4 : K ≠ ⊥ ∧ K ≠ N<GOAL>∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>inst✝ : K.Normal<VAR>hK : K ≤ N<VAR>this : Function.Surjective ⇑(QuotientGroup.mk' K)<VAR>h4 : K ≠ ⊥ ∧ K ≠ N<VAR>h5 : Nat.card (G ⧸ K) < Nat.card G<GOAL>∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>inst✝ : K.Normal<VAR>hK : K ≤ N<VAR>this : Function.Surjective ⇑(QuotientGroup.mk' K)<VAR>h4 : K ≠ ⊥ ∧ K ≠ N<VAR>h5 : Nat.card (G ⧸ K) < Nat.card G<VAR>h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index<GOAL>∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>μ : Measure α<VAR>a : α<GOAL>(κ ∘ₖ const α μ) a = μ.bind ⇑κ
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝² : CommRing R<VAR>L : Type w<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>F : FreeLieAlgebra R X →ₗ⁅R⁆ L<GOAL>(lift R) (⇑F ∘ of R) = F
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝² : CommRing R<VAR>L : Type w<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>F : FreeLieAlgebra R X →ₗ⁅R⁆ L<GOAL>(lift R) ((lift R).symm F) = F
<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>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map₂ m (pure a) (pure b) = pure (m a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝¹ : Star α<VAR>inst✝ : Star β<VAR>A : Matrix n n α<VAR>e : m ≃ n<VAR>h : (A.submatrix ⇑e ⇑e).IsHermitian<GOAL>A.IsHermitian
<VAR>n k : ℕ<VAR>h : MinFacHelper n k<GOAL>1 < n
<VAR>n k : ℕ<VAR>h : MinFacHelper n k<VAR>this : 2 < n.minFac<GOAL>1 < n
<VAR>k : ℕ<VAR>h : MinFacHelper 0 k<VAR>this : 2 < minFac 0<GOAL>1 < 0
<VAR>n k : ℕ<VAR>h✝ : MinFacHelper n k<VAR>this : 2 < n.minFac<VAR>h : n > 0<GOAL>1 < n
<VAR>k : ℕ<VAR>h✝ : MinFacHelper (succ 0) k<VAR>this : 2 < (succ 0).minFac<VAR>h : succ 0 > 0<GOAL>1 < succ 0
<VAR>n k : ℕ<VAR>h✝¹ : MinFacHelper n k<VAR>this : 2 < n.minFac<VAR>h✝ : n > 0<VAR>h : succ 0 < n<GOAL>1 < n
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h : Fintype.card R ≤ 3<GOAL>univ = {0, 1, -1}
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h : Fintype.card R ≤ 3<GOAL>univ.card ≤ {0, 1, -1}.card
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h✝ : Fintype.card R ≤ 3<VAR>h : Fintype.card R < 3<GOAL>univ.card ≤ {0, 1, -1}.card
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h✝ : Fintype.card R ≤ 3<VAR>h : Fintype.card R = 3<GOAL>univ.card ≤ {0, 1, -1}.card
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ.IsNontrivial ↔ χ ≠ 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.33376, u_1} C<VAR>inst✝³ : Category.{?u.33380, u_2} D<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<GOAL>F.map S.f ≫ F.map S.g = 0
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>l : Filter α<VAR>s : Set α<GOAL>s ∈ cocountable ↔ sᶜ.Countable
<VAR>x y : PartENat<VAR>hx : x ≠ ⊤<GOAL>x < y + 1 ↔ x ≤ y
<VAR>x y : PartENat<VAR>hx : x ≠ ⊤<VAR>h : x ≤ y<GOAL>x < y + 1
<VAR>y : PartENat<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>h : ↑m ≤ y<GOAL>↑m < y + 1
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>h : ↑m ≤ ⊤<GOAL>↑m < ⊤ + 1
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m ≤ ↑n<GOAL>↑m < ↑n + 1
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m ≤ ↑n<GOAL>m < n + 1
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m ≤ ↑n<GOAL>m ≤ n
<VAR>s m n : Nat<GOAL>range' s m ++ range' (s + m) n = range' s (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ✝ : Type u_5<VAR>mγ✝ : MeasurableSpace γ✝<VAR>f✝ : β → γ✝<VAR>g : γ✝ → α<VAR>κ : Kernel α β<VAR>γ : Type u_6<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>hf : Measurable f<GOAL>(κ.map (fun a => (f a, a)) ⋯).snd = κ
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝¹ : HasColimit (F ⋙ G)<VAR>E : Type u''<VAR>inst✝ : Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : HasColimit ((F ⋙ G) ⋙ H)<VAR>j : J<GOAL>ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝¹ : HasColimit (F ⋙ G)<VAR>E : Type u''<VAR>inst✝ : Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : HasColimit ((F ⋙ G) ⋙ H)<VAR>j : J<GOAL>H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝¹ : HasColimit (F ⋙ G)<VAR>E : Type u''<VAR>inst✝ : Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : HasColimit ((F ⋙ G) ⋙ H)<VAR>j : J<VAR>this : HasColimit (F ⋙ G ⋙ H)<GOAL>H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<GOAL>∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<GOAL>∃ t ⊆ ∅, affineSpan k t = affineSpan k ∅ ∧ AffineIndependent k Subtype.val
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<VAR>b : Set V<VAR>hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s<VAR>hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)<VAR>hb₃ : LinearIndependent (ι := { x // x ∈ b }) k Subtype.val<GOAL>∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<VAR>b : Set V<VAR>hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s<VAR>hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)<VAR>hb₃ : LinearIndependent (ι := { x // x ∈ b }) k Subtype.val<VAR>hb₀ : ∀ v ∈ b, v ≠ 0<GOAL>∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<VAR>b : Set V<VAR>hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s<VAR>hb₂ : Submodule.span k b = Submodule.span k (⇑(Equiv.vaddConst p).symm '' s)<VAR>hb₃ : AffineIndependent k fun p_1 => ↑p_1<VAR>hb₀ : ∀ v ∈ b, v ≠ 0<GOAL>∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
<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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] (R * 0))<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] 0)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] 0)<GOAL>((fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r => R * r) =ᶠ[𝓝[>] 0] fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
<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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] 0)<GOAL>∀ a ∈ Ioi 0, ((fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r => R * r) a = μ (s ∩ ({x} + a • t)) / μ ({x} + a • u)
<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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] 0)<VAR>r : ℝ<GOAL>((fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r => R * r) r = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
<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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] 0)<VAR>r : ℝ<VAR>T : (R * r) • t' = r • t<GOAL>((fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r => R * r) r = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
<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>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>t_bound : t ⊆ closedBall 0 R<VAR>t' : Set E := R⁻¹ • t<VAR>ht' : t' = R⁻¹ • t<VAR>u' : Set E := R⁻¹ • u<VAR>hu' : u' = R⁻¹ • u<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => R * r) (𝓝[>] 0) (𝓝[>] 0)<VAR>r : ℝ<VAR>T : (R * r) • t' = r • t<VAR>U : (R * r) • u' = r • u<GOAL>((fun r => μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) ∘ fun r => R * r) r = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp (a + m • p) b = toIocMod hp a b + m • p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a<GOAL>ContinuousAt (⇑(equivIoc p a)) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>z✝ : 𝕜<VAR>hx : ↑z✝ ≠ ↑a<GOAL>ContinuousAt ⇑(equivIoc p a) ↑z✝
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>z✝ : 𝕜<VAR>hx : ↑z✝ ≠ ↑a<GOAL>Filter.map (⇑(equivIoc p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 ((equivIoc p a) ↑z✝)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>⨅ x, T.rayleighQuotient ↑x = ⨅ x, T.rayleighQuotient ↑x
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<VAR>hc : I.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.IsPartition
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<VAR>hc : ⊤.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.IsPartition
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<VAR>hc : ⊤.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hc' : ⊤.compl.distortion ≤ c<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.IsPartition
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>⨅ i ∈ f, sSup (u '' id i) = ⨅ s ∈ f, ⨆ a ∈ s, u a