ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>p : A → Prop<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra 𝕜 A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus 𝕜 p<VAR>inst✝ : UniqueContinuousFunctionalCalculus 𝕜 A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>p : A → Prop<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra 𝕜 A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus 𝕜 p<VAR>inst✝ : UniqueContinuousFunctionalCalculus 𝕜 A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>h : Continuous ⇑(cfcHom ⋯)<GOAL>cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>p : A → Prop<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra 𝕜 A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus 𝕜 p<VAR>inst✝ : UniqueContinuousFunctionalCalculus 𝕜 A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>h : Continuous ⇑(cfcHom ⋯)<VAR>x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)<GOAL>cfc (exp 𝕜) a = exp 𝕜 ((cfcHom ha) { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>p : A → Prop<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra 𝕜 A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus 𝕜 p<VAR>inst✝ : UniqueContinuousFunctionalCalculus 𝕜 A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>h : Continuous ⇑(cfcHom ⋯)<VAR>x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)<GOAL>(cfcHom ha) { toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } = (cfcHom ⋯) (exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ })
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>p : A → Prop<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra 𝕜 A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus 𝕜 p<VAR>inst✝ : UniqueContinuousFunctionalCalculus 𝕜 A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>h : Continuous ⇑(cfcHom ⋯)<VAR>x✝ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a)<VAR>a✝ : ↑(spectrum 𝕜 a)<GOAL>{ toFun := (spectrum 𝕜 a).restrict (exp 𝕜), continuous_toFun := ⋯ } a✝ = (exp 𝕜 { toFun := (spectrum 𝕜 a).restrict id, continuous_toFun := ⋯ }) a✝
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>num✝ : ℤ<VAR>denom✝ : ℕ<VAR>h : Invertible ↑denom✝<GOAL>-(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>num✝ : ℤ<VAR>denom✝ : ℕ<VAR>h : Invertible ↑denom✝<GOAL>↑(-num✝) * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : HasCokernel f✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : Epi f<VAR>inst✝ : HasCokernel g<GOAL>g ≫ cokernel.π (f ≫ g) = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : HasCokernel f✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : Epi f<VAR>inst✝ : HasCokernel g<GOAL>(f ≫ g) ≫ cokernel.π (f ≫ g) = f ≫ 0
<VAR>m✝ n✝ m n : ℤ<GOAL>4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
<VAR>m✝ n✝ m n : ℤ<VAR>h : Even (m + n)<GOAL>4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
<VAR>m✝ n✝ m n : ℤ<VAR>h : Odd (m + n)<GOAL>4 ∣ 2 * m + 1 + (2 * n + 1) ∨ 4 ∣ 2 * m + 1 - (2 * n + 1)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>s : S<VAR>a : G<VAR>ha : a ∈ s<VAR>x✝ : G<GOAL>x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
<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>E : K ⥤ J<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>inst✝² : HasLimit F<VAR>inst✝¹ : HasLimit (E ⋙ F)<VAR>inst✝ : HasLimit (F ⋙ G)<VAR>h : HasLimit ((E ⋙ F) ⋙ G)<VAR>this : HasLimit (E ⋙ F ⋙ G)<VAR>j✝ : K<GOAL>(G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>⨅ α, Weight.ker = ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>⨆ i, Weight.ker.dualAnnihilator = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>(Algebra.norm R[X]) (p • 1 + q • (mk W) Y) = p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>(p * 1 + q * 0) * ((q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) * if 0 = 1 then 1 else 0) + (p - q * (C W.a₁ * X + C W.a₃)) * 1) - (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) * 1 + (p - q * (C W.a₁ * X + C W.a₃)) * 0) * ((p * if 0 = 1 then 1 else 0) + q * 1) = p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>hb : o < b<GOAL>CNF b o = [(0, o)]
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>f : (ι → ℝ) →ₗ[ℝ] ι → ℝ<VAR>hf : LinearMap.det f ≠ 0<GOAL>Measure.map (⇑f) volume = ofReal |(LinearMap.det f)⁻¹| • volume
<VAR>c : ℝ<VAR>f✝ g : ℕ → Bool<VAR>n : ℕ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
<VAR>c : ℝ<VAR>f✝ g : ℕ → Bool<VAR>n : ℕ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1) = (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
<VAR>c : ℝ<VAR>f✝ g : ℕ → Bool<VAR>n : ℕ<VAR>f : ℕ → Bool<VAR>h1 : 0 ≤ c<VAR>h2 : c < 1<GOAL>(bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n => f (n + 1)) x = (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m n : ℕ<GOAL>(↑(powers a)).Finite ↔ IsOfFinOrder a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m n : ℕ<VAR>h : (↑(powers a)).Finite<GOAL>IsOfFinOrder a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n✝ : ℕ<VAR>h : (↑(powers a)).Finite<VAR>m n : ℕ<VAR>hmn : m < n<VAR>ha : a ^ m = a ^ n<GOAL>IsOfFinOrder a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n✝ : ℕ<VAR>h : (↑(powers a)).Finite<VAR>m n : ℕ<VAR>hmn : m < n<VAR>ha : a ^ m = a ^ n<GOAL>a ^ (n - m) = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>b : ↑(Iic a)<VAR>h : CompleteLattice.IsCompactElement ↑b<GOAL>CompleteLattice.IsCompactElement b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>b : ↑(Iic a)<VAR>h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a<GOAL>∀ (ι : Type u_2) (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>b : ↑(Iic a)<VAR>h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a<VAR>ι : Type u_2<VAR>s : ι → ↑(Iic a)<VAR>hb : b ≤ iSup s<GOAL>∃ t, b ≤ ⨆ a_1 ∈ t, s a_1
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>b : ↑(Iic a)<VAR>h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a<VAR>ι : Type u_2<VAR>s : ι → ↑(Iic a)<VAR>hb : ↑b ≤ iSup (Subtype.val ∘ s)<GOAL>∃ t, b ≤ ⨆ a_1 ∈ t, s a_1
<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 : Subgroup G<VAR>x : G<VAR>xH : x ∈ H<VAR>n : G<GOAL>n ∈ H ↔ x * n * x⁻¹ ∈ H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>p : Multiset (Associates α)<GOAL>∀ (a : Associates α) (s : Multiset (Associates α)), (s.prod = 1 ↔ ∀ a ∈ s, a = 1) → ((a ::ₘ s).prod = 1 ↔ ∀ a_2 ∈ a ::ₘ s, a_2 = 1)
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : LeftLift f g<VAR>i : s ⟶ t<VAR>x : B<VAR>h : x ⟶ c<GOAL>(s.whisker h).hom ≫ (postcomp x f).map (h ◁ i.right) = (t.whisker h).hom
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : LeftLift f g<VAR>i : s ⟶ t<VAR>x : B<VAR>h : x ⟶ c<GOAL>((s.whisker h).hom ≫ (postcomp x f).map (h ◁ i.right)) ≫ (α_ h t.lift f).hom = (t.whisker h).hom ≫ (α_ h t.lift f).hom
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>a d : α<GOAL>a * b ∣ a * (b * d)
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>a d : α<GOAL>a * (b * d) = a * b * d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : c ≤ max a b<GOAL>Icc a b ∪ Ici c = Ici (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>h : c ≤ b<GOAL>Icc a b ∪ Ici c = Ici (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b < a<VAR>h : c ≤ a ∨ c ≤ b<GOAL>Icc a b ∪ Ici c = Ici (min a c)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>inst✝² : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<VAR>s : Set α<GOAL>Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>inst✝² : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<VAR>s : Set α<GOAL>∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>inst✝² : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<VAR>s : Set α<GOAL>Tendsto (fun i => ∫⁻ (x : α) in s, ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>↑p ∣ r.num - r.num * r.den.gcdA p % ↑p * ↑r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>↑(r.num - r.num * r.den.gcdA p % ↑p * ↑r.den) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : (fun x => ↑x % ↑p) ↑(r.den.gcd p) = (fun x => ↑x % ↑p) (↑r.den * r.den.gcdA p + ↑p * r.den.gcdB p)<GOAL>↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>↑r.num - ↑r.num * ↑(r.den.gcdA p) * ↑r.den = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>↑r.num - ↑r.num * ↑(r.den.gcd p) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>r.den.Coprime p
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>p.Coprime r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>¬p ∣ r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>1 ≤ ‖↑↑r.den‖
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>‖↑↑r.den‖ = 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)<GOAL>IsUnit ↑↑r.den
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<GOAL>normalClosure F (↥K) L = ⨆ f, map f K
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>f : ↥K →ₐ[F] L<GOAL>f.fieldRange ≤ ⨆ f, map f K
<VAR>F : Type u_1<VAR>K✝ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝<VAR>inst✝¹ : Algebra F L<VAR>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>f : L →ₐ[F] L<GOAL>map f K ≤ ⨆ f, f.fieldRange
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y x' y' : α<VAR>ex : x = gcd x y * x'<VAR>ey : y = gcd x y * y'<VAR>h : gcd x y ≠ 0<GOAL>IsUnit (gcd x' y')
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y x' y' : α<VAR>ex : x = gcd x y * x'<VAR>ey : y = gcd x y * y'<VAR>h : gcd x y ≠ 0<GOAL>Associated (gcd x' y') 1
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y x' y' : α<VAR>ex : x = gcd x y * x'<VAR>ey : y = gcd x y * y'<VAR>h : gcd x y ≠ 0<GOAL>Associated (gcd x y * gcd x' y') (gcd x y * 1)
<VAR>α✝ : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α✝<VAR>α : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y x' y' : α<VAR>ex : x = gcd x y * x'<VAR>ey : y = gcd x y * y'<VAR>h : gcd x y ≠ 0<GOAL>gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsTrans α r<VAR>f : ℕ → α<GOAL>∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsTrans α r<VAR>f : ℕ → α<VAR>g : ℕ ↪o ℕ<VAR>hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))<GOAL>∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsTrans α r<VAR>f : ℕ → α<VAR>g : ℕ ↪o ℕ<VAR>hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))<GOAL>∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f : ↥(simpleFunc E 1 μ)<VAR>this : ↑(toSimpleFunc (-f)) =ᶠ[ae μ] ↑(-toSimpleFunc f)<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (-f)) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f : ↥(simpleFunc E 1 μ)<VAR>this : ↑(toSimpleFunc (-f)) =ᶠ[ae μ] ↑(-toSimpleFunc f)<GOAL>SimpleFunc.setToSimpleFunc T (-toSimpleFunc f) = -SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<GOAL>prehaar (↑K₀) U ⊥ = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖x‖ / ((-o).oangle y (x + y)).sin = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖x‖ / ((-o).oangle y (y + x)).sin = ‖y + x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, Ici (f i j)
<VAR>s : List Char<VAR>i e n : Nat<GOAL>go₂ s { byteIdx := i + n } { byteIdx := e + n } = go₂ s { byteIdx := i } { byteIdx := e }
<VAR>s : List Char<VAR>i e n : Nat<GOAL>∀ (c : Char) (cs : List Char) (i : Pos), ¬i = { byteIdx := e } → go₂ cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := e + n } = go₂ cs (i + c) { byteIdx := e } → (if { byteIdx := i.byteIdx + n } = { byteIdx := e + n } then [] else c :: go₂ cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := e + n }) = if i = { byteIdx := e } then [] else c :: go₂ cs (i + c) { byteIdx := e }
<VAR>s : List Char<VAR>i✝ e n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>h : ¬{ byteIdx := i } = { byteIdx := e }<VAR>ih : go₂ cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := e + n } = go₂ cs ({ byteIdx := i } + c) { byteIdx := e }<GOAL>(if { byteIdx := { byteIdx := i }.byteIdx + n } = { byteIdx := e + n } then [] else c :: go₂ cs ({ byteIdx := { byteIdx := i }.byteIdx + n } + c) { byteIdx := e + n }) = if { byteIdx := i } = { byteIdx := e } then [] else c :: go₂ cs ({ byteIdx := i } + c) { byteIdx := e }
<VAR>s : List Char<VAR>i✝ e n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>ih : go₂ cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := e + n } = go₂ cs ({ byteIdx := i } + c) { byteIdx := e }<VAR>h : ¬i = e<GOAL>(if i + n = e + n then [] else c :: go₂ cs { byteIdx := i + n + c.utf8Size } { byteIdx := e + n }) = if i = e then [] else c :: go₂ cs { byteIdx := i + c.utf8Size } { byteIdx := e }
<VAR>s : List Char<VAR>i✝ e n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>ih : go₂ cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := e + n } = go₂ cs ({ byteIdx := i } + c) { byteIdx := e }<VAR>h : ¬i = e<GOAL>go₂ cs { byteIdx := i + n + c.utf8Size } { byteIdx := e + n } = go₂ cs { byteIdx := i + c.utf8Size } { byteIdx := e }
<VAR>s : List Char<VAR>i✝ e n : Nat<VAR>c : Char<VAR>cs : List Char<VAR>i : Nat<VAR>ih : go₂ cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := e + n } = go₂ cs ({ byteIdx := i } + c) { byteIdx := e }<VAR>h : ¬i = e<GOAL>go₂ cs { byteIdx := i + c.utf8Size + n } { byteIdx := e + n } = go₂ cs { byteIdx := i + c.utf8Size } { byteIdx := e }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f : CauSeq α abs<VAR>a : α<VAR>h : -f < const a<GOAL>(f - const (-a)).Pos
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e f : Pretrivialization F proj<GOAL>(f.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ
<VAR>n✝ m n : ℕ<VAR>i : Fin n.succ<VAR>hi : i ∈ Set.range castSucc<GOAL>↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i
<VAR>n✝ m n : ℕ<VAR>i : Fin n.succ<VAR>hi : i ∈ Set.range castSucc<GOAL>↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩).castSucc = ↑i
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0<GOAL>EMetric.closedBall x ↑ε = closedBall x ↑ε
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>smeval 1 x = 1 • x ^ 0