ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>N : Submodule R M<VAR>x : ↥N<GOAL>x ∈ I • ⊤ ↔ N.subtype x ∈ I • N
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>N : Submodule R M<VAR>x : ↥N<VAR>this : map N.subtype (I • ⊤) = I • N<GOAL>x ∈ I • ⊤ ↔ N.subtype x ∈ I • N
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>N : Submodule R M<VAR>x : ↥N<VAR>this : map N.subtype (I • ⊤) = I • N<GOAL>x ∈ I • ⊤ ↔ N.subtype x ∈ map N.subtype (I • ⊤)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddMonoid α<VAR>h : Periodic f c<VAR>n : ℕ<GOAL>Periodic f (n • c)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra K F<VAR>ι : Type w<VAR>inst✝³ : Finite ι<VAR>inst✝² : Nontrivial S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a✝ : Nontrivial R<GOAL>(norm R) 0 = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁹ : CommRing R₂<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : Module R₂ M₂<VAR>e✝ : Basis ι R M<VAR>v✝ : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>b✝ : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : Finite κ<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq ι'<VAR>b : Basis ι R M<VAR>v : ι' → M<VAR>e : ι ≃ ι'<VAR>i✝ j✝ : ι'<GOAL>(b.reindex e).toMatrix v i✝ j✝ = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e)) i✝ j✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ X).hom ▷ 𝟙_ C = (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>((((α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (α_ (𝟙_ C) (𝟙_ C) X).hom) ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv) ≫ (λ_ X).hom ▷ 𝟙_ C = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom) ≫ (β_ X (𝟙_ C)).inv = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv = (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom = (ρ_ X).hom ▷ 𝟙_ C
<VAR>α : Type u_1<VAR>inst✝¹ : Add α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x + y) = (equivShrink α).symm x + (equivShrink α).symm y
<VAR>α : Type u_1<VAR>inst✝¹ : Add α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x + (equivShrink α).symm y)) = (equivShrink α).symm x + (equivShrink α).symm y
<VAR>x : ℝ≥0<GOAL>↑(↑x * ⊤) = ↑↑x * ↑⊤
<VAR>x y : ℝ≥0<GOAL>↑(↑x * ↑y) = ↑↑x * ↑↑y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<GOAL>IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>r : R<VAR>rs : List R<GOAL>IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>hμ : HasEigenvalue T μ<GOAL>(starRingEnd 𝕜) μ = μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>hμ : HasEigenvalue T μ<VAR>v : E<VAR>hv₁ : v ∈ eigenspace T μ<VAR>hv₂ : v ≠ 0<GOAL>(starRingEnd 𝕜) μ = μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>hμ : HasEigenvalue T μ<VAR>v : E<VAR>hv₁ : T v = μ • v<VAR>hv₂ : v ≠ 0<GOAL>(starRingEnd 𝕜) μ = μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>R₃ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R₂<VAR>inst✝⁸ : Ring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>inst✝² : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>ker g ≤ range f ↔ (range f).mkQ ∘ₗ (ker g).subtype = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>μ : Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun x => ∑' (i : ι), f i x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>μ : Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun x => ⨆ s, ∑ i ∈ s, f i x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>μ : Measure α<VAR>h : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>∀ (i : Finset ι), AEMeasurable (fun b => ∑ i ∈ i, f i b) μ
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(ndinsert a s).lcm = GCDMonoid.lcm a s.lcm
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : StandardBorelSpace α<VAR>inst✝ : Finite α<GOAL>∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : StandardBorelSpace α<VAR>inst✝ : Finite α<VAR>n : ℕ<VAR>n_equiv : α ≃ Fin n<GOAL>∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : StandardBorelSpace α<VAR>inst✝ : Finite α<VAR>n : ℕ<VAR>n_equiv : α ≃ Fin n<GOAL>Fin n ≃ ↑(range fun x => ↑↑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>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C<GOAL>‖f‖ ≤ 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>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>‖f 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>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<VAR>H₁ : ‖‖x‖⁻¹ • x‖ = 1<GOAL>‖f 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>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<VAR>H₁ : ‖‖x‖⁻¹ • x‖ = 1<VAR>H₂ : ‖f (‖x‖⁻¹ • x)‖ ≤ C<GOAL>‖f 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>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<VAR>H₁ : ‖‖x‖⁻¹ • x‖ = 1<VAR>H₂ : ‖f x‖ / ‖x‖ ≤ C<GOAL>0 < ‖x‖
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>comap some (𝓝 ∞) = coclosedCompact X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : M.Base B<VAR>h : B.Nonempty<GOAL>M.RkPos
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : M.Base B<VAR>h : B.Nonempty<GOAL>¬M.Base ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB : M.Base B<VAR>h : B.Nonempty<VAR>he : M.Base ∅<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>he hB : M.Base ∅<VAR>h : ∅.Nonempty<GOAL>False
<VAR>x : ℂ<VAR>y : ℝ<GOAL>(x ^ ↑y).im = abs x ^ y * Real.sin (x.arg * y)
<VAR>x : ℂ<VAR>y : ℝ<GOAL>(↑(abs x ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).im = abs x ^ y * Real.sin (x.arg * y)
<VAR>a b c : Ordinal.{u_1}<VAR>ba : b + a = a<GOAL>(a + b) * succ c = a * succ c + b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>univ.Nonempty ↔ Nonempty α
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<GOAL>CompleteLattice.Independent fun i => (ϕ i).range
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<GOAL>CompleteLattice.Independent fun i => (ϕ i).range
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<GOAL>Disjoint ((fun i => (ϕ i).range) i) (⨆ j, ⨆ (_ : j ≠ i), (fun i => (ϕ i).range) j)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<GOAL>(fun i => (ϕ i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i => (ϕ i).range) j ≤ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxi : f ∈ Set.range ⇑(ϕ i)<VAR>hxp : f ∈ ↑(⨆ j, ⨆ (_ : ¬j = i), (ϕ j).range)<GOAL>f ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxi : f ∈ Set.range ⇑(ϕ i)<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>hxp : f ∈ ↑(noncommPiCoprod (fun x => ϕ ↑x) ?intro.intro.hcomm).range<GOAL>f ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxi : f ∈ Set.range ⇑(ϕ i)<VAR>hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)<GOAL>Pairwise fun i_1 j => ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<GOAL>f ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<GOAL>f ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<GOAL>f ∈ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝² : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f✝ g✝ : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype (H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card (H i)).Coprime (Fintype.card (H j))<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>f : G<VAR>hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)<VAR>g : (i_1 : { j // ¬j = i }) → H ↑i_1<VAR>hgf : (noncommPiCoprod (fun x => ϕ ↑x) ⋯) g = f<VAR>g' : H i<VAR>hg'f : (ϕ i) g' = f<VAR>hxi : orderOf f ∣ Fintype.card (H i)<VAR>hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)<GOAL>f = 1