ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Countable G<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)<VAR>aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)<VAR>h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ<VAR>h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s} μ<GOAL>∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Countable G<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)<VAR>aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)<VAR>h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ<VAR>h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s} μ<GOAL>μ (⋃ g, g • s) = μ univ
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Countable G<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)<VAR>aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)<VAR>h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ<VAR>h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s} μ<GOAL>μ univ ≤ μ (⋃ g, g • s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Countable G<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)<VAR>aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)<VAR>h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ<VAR>h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s} μ<GOAL>μ univ ≤ ∑' (i : G), μ (i • s)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>I : LieIdeal R L<GOAL>⁅I, maxTrivSubmodule R L M⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>I : LieIdeal R L<GOAL>∀ x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}, x = 0
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>r : R<GOAL>(mapRingHom f) (C r) = C (f r)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (a : Ω) in s, -f j a ∂μ ≤ ∫ (a : Ω) in s, -f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : UniformSpace α<VAR>inst✝⁶ : Group α<VAR>inst✝⁵ : UniformGroup α<VAR>hom : Type u_3<VAR>inst✝⁴ : UniformSpace β<VAR>inst✝³ : Group β<VAR>inst✝² : UniformGroup β<VAR>inst✝¹ : FunLike hom α β<VAR>inst✝ : MonoidHomClass hom α β<VAR>f : hom<VAR>h : Tendsto (⇑f) (𝓝 1) (𝓝 1)<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : UniformSpace α<VAR>inst✝⁶ : Group α<VAR>inst✝⁵ : UniformGroup α<VAR>hom : Type u_3<VAR>inst✝⁴ : UniformSpace β<VAR>inst✝³ : Group β<VAR>inst✝² : UniformGroup β<VAR>inst✝¹ : FunLike hom α β<VAR>inst✝ : MonoidHomClass hom α β<VAR>f : hom<VAR>h : Tendsto (⇑f) (𝓝 1) (𝓝 1)<VAR>this : ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : UniformSpace α<VAR>inst✝⁶ : Group α<VAR>inst✝⁵ : UniformGroup α<VAR>hom : Type u_3<VAR>inst✝⁴ : UniformSpace β<VAR>inst✝³ : Group β<VAR>inst✝² : UniformGroup β<VAR>inst✝¹ : FunLike hom α β<VAR>inst✝ : MonoidHomClass hom α β<VAR>f : hom<VAR>h : Tendsto (⇑f) (𝓝 1) (𝓝 1)<VAR>this : ((fun x => x.2 / x.1) ∘ fun x => (f x.1, f x.2)) = fun x => f (x.2 / x.1)<GOAL>Tendsto (fun x => f (x.2 / x.1)) (comap (fun x => x.2 / x.1) (𝓝 1)) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : Countable ι<VAR>t : ι → Set α<VAR>f : (i : ι) → ↑(t i) → β<VAR>htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ ⋃ i, t i<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>hfm : ∀ (i : ι), Measurable (f i)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : Countable ι<VAR>t : ι → Set α<VAR>f : (i : ι) → ↑(t i) → β<VAR>htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ ⋃ i, t i<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>hfm : ∀ (i : ι), Measurable (f i)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (inclusion hT ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' s))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>eval {fun x => false} default ≠ 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>ℐ : Set (Ideal A)<VAR>h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I<GOAL>IsHomogeneous 𝒜 (SupSet.sSup ℐ)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>ℐ : Set (Ideal A)<VAR>h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I<GOAL>IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>ba : b ≤ a<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + finrank 𝕜 ↥(Kᗮ ⊓ ⊤)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>K : Submodule 𝕜 E<GOAL>finrank 𝕜 E = finrank 𝕜 ↥⊤
<VAR>n m k : ℕ<GOAL>map (fun x => k + x) (Ico n m) = Ico (n + k) (m + k)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : LiftPropAt P g x<GOAL>LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : LiftPropWithinAt P g univ x<GOAL>LiftPropWithinAt P g s x
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>μ : Measure G<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K₀ : PositiveCompacts G<GOAL>μ = μ ↑K₀ • haarMeasure K₀
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>μ : Measure G<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K₀ : PositiveCompacts G<VAR>A : (interior (closure ↑K₀)).Nonempty<GOAL>μ = μ ↑K₀ • haarMeasure K₀
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>μ : Measure G<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K₀ : PositiveCompacts G<VAR>A : (interior (closure ↑K₀)).Nonempty<VAR>this : μ = (μ (closure ↑K₀) / (haarMeasure K₀) (closure ↑K₀)) • haarMeasure K₀<GOAL>μ = μ ↑K₀ • haarMeasure K₀
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝ : Group G<VAR>a b : G<GOAL>(fun b => b⁻¹ * a) ((fun b => a / b) b) = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝ : Group G<VAR>a b : G<GOAL>(fun b => a / b) ((fun b => b⁻¹ * a) b) = b
<VAR>n : ℕ<VAR>hn : n ≤ 1<VAR>b : ℕ<GOAL>clog b n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : DivisionRing R<VAR>p q : R[X]<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<GOAL>map f p = 0 ↔ p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : DivisionRing R<VAR>p q : R[X]<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<GOAL>(∀ (n : ℕ), (map f p).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), p.coeff n = coeff 0 n
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : DivisionRing R<VAR>p q : R[X]<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<VAR>a✝ : ℕ<GOAL>(map f p).coeff a✝ = coeff 0 a✝ ↔ p.coeff a✝ = coeff 0 a✝
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>b ≤ a * 1 ↔ b ≤ a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>h : Subsingleton M<VAR>x y : Submonoid M<VAR>i : M<GOAL>1 ∈ x ↔ 1 ∈ y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : ι → Submodule R M<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, ↑(p i) = Set.univ<GOAL>⋃ i ∈ s, 0 +ᵥ ↑(p i).toAddSubgroup = Set.univ
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a✝ b✝ : G<GOAL>(setoid ↑⊥.toSubmonoid ↑H).Rel a✝ b✝ ↔ (QuotientGroup.leftRel H).Rel a✝ b✝
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a✝ b✝ : G<GOAL>(setoid ↑⊥.toSubmonoid ↑H).Rel a✝ b✝ ↔ (setoid ↑⊥ ↑H).Rel a✝ b✝
<VAR>n m l : ℕ<GOAL>n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
<VAR>n m l : ℕ<VAR>hnm : n ≤ m<GOAL>n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
<VAR>n m l : ℕ<VAR>hmn : m ≤ n<GOAL>n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>𝔸 : Type u_3<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝔸<VAR>inst✝³ : NormedCommRing 𝔸'<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>inst✝¹ : NormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>c : 𝕜'<GOAL>ContDiff 𝕜 n fun x => f x / c
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>Complex.normSq ((o.kahler x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Reflexive R<VAR>s✝ s t : WSeq α<VAR>h : s = t<GOAL>Computation.LiftRel (LiftRelO R fun x x_1 => x = x_1) s.destruct s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → α → Prop<VAR>H : Reflexive R<VAR>s✝ s t : WSeq α<VAR>h : s = t<GOAL>Reflexive (LiftRelO R fun x x_1 => x = x_1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ Y X : SimplicialObject C<VAR>n : ℕ<GOAL>(obj X).d (n + 1) n = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f : α → β<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(Measure.dirac (f a)) s = s.indicator 1 (f a)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hy : y.Numeric<VAR>ihyx : IH1 y x<VAR>i : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>y.moveLeft k < -(-y).moveLeft l
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hy : y.Numeric<VAR>ihyx : IH1 y x<VAR>i : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>y.moveLeft k < y.moveRight (toLeftMovesNeg.symm l)
<VAR>x : ℂ<GOAL>x ^ 0 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>n : ℕ := max p.natDegree (map f p).natDegree<GOAL>derivative (map f p) = map f (derivative p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>n : ℕ := max p.natDegree (map f p).natDegree<GOAL>((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a => C (a * ↑n) * X ^ (n - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>n : ℕ := max p.natDegree (map f p).natDegree<GOAL>((map f p).sum fun n a => C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>n : ℕ := max p.natDegree (map f p).natDegree<GOAL>∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>n : ℕ := max p.natDegree (map f p).natDegree<GOAL>∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CancelCommMonoidWithZero R<VAR>inst✝² : UniqueFactorizationMonoid R<VAR>inst✝¹ : NormalizationMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>a b : R<VAR>n : ℕ<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>↑n ≤ multiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CancelCommMonoidWithZero R<VAR>inst✝² : UniqueFactorizationMonoid R<VAR>inst✝¹ : NormalizationMonoid R<VAR>inst✝ : DecidableRel Dvd.dvd<VAR>a b : R<VAR>n : ℕ<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b
<VAR>x y z : ℝ<VAR>n : ℕ<GOAL>deriv^[n + 1] rexp = rexp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Preorder α<VAR>f : α → Part β<VAR>g : α → β → Part γ<VAR>hf : Antitone f<VAR>hg : Antitone g<VAR>x y : α<VAR>h : x ≤ y<VAR>a : γ<GOAL>a ∈ (fun x => (f x).bind (g x)) y → a ∈ (fun x => (f x).bind (g x)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Preorder α<VAR>f : α → Part β<VAR>g : α → β → Part γ<VAR>hf : Antitone f<VAR>hg : Antitone g<VAR>x y : α<VAR>h : x ≤ y<VAR>a : γ<GOAL>∀ x_1 ∈ f y, a ∈ g y x_1 → ∃ a_3 ∈ f x, a ∈ g x a_3
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(lineMap p₀ p₁) (1 - c) = (lineMap p₁ p₀) c
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(lineMap p₁ p₀) ((lineMap 1 0) (1 - c)) = (lineMap p₁ p₀) c
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(lineMap 1 0) (1 - c) = c
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<GOAL>∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<VAR>hB : ∀ (j : ↑(Icc 0 n)), IsClosed (B j)<GOAL>∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<VAR>hB : ∀ (j : ↑(Icc 0 n)), IsClosed (B j)<VAR>h : Pairwise (Disjoint on B)<GOAL>False
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<VAR>hB : ∀ (j : ↑(Icc 0 n)), IsClosed (B j)<VAR>h : Pairwise (Disjoint on B)<GOAL>n = 0