ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>hc0 : ¬c = 0<GOAL>c ^ (1 / p).toReal ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a✝ b a : α<VAR>f : β → α<GOAL>⨆ o, o.elim a f = a ⊔ ⨆ b, f b
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>inst✝⁶ : CompleteSpace E'<VAR>inst✝⁵ : NormedSpace ℝ E'<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>inst✝⁶ : CompleteSpace E'<VAR>inst✝⁵ : NormedSpace ℝ E'<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<GOAL>AEStronglyMeasurable'.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable'.mk g hgm
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>inst✝⁶ : CompleteSpace E'<VAR>inst✝⁵ : NormedSpace ℝ E'<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>hf_mk_int_finite : ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s (μ.trim hm)<GOAL>AEStronglyMeasurable'.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable'.mk g hgm
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>inst✝⁶ : CompleteSpace E'<VAR>inst✝⁵ : NormedSpace ℝ E'<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>hf_mk_int_finite : ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s (μ.trim hm)<VAR>hg_mk_int_finite : ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s (μ.trim hm)<GOAL>AEStronglyMeasurable'.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable'.mk g hgm
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>inst✝⁶ : CompleteSpace E'<VAR>inst✝⁵ : NormedSpace ℝ E'<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hgm : AEStronglyMeasurable' m g μ<VAR>hf_mk_int_finite : ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s (μ.trim hm)<VAR>hg_mk_int_finite : ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s (μ.trim hm)<VAR>hfg_mk_eq : ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → ∫ (x : α) in s, AEStronglyMeasurable'.mk f hfm x ∂μ.trim hm = ∫ (x : α) in s, AEStronglyMeasurable'.mk g hgm x ∂μ.trim hm<GOAL>AEStronglyMeasurable'.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable'.mk g hgm
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>f : M → M'<VAR>hf : ContMDiff I I' n (e' ∘ f)<GOAL>ContMDiff I I' n f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>f : M → M'<VAR>hf : ContMDiff I I' n (e' ∘ f)<VAR>this : f = ↑(OpenEmbedding.toPartialHomeomorph e' h').symm ∘ e' ∘ f<GOAL>ContMDiff I I' n f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>f : M → M'<VAR>hf : ContMDiff I I' n (e' ∘ f)<VAR>this : f = ↑(OpenEmbedding.toPartialHomeomorph e' h').symm ∘ e' ∘ f<GOAL>ContMDiff I I' n (↑(OpenEmbedding.toPartialHomeomorph e' h').symm ∘ e' ∘ f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>f : M → M'<VAR>hf : ContMDiff I I' n (e' ∘ f)<VAR>this : f = ↑(OpenEmbedding.toPartialHomeomorph e' h').symm ∘ e' ∘ f<GOAL>∀ (x : M), (e' ∘ f) x ∈ range e'
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>modifyNth f n l = modifyNthTR f n l
<VAR>α : Type u_1<VAR>inst✝ : CircularOrder α<VAR>a b x✝ : α<GOAL>x✝ ∈ (cIoo a b)ᶜ ↔ x✝ ∈ cIcc b a
<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 𝒜 (InfSet.sInf ℐ)
<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>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s✝ s : Set G<VAR>a : G<VAR>h : a ∈ closure s<VAR>x✝² : G<VAR>x✝¹ : InClosure s x✝²<VAR>x✝ : ∃ l, (∀ x ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = x✝²<VAR>L : List G<VAR>HL1 : ∀ x ∈ L, x ∈ s ∨ x⁻¹ ∈ s<VAR>HL2 : L.prod = x✝²<VAR>x : G<VAR>hx : x ∈ List.map Inv.inv L.reverse<VAR>y : G<VAR>hy1 : y ∈ L.reverse<VAR>hy2 : y⁻¹ = x<GOAL>y ∈ s → y⁻¹⁻¹ ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s✝ s : Set G<VAR>a : G<VAR>h : a ∈ closure s<VAR>x✝² : G<VAR>x✝¹ : InClosure s x✝²<VAR>x✝ : ∃ l, (∀ x ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = x✝²<VAR>L : List G<VAR>HL1 : ∀ x ∈ L, x ∈ s ∨ x⁻¹ ∈ s<VAR>HL2 : L.prod = x✝²<VAR>x : G<VAR>hx : x ∈ List.map Inv.inv L.reverse<VAR>y : G<VAR>hy1 : y ∈ L.reverse<VAR>hy2 : y⁻¹ = x<GOAL>y ∈ s → y ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s✝ s : Set G<VAR>a : G<VAR>h : a ∈ closure s<VAR>x : G<VAR>x✝¹ : InClosure s x<VAR>x✝ : ∃ l, (∀ x ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = x<VAR>L : List G<VAR>HL1 : ∀ x ∈ L, x ∈ s ∨ x⁻¹ ∈ s<VAR>HL2 : L.prod = x<VAR>hd : G<VAR>tl : List G<VAR>ih : (List.map Inv.inv tl.reverse).prod = tl.prod⁻¹<GOAL>(List.map Inv.inv (hd :: tl).reverse).prod = (hd :: tl).prod⁻¹
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s✝ s : Set G<VAR>a : G<VAR>h : a ∈ closure s<VAR>x y : G<VAR>x✝³ : InClosure s x<VAR>x✝² : InClosure s y<VAR>x✝¹ : ∃ l, (∀ x ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = x<VAR>x✝ : ∃ l, (∀ x ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = y<VAR>L1 : List G<VAR>HL1 : ∀ x ∈ L1, x ∈ s ∨ x⁻¹ ∈ s<VAR>HL2 : L1.prod = x<VAR>L2 : List G<VAR>HL3 : ∀ x ∈ L2, x ∈ s ∨ x⁻¹ ∈ s<VAR>HL4 : L2.prod = y<GOAL>(L1 ++ L2).prod = x * y
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>H : Infinite (α ⊕ β)<GOAL>Infinite α ∨ Infinite β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>H : ¬Infinite α ∧ ¬Infinite β<GOAL>¬Infinite (α ⊕ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>H : ¬Infinite α ∧ ¬Infinite β<VAR>this : Fintype α<GOAL>¬Infinite (α ⊕ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>H : ¬Infinite α ∧ ¬Infinite β<VAR>this✝ : Fintype α<VAR>this : Fintype β<GOAL>¬Infinite (α ⊕ β)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<GOAL>ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t t' : Set (PrimeSpectrum R)<VAR>r : R<GOAL>r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t t' : Set (PrimeSpectrum R)<VAR>r : R<GOAL>(∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t t' : Set (PrimeSpectrum R)<VAR>f : R<VAR>hf : f ∈ vanishingIdeal t<VAR>g : R<VAR>hg : g ∈ vanishingIdeal t'<VAR>x : PrimeSpectrum R<VAR>hxt : x ∈ t<VAR>hxt' : x ∈ t'<GOAL>f + g ∈ x.asIdeal
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t t' : Set (PrimeSpectrum R)<VAR>f : R<VAR>hf : ∀ x ∈ t, f ∈ x.asIdeal<VAR>g : R<VAR>hg : ∀ x ∈ t', g ∈ x.asIdeal<VAR>x : PrimeSpectrum R<VAR>hxt : x ∈ t<VAR>hxt' : x ∈ t'<GOAL>f + g ∈ x.asIdeal
<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>inst✝ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : IsInternal V<VAR>hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>w : PiLp 2 fun i => ↥(V i)<GOAL>(hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i : ι, ↑(w i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>Independent (f ∘ Subtype.val) ↔ s.SupIndep f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List α<VAR>i : Fin L.length<GOAL>drop (↑i) (take (↑i + 1) L) = [L.get i]
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>sr i * sr i = 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s : Set X<GOAL>μ ≤ pre m r ↔ ∀ (s : Set X), diam s ≤ r → μ s ≤ m s
<VAR>x : ℝ<VAR>y : ℂ<VAR>h : 0 < y.re ∨ x ≠ 0<GOAL>ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)
<VAR>x : ℝ<VAR>y : ℂ<VAR>h : 0 < y.re ∨ x ≠ 0<VAR>hx : 0 < x<GOAL>ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)
<VAR>y : ℂ<VAR>h : 0 < y.re ∨ 0 ≠ 0<GOAL>ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)
<VAR>x : ℝ<VAR>y : ℂ<VAR>h : 0 < y.re ∨ x ≠ 0<VAR>hx : x < 0<GOAL>ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>FiniteDimensional.finrank K L = n
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>this : FiniteDimensional K L<GOAL>FiniteDimensional.finrank K L = n
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>this✝ : FiniteDimensional K L<VAR>this : IsGalois K L<GOAL>FiniteDimensional.finrank K L = n
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>this✝ : FiniteDimensional K L<VAR>this : IsGalois K L<VAR>hn : 0 < n<GOAL>FiniteDimensional.finrank K L = n
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>this✝¹ : FiniteDimensional K L<VAR>this✝ : IsGalois K L<VAR>hn : 0 < n<VAR>this : NeZero n<GOAL>FiniteDimensional.finrank K L = n
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>m : ℕ<VAR>heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K<VAR>hf : Surjective ⇑f<VAR>hi : Injective ⇑i<VAR>n : ℕ<GOAL>f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
<VAR>R : Type u<VAR>L : Type v<VAR>M : 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>N : LieSubmodule R L M<VAR>x : L<VAR>m : M<VAR>hm : m ∈ ↑↑N<GOAL>((toEnd R L M) x) m ∈ ↑N
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<GOAL>∀ (n : ℕ), (X * p.divX + C (p.coeff 0)).coeff n = p.coeff n
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>hf : ¬Summable f<GOAL>↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<GOAL>of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : of' R M m ∈ span R (of' R M '' S)<GOAL>m ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : ↑{m} ⊆ S<GOAL>m ∈ S
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c d : α<GOAL>↑(Icc a b * Ico c d) ⊆ ↑(Ico (a * c) (b * d))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Set α<VAR>t✝ t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → α → β<VAR>s t : Set α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t
<VAR>p n r b : ℕ<VAR>hp : Prime p<VAR>hbn : log p n < b<GOAL>p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>i.succ ≤ p ∨ p ≤ i.castSucc
<VAR>n₁ n₂ d₁ d₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂)
<VAR>q : Λ'<VAR>c : List Γ'<VAR>x : Γ'<VAR>b : List Γ'<VAR>IH : ∀ (s : Option Γ') (a d : List Γ'), Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d } { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }<VAR>s : Option Γ'<VAR>a d : List Γ'<GOAL>Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a (x :: b) c d } { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }
<VAR>q : Λ'<VAR>c : List Γ'<VAR>x : Γ'<VAR>b : List Γ'<VAR>IH : ∀ (s : Option Γ') (a d : List Γ'), Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d } { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }<VAR>s : Option Γ'<VAR>a d : List Γ'<GOAL>TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr q.copy) s (elim a (x :: b) c d)) { l := some q, var := none, stk := elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d) }
<VAR>q : Λ'<VAR>c : List Γ'<VAR>x : Γ'<VAR>b : List Γ'<VAR>IH : ∀ (s : Option Γ') (a d : List Γ'), Reaches₁ (TM2.step tr) { l := some q.copy, var := s, stk := elim a b c d } { l := some q, var := none, stk := elim (b.reverseAux a) [] c (b.reverseAux d) }<VAR>s : Option Γ'<VAR>a d : List Γ'<GOAL>TransGen (fun a b => (match a with | { l := none, var := var, stk := stk } => none | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) = some b) { l := some q.copy, var := some x, stk := elim ((some x).iget :: a) b c ((some x).iget :: d) } { l := some q, var := none, stk := elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d)) }
<VAR>n : ℤ<VAR>hn : n % 4 = 1<GOAL>χ₄ ↑n = 1
<VAR>n : ℤ<VAR>hn : n % 4 = 1<GOAL>χ₄ ↑1 = 1
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>zw : SqLe y d x c<VAR>h : SqLe (x + z) c (y + w) d<GOAL>SqLe z c w d
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>zw : SqLe y d x c<VAR>h : SqLe (x + z) c (y + w) d<GOAL>¬c * z * z > d * w * w
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>zw : SqLe y d x c<VAR>h : SqLe (x + z) c (y + w) d<VAR>l : c * z * z > d * w * w<GOAL>False
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>zw : SqLe y d x c<VAR>h : SqLe (x + z) c (y + w) d<VAR>l : c * z * z > d * w * w<GOAL>c * (x + z) * (x + z) > d * (y + w) * (y + w)