ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>this : SeparableSpace ↑(range (uncurry f) ∪ {0})<VAR>s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯<GOAL>StronglyMeasurable 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✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>this : SeparableSpace ↑(range (uncurry f) ∪ {0})<VAR>s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯<VAR>s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯<GOAL>StronglyMeasurable 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✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>this : SeparableSpace ↑(range (uncurry f) ∪ {0})<VAR>s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯<VAR>s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯<VAR>f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)<GOAL>StronglyMeasurable 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✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>this : SeparableSpace ↑(range (uncurry f) ∪ {0})<VAR>s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯<VAR>s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯<VAR>f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)<VAR>hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)<GOAL>StronglyMeasurable 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✝¹ : NormedSpace ℝ E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<VAR>hE : CompleteSpace E<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>this : SeparableSpace ↑(range (uncurry f) ∪ {0})<VAR>s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯<VAR>s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯<VAR>f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)<VAR>hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)<VAR>h2f' : Tendsto f' atTop (𝓝 fun x => ∫ (y : β), f x y ∂ν)<GOAL>StronglyMeasurable 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>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>h : μ ≪ ν<VAR>c : R<VAR>s : Set α<VAR>hνs : ν s = 0<GOAL>(c • μ) s = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>h : a₂ ≠ 0<GOAL>HasSum (fun i => f i / a₂) (a₁ / a₂) ↔ HasSum f a₁
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ X<GOAL>α.hom = β.inv ↔ β.hom = α.inv
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>β : Y ≅ X<GOAL>β.hom = α.symm.hom ↔ β.hom = α.inv
<VAR>Y : Type u_1<VAR>inst✝ : TopologicalSpace Y<VAR>left✝ : PathConnectedSpace Y<VAR>right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)<GOAL>SimplyConnectedSpace Y
<VAR>Y : Type u_1<VAR>inst✝ : TopologicalSpace Y<VAR>left✝ : PathConnectedSpace Y<VAR>right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)<GOAL>Nonempty Y ∧ ∀ (x y : Y), Nonempty (Unique (Path.Homotopic.Quotient x y))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : MulZeroClass α<VAR>s✝ t s : Set α<GOAL>s * 0 ⊆ 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a✝ b : α<VAR>f : ι → α<VAR>a : α<GOAL>(⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<GOAL>Tendsto f atTop (𝓝 (limUnder atTop f))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<GOAL>∃ a, Tendsto f atTop (𝓝 a)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<GOAL>CauchySeq f
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∃ N, ∀ n ≥ N, dist (f n) (f N) < ε
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε<GOAL>∃ N, ∀ n ≥ N, dist (f n) (f N) < ε
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε<VAR>B : ∀ᶠ (n : ℕ) in atTop, a < ↑n<GOAL>∃ N, ∀ n ≥ N, dist (f n) (f N) < ε
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε<VAR>B : ∀ᶠ (n : ℕ) in atTop, a < ↑n<VAR>N : ℕ<VAR>hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε<VAR>h'N : a < ↑N<GOAL>∃ N, ∀ n ≥ N, dist (f n) (f N) < ε
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x y : G × G → CoeSort.coe A<VAR>g : G × G × G<GOAL>(A.ρ g.1) (x (g.2.1, g.2.2) + y (g.2.1, g.2.2)) - (x (g.1 * g.2.1, g.2.2) + y (g.1 * g.2.1, g.2.2)) + (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) - (x (g.1, g.2.1) + y (g.1, g.2.1)) = (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1) + ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>r : k<VAR>x : G × G → CoeSort.coe A<VAR>g : G × G × G<GOAL>(A.ρ g.1) (r • x (g.2.1, g.2.2)) - r • x (g.1 * g.2.1, g.2.2) + r • x (g.1, g.2.1 * g.2.2) - r • x (g.1, g.2.1) = r • ((A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1))
<VAR>cs cs' : List Char<VAR>c : Char<VAR>i p : Nat<VAR>hp : i + (utf8Len cs + c.utf8Size) = p<GOAL>utf8PrevAux (cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len cs }
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : D<GOAL>R.map (h.counit.app (L.obj (R.obj X))) ≫ R.map (h.counit.app X) = R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X✝ Y✝ : D<VAR>f : X✝ ⟶ Y✝<GOAL>R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y✝) = R.map (h.counit.app X✝) ≫ R.map f
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>Disjoint xᶜ y ↔ y ≤ x
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>inst✝⁹ : Ring R✝<VAR>inst✝⁸ : Ring S<VAR>M : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R✝ M<VAR>m : Submodule R✝ M<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R✝ N<VAR>inst✝³ : IsSemisimpleModule R✝ M<VAR>R : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsSemisimpleModule R M<GOAL>(Module.annihilator R M).IsRadical
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>inst✝⁹ : Ring R✝<VAR>inst✝⁸ : Ring S<VAR>M : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R✝ M<VAR>m : Submodule R✝ M<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R✝ N<VAR>inst✝³ : IsSemisimpleModule R✝ M<VAR>R : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsSemisimpleModule R M<GOAL>(⨅ i, (↑i).annihilator).IsRadical
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁴ : Category.{v', u'} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasEqualizers C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : f = 0<VAR>inst✝ : HasImage f<GOAL>ι f = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁴ : Category.{v', u'} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasEqualizers C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : f = 0<VAR>inst✝ : HasImage f<GOAL>(eqToIso h).hom ≫ ι 0 = 0
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => ↑n + x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<GOAL>UniformContinuous fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f : β → α<VAR>hf : UniformContinuous f<VAR>this : UniformContinuous fun x => 1 / f x<GOAL>UniformContinuous fun x => (f x)⁻¹
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommSemiring P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : DecidableEq R<VAR>s : Finset S<GOAL>⇑(algebraMap R S) '' ↑(Finset.image (fun t => integerMultiple M s id t) s.attach) = commonDenomOfFinset M s • ↑s
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommSemiring P<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : DecidableEq R<VAR>s : Finset S<GOAL>⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) = commonDenomOfFinset M s • ↑s
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>s : Set Y<VAR>h : s ⊆ e.target<GOAL>ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>s : Set Y<VAR>h : s ⊆ e.target<GOAL>(∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>s : Set Y<VAR>h : s ⊆ e.target<VAR>x : Y<VAR>hx : x ∈ s<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Y → Z<VAR>s : Set Y<VAR>h : s ⊆ e.target<VAR>x : Y<VAR>hx : x ∈ s<GOAL>e.source ∈ 𝓝 (↑e.symm x)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>𝒜 : Finset (Finset α)<GOAL>∑ s : Finset α, ↑(𝒜ᶜˢ.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) + ∑ s : Finset α, ↑(𝒜.truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>𝒜 : Finset (Finset α)<GOAL>∑ x : Finset α, ↑(𝒜ᶜˢ.truncatedInf ({ toFun := compl, inj' := ⋯ } x)).card / (↑({ toFun := compl, inj' := ⋯ } x).card * ↑((card α).choose ({ toFun := compl, inj' := ⋯ } x).card)) + ∑ s ∈ map { toFun := compl, inj' := ⋯ } univ, ↑(𝒜.truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
<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>f : α →. β<VAR>x✝ : α<GOAL>x✝ ∈ f.preimage Set.univ ↔ x✝ ∈ f.Dom
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : Cardinal.lift.{v, u} o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c<VAR>a : Ordinal.{max u v}<GOAL>Cardinal.lift.{v, u} #(Quotient.out o).α < c.cof
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s (closure t) = hausdorffEdist s t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>v : ι → E<VAR>hon : Orthonormal 𝕜 v<VAR>hsp : ⊤ ≤ span 𝕜 (range v)<GOAL>⇑(OrthonormalBasis.mk hon hsp) = v
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : CharZero α<VAR>m n d : ℕ<VAR>hn : d ∣ n<VAR>hm : d ∣ m<GOAL>↑(m / d) / ↑(n / d) = ↑m / ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : CharZero α<VAR>m n : ℕ<VAR>hn : 0 ∣ n<VAR>hm : 0 ∣ m<GOAL>↑(m / 0) / ↑(n / 0) = ↑m / ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : CharZero α<VAR>m n d : ℕ<VAR>hn : d ∣ n<VAR>hm : d ∣ m<VAR>hd : d ≠ 0<GOAL>↑(m / d) / ↑(n / d) = ↑m / ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : CharZero α<VAR>m n d : ℕ<VAR>hn : d ∣ n<VAR>hm : d ∣ m<VAR>hd : ↑d ≠ 0<GOAL>↑(m / d) / ↑(n / d) = ↑m / ↑n
<VAR>n : ℕ<GOAL>(n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0
<VAR>n k : ℕ<GOAL>(n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d✝ : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>d : 𝔸<GOAL>HasDerivWithinAt (fun y => c y * d) (c' * d) s x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d✝ : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>d : 𝔸<GOAL>c' * d = c' * d + c x * 0
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)<GOAL>∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)<VAR>this : MeasurableSet (Ioi 0)<GOAL>∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)<VAR>this : MeasurableSet (Ioi 0)<GOAL>∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)<VAR>this : MeasurableSet (Ioi 0)<GOAL>∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)<VAR>this✝ : MeasurableSet (Ioi 0)<VAR>this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)<GOAL>∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)<VAR>this✝ : MeasurableSet (Ioi 0)<VAR>this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)<VAR>t1 : Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))<GOAL>∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>full_integral : ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)<VAR>this✝ : MeasurableSet (Ioi 0)<VAR>this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)<VAR>t1 : Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))<VAR>t2 : Tendsto (fun c => ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2)))<GOAL>∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)
<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>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>s t : Set α<VAR>ht : MeasurableSet t<GOAL>((sum μ).restrict s) t = (sum fun i => (μ i).restrict s) t
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℤ → M<VAR>hf : HasProd f m<GOAL>HasProd (fun n => f ↑n * f (-↑n)) (m * f 0)
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℤ → M<VAR>hf : HasProd f m<VAR>u : Finset ℤ<GOAL>∃ v, ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<GOAL>Irreducible p ↔ p.roots = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<GOAL>Irreducible p ↔ p.roots = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<VAR>hp1 : p ≠ 1<GOAL>Irreducible p ↔ p.roots = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<VAR>hp1 : p ≠ 1<GOAL>(∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<VAR>hp1 : p ≠ 1<GOAL>(∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔ ∀ (a : R), ¬X - C a ∣ p
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<VAR>hp1 : p ≠ 1<VAR>h : ∀ (a : R), ¬X - C a ∣ p<VAR>q : R[X]<VAR>hq : q.Monic<VAR>hq1 : q.natDegree = 1<GOAL>¬q ∣ p