ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>x✝ : Dual R M₂<GOAL>(∀ (x : M₁), (f.dualMap x✝) x = 0 x) ↔ ∀ (i : M₁), x✝ (f i) = 0
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : NonAssocSemiring R<VAR>s : Set Rᵐᵒᵖ<GOAL>(closure s).unop = closure (MulOpposite.op ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : NonAssocSemiring R<VAR>s : Set Rᵐᵒᵖ<GOAL>sInf {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} = sInf {S | MulOpposite.op ⁻¹' s ⊆ ↑S}
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>inst✝ : NonAssocSemiring R<VAR>s : Set Rᵐᵒᵖ<VAR>a : Subsemiring R<GOAL>a ∈ {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.op ⁻¹' s ⊆ ↑S}
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>c : E<GOAL>IntervalIntegrable (fun x => c) μ a b ↔ c = 0 ∨ μ (Ι a b) < ⊤
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>log b (b ^ x) = x
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>log b (b ^ x) = log b (b ^ x * 1 + 0)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>Convex ℝ (p.ball x r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>p.ball x r = {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z => z + -x) x_1 < r}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>y ∈ p.ball x r ↔ y ∈ {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z => z + -x) x_1 < r}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>p (y + -x) < r ↔ y ∈ {x_1 | (⇑p ∘ fun z => z + -x) x_1 < r}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>hR : R ⊆ M.E<VAR>hX : (M ↾ R).Dep X<GOAL>M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>hR : R ⊆ M.E<VAR>hX : ¬M.Indep X ∧ X ⊆ R<GOAL>M.Dep X
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>x : α<VAR>l₁ l₂ : List α<GOAL>x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂
<VAR>a b c : ℕ<VAR>h : a ≤ b<VAR>x : ℕ<GOAL>x ∈ insert a (Icc (a + 1) b) ↔ x ∈ Icc a b
<VAR>a b c : ℕ<VAR>h : a ≤ b<VAR>x : ℕ<GOAL>x = a ∨ a + 1 ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U✝ : TopCat<VAR>X : Scheme<VAR>f : U✝ ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>U : (X.restrict h).Opens<GOAL>(Hom.appIso (X.ofRestrict h) U).hom = (Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)).hom
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>map proj (𝓝 x) = 𝓝 (proj x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>a b : FactorSet α<VAR>h : a.prod = b.prod<VAR>this : a.prod.factors = b.prod.factors<GOAL>a = b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space Z<VAR>s : Set X<VAR>t : Set Y<VAR>f g : X → Y → Z<VAR>h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y<VAR>hf₁ : ∀ (x : X), Continuous (f x)<VAR>hf₂ : ∀ (y : Y), Continuous fun x => f x y<VAR>hg₁ : ∀ (x : X), Continuous (g x)<VAR>hg₂ : ∀ (y : Y), Continuous fun x => g x y<VAR>this : closure s ⊆ ⋂ y ∈ closure t, {x | f x y = g x y}<GOAL>∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(v.trim ⋯) i = ↑v i
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>p q : Subgroup G<VAR>h : p.toSubmonoid = q.toSubmonoid<GOAL>p = q
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>p q : Subgroup G<VAR>h : p.toSubmonoid = q.toSubmonoid<VAR>this : ↑p.toSubmonoid = ↑q.toSubmonoid<GOAL>p = q
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>p q : Subgroup G<VAR>h : p.toSubmonoid = q.toSubmonoid<VAR>this : ↑p = ↑q<GOAL>p = q
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b c : α<VAR>m n✝ : ℕ<VAR>hab : a ∣ b<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>a ∣ b ^ (n + 1)
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b c : α<VAR>m n✝ : ℕ<VAR>hab : a ∣ b<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>a ∣ b * b ^ n
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : RingQuot s →ₐ[S] B<GOAL>f = (liftAlgHom S) ⟨f.comp (mkAlgHom S s), ⋯⟩
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : RingQuot s →ₐ[S] B<GOAL>(liftAlgHom S) ((liftAlgHom S).symm f) = (liftAlgHom S) ⟨f.comp (mkAlgHom S s), ⋯⟩
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f : RingQuot s →ₐ[S] B<GOAL>{ toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ({ toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.symm f) = { toFun := fun f' => preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨f.comp (mkAlgHom S s), ⋯⟩
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Injective f<VAR>a : α<VAR>b : β<VAR>h : partialInv f b = some a<VAR>hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none<VAR>h' : ∃ a, f a = b<GOAL>f a = b
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Injective f<VAR>a : α<VAR>b : β<VAR>hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none<VAR>h' : ∃ a, f a = b<VAR>h : some (Classical.choose h') = some a<GOAL>f a = b
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Injective f<VAR>b : β<VAR>hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none<VAR>h' : ∃ a, f a = b<GOAL>f (Classical.choose h') = b
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Injective f<VAR>a : α<VAR>b : β<VAR>h : partialInv f b = some a<VAR>hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none<VAR>h' : ¬∃ a, f a = b<GOAL>f a = b
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Injective f<VAR>a : α<VAR>b : β<VAR>h : none = some a<VAR>hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none<VAR>h' : ¬∃ a, f a = b<GOAL>f a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>s t : Finset α<GOAL>sᶜˢ ⊼ t = t \\ s
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin (n + 1)) (Fin n) R<VAR>hv : ∑ j : Fin (n + 1), M j = 0<VAR>j₁ j₂ : Fin (n + 1)<GOAL>(M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin (n + 1)) (Fin n) R<VAR>hv : ∑ j : Fin (n + 1), M j = 0<VAR>j₁ j₂ : Fin (n + 1)<GOAL>∀ (j : Fin (n + 1)), (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
<VAR>p : ℝ × ℝ<GOAL>↑Complex.polarCoord.symm p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * I)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>rω : cs.IsReduced ω<GOAL>(cs.leftInvSeq ω).Nodup
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>rω : cs.IsReduced ω<GOAL>(cs.rightInvSeq ω.reverse).Nodup
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>rω : cs.IsReduced ω<GOAL>cs.IsReduced ω.reverse
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : FunLike 𝓕 E F<VAR>ι : Type u_11<VAR>inst✝² : Fintype ι<VAR>M : ι → Type u_12<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (M i)<VAR>C : ℝ<VAR>L : (i : ι) → E →L[𝕜] M i<VAR>hL : ∀ (i : ι), ‖L i‖ ≤ C<VAR>hC : 0 ≤ C<GOAL>‖pi L‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : FunLike 𝓕 E F<VAR>ι : Type u_11<VAR>inst✝² : Fintype ι<VAR>M : ι → Type u_12<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (M i)<VAR>C : ℝ<VAR>L : (i : ι) → E →L[𝕜] M i<VAR>hL : ∀ (i : ι), ‖L i‖ ≤ C<VAR>hC : 0 ≤ C<VAR>x : E<GOAL>‖(pi L) x‖ ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : FunLike 𝓕 E F<VAR>ι : Type u_11<VAR>inst✝² : Fintype ι<VAR>M : ι → Type u_12<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (M i)<VAR>C : ℝ<VAR>L : (i : ι) → E →L[𝕜] M i<VAR>hL : ∀ (i : ι), ‖L i‖ ≤ C<VAR>hC : 0 ≤ C<VAR>x : E<VAR>i : ι<GOAL>‖(pi L) x i‖ ≤ C * ‖x‖
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a b : A<VAR>ha : autoParam (0 ≤ a) _auto✝<VAR>hab : a ≤ b<GOAL>‖a‖ ≤ ‖b‖
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a b : A<VAR>ha : autoParam (0 ≤ a) _auto✝<VAR>hab : a ≤ b<GOAL>∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a✝ b✝ : A<VAR>ha✝ : autoParam (0 ≤ a✝) _auto✝<VAR>hab✝ : a✝ ≤ b✝<VAR>a b : Unitization ℂ A<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<VAR>hb_nonneg : 0 ≤ b<VAR>this : 0 ≤ a<GOAL>‖a‖ ≤ ‖b‖
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a✝ b✝ : A<VAR>ha✝ : autoParam (0 ≤ a✝) _auto✝<VAR>hab✝ : a✝ ≤ b✝<VAR>a b : Unitization ℂ A<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<VAR>hb_nonneg : 0 ≤ b<VAR>this : 0 ≤ a<VAR>h₂ : cfc id a ≤ cfc (fun x => ‖b‖) a<GOAL>‖a‖ ≤ ‖b‖
<VAR>A : Type u_1<VAR>inst✝⁹ : NonUnitalNormedRing A<VAR>inst✝⁸ : CompleteSpace A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a✝ b✝ : A<VAR>ha✝ : autoParam (0 ≤ a✝) _auto✝<VAR>hab✝ : a✝ ≤ b✝<VAR>a b : Unitization ℂ A<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<VAR>hb_nonneg : 0 ≤ b<VAR>this : 0 ≤ a<VAR>h₂ : ∀ x ∈ spectrum ℝ a, id x ≤ ‖b‖<GOAL>‖a‖ ≤ ‖b‖
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>a : α<VAR>h : ∀ (a : α), a ∈ x → p a<VAR>ha : a ∈ x<GOAL>f a ⋯ ∈ pmap f x h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>a : α<VAR>h : ∀ (a : α), a ∈ x → p a<VAR>ha✝ : a ∈ x<VAR>ha : x = some a<GOAL>pmap f x h = some (f a ⋯)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<GOAL>x ∈ s.toList ↔ x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑s.card * ∑ i ∈ s, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f g : ι → α<VAR>hfg : MonovaryOn f g ↑s<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ s.card • ∑ i ∈ s, f i * g i
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>h : (f i) x = 0<GOAL>f.toPOUFun i x = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hx : 0 < x<VAR>hy : y < 1<VAR>y_pos : ¬y ≤ 0<GOAL>∃ n, y ^ n < x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hx : 0 < x<VAR>hy : y < 1<VAR>y_pos : 0 < y<GOAL>∃ n, y ^ n < x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hx : 0 < x<VAR>hy : y < 1<VAR>y_pos : 0 < y<VAR>q : ℕ<VAR>hq : x⁻¹ < y⁻¹ ^ q<GOAL>∃ n, y ^ n < x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : LeftInvOn g f s<VAR>F : Filter α<VAR>hF : F ≤ 𝓟 s<GOAL>map g (map f F) = F
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : LeftInvOn g f s<VAR>F : Filter α<VAR>hF : F ≤ 𝓟 s<VAR>this : g ∘ f =ᶠ[𝓟 s] id<GOAL>map g (map f F) = F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.WeaklyRegular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<GOAL>(μ.restrict A).WeaklyRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.WeaklyRegular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<VAR>this : Fact (μ A < ⊤)<GOAL>(μ.restrict A).WeaklyRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.WeaklyRegular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<VAR>this : Fact (μ A < ⊤)<VAR>V : Set α<VAR>V_open : IsOpen V<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) V<GOAL>∃ K ⊆ V, IsClosed K ∧ r < (μ.restrict A) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.WeaklyRegular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<VAR>this✝ : Fact (μ A < ⊤)<VAR>V : Set α<VAR>V_open : IsOpen V<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) V<VAR>this : (μ.restrict A).InnerRegularWRT IsClosed fun s => MeasurableSet s<GOAL>∃ K ⊆ V, IsClosed K ∧ r < (μ.restrict A) K
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map f (weightSpace M χ) ≤ weightSpace M₂ χ
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>weightSpace M χ ≤ LieSubmodule.comap f (weightSpace M₂ χ)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>m : M<VAR>hm : m ∈ weightSpace M χ<GOAL>m ∈ LieSubmodule.comap f (weightSpace M₂ χ)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>m : M<VAR>hm : m ∈ weightSpace M χ<GOAL>∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>m : M<VAR>hm : m ∈ weightSpace M χ<VAR>x : L<VAR>this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)<GOAL>∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0