ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ Ioc a b ↔ a < b
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup F'<VAR>inst✝⁶ : NormedSpace 𝕜 F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>E : Type u_5<VAR>inst✝³ : NormedLatticeAddCommGroup E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : OrderedSMul ℝ E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f|m] ≤ᶠ[ae μ] μ[g|m]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionCommMonoid α<VAR>a✝ b✝ c d a b : α<VAR>n : ℕ<GOAL>(a / b) ^ n = a ^ n / b ^ n
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<GOAL>WithTop.map (fun x => ↑x) ⋯.order - ↑(Exists.choose hf) = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>h : ⋯.order = ⊤<GOAL>WithTop.map (fun x => ↑x) ⋯.order - ↑(Exists.choose hf) = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>h : ¬⋯.order = ⊤<GOAL>WithTop.map (fun x => ↑x) ⋯.order - ↑(Exists.choose hf) = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>(Icc a b).Nonempty ↔ a ≤ b
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>x : α<VAR>y : β<GOAL>y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<GOAL>⊤ * f = ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s✝ : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<VAR>s : Set α<GOAL>s ∈ ⊤ * f → s ∈ ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s✝ : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<VAR>s : Set α<GOAL>(∃ t₂ ∈ f, univ * t₂ ⊆ s) → s = univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s✝ : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<VAR>s t : Set α<VAR>ht : t ∈ f<VAR>hs : univ * t ⊆ s<GOAL>s = univ
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>f✝¹ : α✝ → β✝<VAR>E I✝ s : Set α✝<VAR>M✝ : Matroid α✝<VAR>N : Matroid β✝<VAR>f✝ : α✝ ≃ β✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>M : Matroid α<VAR>f : α ≃ β<VAR>I X : Set β<GOAL>(M.mapEquiv f).Basis I X ↔ M.Basis (⇑f.symm '' I) (⇑f.symm '' X)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>f✝¹ : α✝ → β✝<VAR>E I✝ s : Set α✝<VAR>M✝ : Matroid α✝<VAR>N : Matroid β✝<VAR>f✝ : α✝ ≃ β✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>M : Matroid α<VAR>f : α ≃ β<VAR>I X : Set β<GOAL>(∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.Basis (⇑f.symm '' I) (⇑f.symm '' X)
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>y : F<GOAL>SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : F<VAR>hx : x ≠ 0<GOAL>SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>f : α →o β<VAR>g : β →o γ<VAR>hfc : ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)<VAR>hgc : ∀ (c : Chain β), g (ωSup c) = ωSup (c.map g)<VAR>c✝ : Chain α<GOAL>g (f (ωSup c✝)) = ωSup (c✝.map (g.comp f))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<GOAL>IsRadical 0 ↔ IsReduced R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<GOAL>IsRadical 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x
<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✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT') f = c • (setToL1 hT) 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✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 hT' = c • setToL1 hT
<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✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : ↥(Lp E 1 μ)<GOAL>(c • setToL1 hT).comp (coeToLp α E ℝ) = setToL1SCLM α E μ hT'
<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✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>c • (setToL1 hT) ↑f = (setToL1SCLM α E μ hT') f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>m : ℕ<VAR>hm : finrank K V ≤ m<GOAL>LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>m : ℕ<VAR>hm : finrank K V ≤ m<VAR>k : ℕ<VAR>h_k_le : k ≤ finrank K V<VAR>hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)<GOAL>LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<GOAL>¬Irreducible a
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<GOAL>¬¬IsUnit a ∨ ¬∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>ha : ℵ₀ ≤ a<VAR>h : ∀ (a_1 b : Cardinal.{u}), a = a_1 * b → IsUnit a_1 ∨ IsUnit b<GOAL>False
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁵ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : CompactSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<VAR>x : M<VAR>hx : x ∈ U<VAR>H₁ : ‖f x‖ = ‖f c‖<VAR>hd' : MDifferentiableOn I 𝓘(ℂ, F) (fun x => f x + f c) U<VAR>H₂ : ‖f x + f c‖ = ‖f c + f c‖<GOAL>‖f x + const M (f c) x‖ = ‖f x‖ + ‖const M (f c) x‖
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>x : α<VAR>xs : List α<GOAL>xs <+ orderedInsert r x xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>x : α<VAR>xs : List α<GOAL>xs <+ takeWhile (fun b => decide ¬r x b) xs ++ x :: dropWhile (fun b => decide ¬r x b) xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>x : α<VAR>xs : List α<GOAL>xs <+ takeWhile (fun b => decide ¬r x b) xs ++ dropWhile (fun b => decide ¬r x b) xs
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>this : HasPullback f i<GOAL>(Limits.pullback.lift (pullback.fst f hi) (pullback.snd f hi) ⋯ ≫ pullback.lift f hi (Limits.pullback.fst f i) (Limits.pullback.snd f i) ⋯) ≫ pullback.fst f hi = 𝟙 (pullback f hi) ≫ pullback.fst f hi
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>this : HasPullback f i<GOAL>pullback.lift f hi (Limits.pullback.fst f i) (Limits.pullback.snd f i) ⋯ ≫ Limits.pullback.lift (pullback.fst f hi) (pullback.snd f hi) ⋯ = 𝟙 (Limits.pullback f i)
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>this : HasPullback f i<GOAL>(pullback.lift f hi (Limits.pullback.fst f i) (Limits.pullback.snd f i) ⋯ ≫ Limits.pullback.lift (pullback.fst f hi) (pullback.snd f hi) ⋯) ≫ Limits.pullback.fst f i = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst f i
<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>this : HasPullback f i<GOAL>(pullback.lift f hi (Limits.pullback.fst f i) (Limits.pullback.snd f i) ⋯ ≫ Limits.pullback.lift (pullback.fst f hi) (pullback.snd f hi) ⋯) ≫ Limits.pullback.snd f i = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Filter α<VAR>G : Filter β<VAR>s : Set α<VAR>t : Set β<VAR>m : α → β<GOAL>MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y : E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>(convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y : E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>(convexHull 𝕜) ((convexHull 𝕜) s ∪ (convexHull 𝕜) t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<GOAL>(s ∪ t).Disjoint u ↔ s.Disjoint u ∧ t.Disjoint u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s✝ t✝ : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>s : Set α<VAR>sl : s ∈ l<VAR>hs : IntegrableOn f s μ<VAR>t : Set α<VAR>tl : t ∈ l<VAR>ht : IntegrableOn g t μ<GOAL>IntegrableAtFilter (f + g) l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g✝ : α → E<VAR>s✝ t✝ : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f g : α → E<VAR>s : Set α<VAR>sl : s ∈ l<VAR>hs : IntegrableOn f s μ<VAR>t : Set α<VAR>tl : t ∈ l<VAR>ht : IntegrableOn g t μ<GOAL>IntegrableOn (f + g) (s ∩ t) μ
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra K S<VAR>x : S<VAR>hx : IsIntegral K x<VAR>i : Fin (minpoly K x).natDegree<GOAL>(powerBasisAux hx) i = ⟨x, ⋯⟩ ^ ↑i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j : n<VAR>b✝ : n → α<VAR>c : m → α<VAR>inst✝ : Subsingleton n<VAR>A : Matrix m n R<VAR>i : n<VAR>b : m → R<VAR>x : m<VAR>y : n<GOAL>A.updateColumn i b x y = (col (Fin 1) b).submatrix id (Function.const n 0) x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f u : ℕ → α<VAR>n : ℕ<GOAL>dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>hs : a ∉ s<VAR>ht : a ∉ t<GOAL>cons a s hs ⊆ cons a t ht ↔ s ⊆ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>c : Composition n<VAR>v : Fin n → E<VAR>i : Fin c.length<GOAL>p.removeZero.applyComposition c v i = p.applyComposition c v i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<GOAL>GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>ideal_gc : GaloisConnection Ideal.span SetLike.coe<GOAL>GaloisConnection (fun s => zeroLocus 𝒜 s) fun t => ↑(vanishingIdeal t)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι' : Sort u_2<VAR>ι : Sort u_3<VAR>p : ι' → Prop<VAR>V : ι' → Set (α × α)<VAR>U : ι → Set α<VAR>hbasis : (𝓤 α).HasBasis p V<VAR>hK : IsCompact K<VAR>hopen : ∀ (j : ι), IsOpen (U j)<VAR>hcover : K ⊆ ⋃ j, U j<GOAL>∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>ι' : Sort u_2<VAR>ι : Sort u_3<VAR>p : ι' → Prop<VAR>V : ι' → Set (α × α)<VAR>U : ι → Set α<VAR>hbasis : (𝓤 α).HasBasis p V<VAR>hK : IsCompact K<VAR>hopen : ∀ (j : ι), IsOpen (U j)<VAR>hcover : K ⊆ ⋃ j, U j<GOAL>∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ i, ball x t ⊆ U i) → ∀ x ∈ K, ∃ i, ball x s ⊆ U i
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set (M × M')<VAR>p : TangentBundle (I.prod I') (M × M')<VAR>hs : UniqueMDiffWithinAt (I.prod I') s p.proj<GOAL>{ proj := p.proj.2, snd := (mfderivWithin (I.prod I') I' Prod.snd s p.proj) p.snd } = { proj := p.proj.2, snd := p.snd.2 }
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set (M × M')<VAR>p : TangentBundle (I.prod I') (M × M')<VAR>hs : UniqueMDiffWithinAt (I.prod I') s p.proj<GOAL>{ proj := p.proj.2, snd := (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd } = { proj := p.proj.2, snd := p.snd.2 }
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set (M × M')<VAR>p : TangentBundle (I.prod I') (M × M')<VAR>hs : UniqueMDiffWithinAt (I.prod I') s p.proj<GOAL>UniqueMDiffWithinAt (I.prod I') s p.proj
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>δ₁ : Type u_1<VAR>δ₂ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ₁<VAR>inst✝ : TopologicalSpace δ₂<VAR>φ₁ : C(δ₁, α)<VAR>φ₂ : C(δ₂, α)<VAR>h_proper₁ : IsProperMap ⇑φ₁<VAR>h_proper₂ : IsProperMap ⇑φ₂<VAR>h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ<VAR>𝔖 : Set (Set α) := {K | IsCompact K}<VAR>𝔗₁ : Set (Set δ₁) := {K | IsCompact K}<VAR>𝔗₂ : Set (Set δ₂) := {K | IsCompact K}<VAR>h_image₁ : MapsTo (fun x => ⇑φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => ⇑φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂<GOAL>inferInstanceAs (UniformSpace C(α, β)) = UniformSpace.comap (fun x => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x => x.comp φ₂) inferInstance
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>δ₁ : Type u_1<VAR>δ₂ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ₁<VAR>inst✝ : TopologicalSpace δ₂<VAR>φ₁ : C(δ₁, α)<VAR>φ₂ : C(δ₂, α)<VAR>h_proper₁ : IsProperMap ⇑φ₁<VAR>h_proper₂ : IsProperMap ⇑φ₂<VAR>h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ<VAR>𝔖 : Set (Set α) := {K | IsCompact K}<VAR>𝔗₁ : Set (Set δ₁) := {K | IsCompact K}<VAR>𝔗₂ : Set (Set δ₂) := {K | IsCompact K}<VAR>h_image₁ : MapsTo (fun x => ⇑φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => ⇑φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂<GOAL>inferInstanceAs (UniformSpace C(α, β)) = UniformSpace.comap (fun x => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x => x.comp φ₂) inferInstance
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>δ₁ : Type u_1<VAR>δ₂ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ₁<VAR>inst✝ : TopologicalSpace δ₂<VAR>φ₁ : C(δ₁, α)<VAR>φ₂ : C(δ₂, α)<VAR>h_proper₁ : IsProperMap ⇑φ₁<VAR>h_proper₂ : IsProperMap ⇑φ₂<VAR>h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ<VAR>𝔖 : Set (Set α) := {K | IsCompact K}<VAR>𝔗₁ : Set (Set δ₁) := {K | IsCompact K}<VAR>𝔗₂ : Set (Set δ₂) := {K | IsCompact K}<VAR>h_image₁ : MapsTo (fun x => ⇑φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => ⇑φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂<GOAL>UniformSpace.comap ((⇑(UniformOnFun.ofFun 𝔗₁) ∘ (fun x => x ∘ ⇑φ₁) ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ toUniformOnFunIsCompact) (UniformOnFun.uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap ((⇑(UniformOnFun.ofFun 𝔗₂) ∘ (fun x => x ∘ ⇑φ₂) ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ toUniformOnFunIsCompact) (UniformOnFun.uniformSpace δ₂ β 𝔗₂) = UniformSpace.comap (toUniformOnFunIsCompact ∘ fun x => x.comp φ₁) (UniformOnFun.uniformSpace δ₁ β {K | IsCompact K}) ⊓ UniformSpace.comap (toUniformOnFunIsCompact ∘ fun x => x.comp φ₂) (UniformOnFun.uniformSpace δ₂ β {K | IsCompact K})
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<VAR>h : a ∉ s<GOAL>(insert a b s).entries = ⟨a, b⟩ :: s.entries
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ < π / 2