ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑(sa * s₁) = ra * ↑s₂<GOAL>(r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (ra • r₂ /ₒ (sa * s₁))
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑(sa * s₁) = ra * ↑s₂<GOAL>oreNum r₃ (sa * s₁) • (sa • r₁ + ra • r₂) /ₒ (oreDenom r₃ (sa * s₁) * s₃) = oreNum r₃ (sa * s₁) • sa • r₁ /ₒ (oreDenom r₃ (sa * s₁) * s₃) + oreNum r₃ (sa * s₁) • ra • r₂ /ₒ (oreDenom r₃ (sa * s₁) * s₃)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure β<VAR>s : Set β<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(Measure.comap f (μ.restrict s)) t = ((Measure.comap f μ).restrict (f ⁻¹' s)) t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 ≤ a<VAR>hb₀ : 0 < b<VAR>hb₁ : b ≤ 1<GOAL>a ≤ a / b
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>inst✝¹¹ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K✝ L✝ M K' L' : HomologicalComplex C c<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>inst✝¹⁰ : Category.{u_4, u_2} C₁<VAR>inst✝⁹ : Category.{u_5, u_3} C₂<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>K L : HomologicalComplex C₁ c<VAR>φ : K ⟶ L<VAR>F : C₁ ⥤ C₂<VAR>inst✝⁶ : F.Additive<VAR>inst✝⁵ : F.PreservesHomology<VAR>inst✝⁴ : ∀ (i : ι), K.HasHomology i<VAR>inst✝³ : ∀ (i : ι), L.HasHomology i<VAR>inst✝² : ∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i<VAR>inst✝¹ : ∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i<VAR>inst✝ : F.ReflectsIsomorphisms<GOAL>QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ
<VAR>n a b : ℕ<VAR>a1 : a ≠ 1<VAR>b1 : b ≠ 1<GOAL>¬Prime (a * b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_6, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝¹ : Category.{u_5, u_3} E<VAR>inst✝ : L.IsLocalization W<VAR>F₁ F₂ F₃ : C ⥤ E<VAR>F₁' F₂' F₃' : D ⥤ E<VAR>h₁ : Lifting L W F₁ F₁'<VAR>h₂ : Lifting L W F₂ F₂'<VAR>h₃ : Lifting L W F₃ F₃'<VAR>τ : F₁ ⟶ F₂<VAR>τ' : F₂ ⟶ F₃<VAR>X : C<GOAL>(liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ').app (L.obj X) = (liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ')).app (L.obj X)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<VAR>f : R →+* S<GOAL>(map f) (esymm σ R n) = esymm σ S n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<GOAL>Summable fun n => ‖p n‖ * ↑r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n<GOAL>Summable fun n => ‖p n‖ * ↑r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>r : α → α → Prop<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b<GOAL>Pairwise r l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>r : α → α → Prop<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b<GOAL>∀ {a b : α}, [a, b] <+ l → r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a✝ : α<VAR>l✝ l : List α<VAR>r : α → α → Prop<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b<VAR>a b : α<VAR>hab : [a, b] <+ l<GOAL>r a b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_mon : Monotone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f i = f a₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_mon : Monotone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f i ≤ f a₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_mon : Monotone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f a₁ ≤ f i
<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✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>c : E<GOAL>a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>a : T<GOAL>(C a).aroots S = 0
<VAR>α : Type u<GOAL>#(List α) ≤ max ℵ₀ #α
<VAR>α : Type u<VAR>h✝ : Finite α<GOAL>#(List α) ≤ max ℵ₀ #α
<VAR>α : Type u<VAR>h✝ : Infinite α<GOAL>#(List α) ≤ max ℵ₀ #α
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i : n<VAR>this : Nonempty n<GOAL>A.det = ∑ j : n, A i j * A.adjugate j i
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i : n<VAR>this : Nonempty n<VAR>n' : ℕ<VAR>hn' : Fintype.card n = n'.succ<GOAL>A.det = ∑ j : n, A i j * A.adjugate j i
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i : n<VAR>this : Nonempty n<VAR>n' : ℕ<VAR>hn' : Fintype.card n = n'.succ<VAR>x✝ : Trunc (n ≃ Fin n'.succ)<VAR>e : n ≃ Fin n'.succ<VAR>A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A<GOAL>A.det = ∑ j : n, A i j * A.adjugate j i
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i : n<VAR>this : Nonempty n<VAR>n' : ℕ<VAR>hn' : Fintype.card n = n'.succ<VAR>x✝ : Trunc (n ≃ Fin n'.succ)<VAR>e : n ≃ Fin n'.succ<VAR>A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A<GOAL>A'.det = ∑ j : Fin n'.succ, A' (e i) j * A'.adjugate j (e i)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i : n<VAR>this : Nonempty n<VAR>n' : ℕ<VAR>hn' : Fintype.card n = n'.succ<VAR>x✝ : Trunc (n ≃ Fin n'.succ)<VAR>e : n ≃ Fin n'.succ<VAR>A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A<GOAL>∑ j : Fin n'.succ, (-1) ^ (↑(e i) + ↑j) * A' (e i) j * (A'.submatrix (e i).succAbove j.succAbove).det = ∑ j : Fin n'.succ, A' (e i) j * A'.adjugate j (e i)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<GOAL>Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<VAR>L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)<GOAL>Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<VAR>L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)<VAR>Z : Tendsto (fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) l (𝓝 (a * 1))<GOAL>Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<VAR>L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)<VAR>Z : Tendsto (fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) l (𝓝 a)<GOAL>Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<VAR>L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)<VAR>Z : Tendsto (fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) l (𝓝 a)<GOAL>(fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l] fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<VAR>L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)<VAR>Z : Tendsto (fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) l (𝓝 a)<VAR>this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x<GOAL>(fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l] fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
<VAR>f : ℝ → ℝ<VAR>x a c d : ℝ<VAR>l : Filter ℝ<VAR>hl : l ≤ 𝓝[≠] x<VAR>hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)<VAR>h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l<VAR>L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)<VAR>Z : Tendsto (fun x_1 => ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) l (𝓝 a)<VAR>this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x<VAR>y : ℝ<VAR>hy : y + c * (y - x) ^ 2 ≠ x<GOAL>((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) y * ((y + c * (y - x) ^ 2 - x) / (y - x)) = (f (y + c * (y - x) ^ 2) - d) / (y - x)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>L' : Tendsto (fun r => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>L' : Tendsto (fun r => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>L'' : Tendsto (fun r => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>L' : Tendsto (fun r => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>L'' : Tendsto (fun r => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>this : Tendsto (fun a => μ ({x} + a • t) / μ ({x} + a • t) - μ (sᶜ ∩ ({x} + a • t)) / μ ({x} + a • t)) (𝓝[>] 0) (𝓝 (1 - 0))<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>L' : Tendsto (fun r => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>L'' : Tendsto (fun r => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>this : Tendsto (fun a => μ ({x} + a • t) / μ ({x} + a • t) - μ (sᶜ ∩ ({x} + a • t)) / μ ({x} + a • t)) (𝓝[>] 0) (𝓝 1)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>L' : Tendsto (fun r => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>L'' : Tendsto (fun r => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>this : Tendsto (fun a => μ ({x} + a • t) / μ ({x} + a • t) - μ (sᶜ ∩ ({x} + a • t)) / μ ({x} + a • t)) (𝓝[>] 0) (𝓝 1)<GOAL>(fun a => μ ({x} + a • t) / μ ({x} + a • t) - μ (sᶜ ∩ ({x} + a • t)) / μ ({x} + a • t)) =ᶠ[𝓝[>] 0] fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)
<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>hs : MeasurableSet s<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ⊤ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u<VAR>L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>L' : Tendsto (fun r => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>L'' : Tendsto (fun r => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>this : Tendsto (fun a => μ ({x} + a • t) / μ ({x} + a • t) - μ (sᶜ ∩ ({x} + a • t)) / μ ({x} + a • t)) (𝓝[>] 0) (𝓝 1)<GOAL>∀ a ∈ Ioi 0, μ ({x} + a • t) / μ ({x} + a • t) - μ (sᶜ ∩ ({x} + a • t)) / μ ({x} + a • t) = μ (s ∩ ({x} + a • t)) / μ ({x} + a • t)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>h : Normal F K<VAR>inst✝ : FiniteDimensional F K<VAR>s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K<GOAL>∃ p, IsSplittingField F K p
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>h : Normal F K<VAR>inst✝ : FiniteDimensional F K<VAR>s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K<GOAL>Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x)).rootSet K)) = Subalgebra.toSubmodule ⊤
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>h : Normal F K<VAR>inst✝ : FiniteDimensional F K<VAR>s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K<GOAL>∀ (y : ↑(Basis.ofVectorSpaceIndex F K)), s y ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x)).rootSet K)))
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>h : Normal F K<VAR>inst✝ : FiniteDimensional F K<VAR>s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K<VAR>x✝¹ x : ↑(Basis.ofVectorSpaceIndex F K)<VAR>x✝ : x ∈ Finset.univ<GOAL>minpoly F (s x) ≠ 0
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>h : Normal F K<VAR>inst✝ : FiniteDimensional F K<VAR>s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K<VAR>x : ↑(Basis.ofVectorSpaceIndex F K)<GOAL>(map (algebraMap F K) (∏ x : ↑(Basis.ofVectorSpaceIndex F K), minpoly F (s x))).IsRoot (s x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>h : Normal F K<VAR>inst✝ : FiniteDimensional F K<VAR>s : Basis (↑(Basis.ofVectorSpaceIndex F K)) F K := Basis.ofVectorSpace F K<VAR>x : ↑(Basis.ofVectorSpaceIndex F K)<GOAL>∏ x_1 : ↑(Basis.ofVectorSpaceIndex F K), (aeval (s x)) (minpoly F (s x_1)) = 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>e✝ e : P ≃ᵃⁱ[𝕜] P₂<GOAL>range ⇑e = univ
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>e✝ e : P ≃ᵃⁱ[𝕜] P₂<GOAL>range ⇑e.toIsometryEquiv = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>f : Filter α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>a : α<VAR>hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝<VAR>h : a < f.limsSup<GOAL>∃ᶠ (n : α) in f, a < n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>f : Filter α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>a : α<VAR>hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝<VAR>h : ¬∃ᶠ (n : α) in f, a < n<GOAL>f.limsSup ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>f : Filter α<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>a : α<VAR>hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝<VAR>h : ∀ᶠ (x : α) in f, x ≤ a<GOAL>f.limsSup ≤ a
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<GOAL>x.IsSt x.st