ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SecondCountableTopology H<VAR>inst✝ : SigmaCompactSpace M<GOAL>SecondCountableTopology M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SecondCountableTopology H<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hsc : s.Countable<VAR>hsU : ⋃ x ∈ s, (chartAt H x).source = univ<GOAL>SecondCountableTopology M
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P'<GOAL>(canonicalEquiv S P P') ((canonicalEquiv S P' P) I) = I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P'<GOAL>(canonicalEquiv S P' P).symm ((canonicalEquiv S P' P) I) = I
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.320996<VAR>Bₘ : Type ?u.320999<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Module.Free A B<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(intTrace A B) x = (trace A B) x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.320996<VAR>Bₘ : Type ?u.320999<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Module.Free A B<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(intTrace A B) x = (trace A B) x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁰ : CommRing A<VAR>inst✝²⁹ : CommRing B<VAR>inst✝²⁸ : Algebra A B<VAR>inst✝²⁷ : Field K<VAR>inst✝²⁶ : Field L<VAR>inst✝²⁵ : Algebra A K<VAR>inst✝²⁴ : IsFractionRing A K<VAR>inst✝²³ : Algebra B L<VAR>inst✝²² : Algebra K L<VAR>inst✝²¹ : Algebra A L<VAR>inst✝²⁰ : IsScalarTower A B L<VAR>inst✝¹⁹ : IsScalarTower A K L<VAR>inst✝¹⁸ : IsIntegralClosure B A L<VAR>inst✝¹⁷ : FiniteDimensional K L<VAR>Aₘ : Type ?u.320996<VAR>Bₘ : Type ?u.320999<VAR>inst✝¹⁶ : CommRing Aₘ<VAR>inst✝¹⁵ : CommRing Bₘ<VAR>inst✝¹⁴ : Algebra Aₘ Bₘ<VAR>inst✝¹³ : Algebra A Aₘ<VAR>inst✝¹² : Algebra B Bₘ<VAR>inst✝¹¹ : Algebra A Bₘ<VAR>inst✝¹⁰ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁸ : IsLocalization M Aₘ<VAR>inst✝⁷ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Module.Free A B<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intTrace A B) x) = (algebraMap A (FractionRing A)) ((trace A B) x)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : ‖a‖₊ ≤ t<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : ‖a‖₊ ≤ t<VAR>this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : spectralRadius ℝ a ≤ ↑t<VAR>this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : spectralRadius ℝ a ≤ ↑t<VAR>this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)<GOAL>SpectrumRestricts ((algebraMap ℝ A) ↑t - a) ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : spectralRadius ℂ a ≤ ↑t<VAR>this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)<GOAL>SpectrumRestricts a ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : spectralRadius ℂ a ≤ ↑t<VAR>this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)<GOAL>IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ha : IsSelfAdjoint a<VAR>ht : ↑‖a‖₊ ≤ ↑t<VAR>this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)<GOAL>IsSelfAdjoint a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>a : α<VAR>ha : a ∈ s<GOAL>Tendsto (fun i => F i a) p (𝓝 (f a))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>a : α<VAR>ha : a ∈ s<GOAL>𝓟 {a} ≤ 𝓝[s] a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>(trunc (n + 1) f).natDegree < n + 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>∀ (N : ℕ), n < N → (trunc (n + 1) f).coeff N = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n N✝ : ℕ<VAR>a✝ : n < N✝<GOAL>(trunc (n + 1) f).coeff N✝ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n N✝ : ℕ<VAR>a✝ : n < N✝<GOAL>(if N✝ < n + 1 then (coeff R N✝) f else 0) = 0
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>d : ℕ<GOAL>selfZPow x B (-↑d) = mk' B 1 (Submonoid.pow x d)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : Cᵒᵖ<GOAL>IsDetector (unop G) ↔ IsCodetector G
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f✝ g : ι → N<VAR>s✝ t s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, f x ≤ n<GOAL>s.prod f ≤ n ^ s.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f✝ g : ι → N<VAR>s✝ t s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, f x ≤ n<GOAL>∀ x ∈ Multiset.map f s.val, x ≤ n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f✝ g : ι → N<VAR>s✝ t s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, f x ≤ n<GOAL>n ^ Multiset.card (Multiset.map f s.val) ≤ n ^ s.card
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Mul R<VAR>inst✝ : HasDistribNeg R<VAR>a x y : R<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy a (-x) (-y)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p q a b : MvPolynomial σ R<GOAL>(a - b).totalDegree = (a + -b).totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p q a b : MvPolynomial σ R<GOAL>max a.totalDegree (-b).totalDegree = max a.totalDegree b.totalDegree
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>T : Set (Set X)<VAR>To : ∀ t ∈ T, IsOpen t<VAR>Tct : T.Countable<VAR>hd : Dense (⋂₀ T)<GOAL>⋂₀ T ∈ residual X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : ↑M.E ↪ β<VAR>I : Set β<GOAL>(M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : ↑M.E ↪ β<VAR>I : Set β<GOAL>(M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : ↑M.E ↪ β<VAR>I : Set ↑M.E<VAR>hI : M.Indep ↑I<GOAL>M.Indep ↑(⇑f ⁻¹' (⇑f '' I)) ∧ ∃ t, ⇑f '' t = ⇑f '' I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : ↑M.E ↪ β<VAR>I : Set ↑M.E<VAR>hI : M.Indep ↑I<GOAL>M.Indep ↑I ∧ ∃ t, ⇑f '' t = ⇑f '' I
<VAR>n : ℕ<GOAL>aleph' (succ ↑n) = ↑n.succ
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : a ^ 4 + b ^ 4 = c ^ 2<GOAL>False
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : a ^ 4 + b ^ 4 = c ^ 2<VAR>a0 b0 c0 : ℤ<VAR>hf : Fermat42.Minimal a0 b0 c0<VAR>h2 : a0 % 2 = 1<VAR>hp : 0 < c0<GOAL>False
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>tensor_μ C (M.X, N.X) (M.X, N.X) ▷ (M.X ⊗ N.X) ≫ (M.mul ⊗ N.mul) ▷ (M.X ⊗ N.X) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) = (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.X ⊗ N.X) ◁ (M.mul ⊗ N.mul) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>tensor_μ C (M.X, N.X) (M.X, N.X) ▷ (M.X ⊗ N.X) ≫ (tensor_μ C (M.X ⊗ M.X, N.X ⊗ N.X) (M.X, N.X) ≫ (M.mul ▷ M.X ⊗ N.mul ▷ N.X)) ≫ (M.mul ⊗ N.mul) = (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.X ⊗ N.X) ◁ (M.mul ⊗ N.mul) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>tensor_μ C (M.X, N.X) (M.X, N.X) ▷ (M.X ⊗ N.X) ≫ tensor_μ C (M.X ⊗ M.X, N.X ⊗ N.X) (M.X, N.X) ≫ ((α_ M.X M.X M.X).hom ⊗ (α_ N.X N.X N.X).hom) ≫ (M.X ◁ M.mul ⊗ N.X ◁ N.mul) ≫ (M.mul ⊗ N.mul) = (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.X ⊗ N.X) ◁ (M.mul ⊗ N.mul) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(((α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ tensor_μ C (M.X, N.X) (M.X ⊗ M.X, N.X ⊗ N.X)) ≫ (M.X ◁ M.mul ⊗ N.X ◁ N.mul)) ≫ (M.mul ⊗ N.mul) = (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.X ⊗ N.X) ◁ (M.mul ⊗ N.mul) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M N : Mon_ C<GOAL>(α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ ((M.X ⊗ N.X) ◁ (M.mul ⊗ N.mul) ≫ tensor_μ C (M.X, N.X) (M.X, N.X)) ≫ (M.mul ⊗ N.mul) = (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.X ⊗ N.X) ◁ (M.mul ⊗ N.mul) ≫ tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<GOAL>s.chainHeight = ⊤ ↔ ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n<GOAL>s.chainHeight = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>h : s.chainHeight ≠ ⊤<GOAL>∃ n, ∀ l ∈ s.subchain, l.length ≠ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>h : s.chainHeight ≠ ⊤<VAR>n : ℕ<VAR>hn : ↑n = s.chainHeight<GOAL>∃ n, ∀ l ∈ s.subchain, l.length ≠ n
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<VAR>heq : b = a<GOAL>(l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<VAR>heq : b = a<GOAL>(l₂.erase a).diff l₁ <+ (l₂.erase a).diff l₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<VAR>heq : ¬b = a<GOAL>(l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<VAR>heq : ¬b = a<GOAL>((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<VAR>heq : ¬b = a<VAR>h' : (b :: l₁).erase b <+ l₂.erase b<GOAL>((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<VAR>heq : ¬b = a<VAR>h' : l₁ <+ l₂.erase b<GOAL>((l₂.erase b).erase a).diff (l₁.erase a) <+ (l₂.erase b).diff l₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>L S : TopologicalSpace α<VAR>inst✝¹ : IsLawson α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsOpen s ↔ IsOpen s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup γ<VAR>F : Filter α<VAR>G : Filter β<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Tendsto f F atTop<VAR>hg : Tendsto g G atTop<GOAL>Tendsto (Prod.map f g) (F ×ˢ G) atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup γ<VAR>F : Filter α<VAR>G : Filter β<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Tendsto f F atTop<VAR>hg : Tendsto g G atTop<GOAL>Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hm : AEStronglyMeasurable X ℙ<VAR>hX : ¬Memℒp X 2 ℙ<GOAL>variance X ℙ ≤ ∫ (a : Ω), (X ^ 2) a
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hm : AEStronglyMeasurable X ℙ<VAR>hX : ¬Memℒp X 2 ℙ<GOAL>∫ (a : Ω), (X a - ∫ (x : Ω), X x) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hm : AEStronglyMeasurable X ℙ<VAR>hX : ¬Memℒp X 2 ℙ<GOAL>0 ≤ᶠ[ae ℙ] fun ω => (X ω - ∫ (x : Ω), X x) ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hm : AEStronglyMeasurable X ℙ<VAR>hX : ¬Memℒp X 2 ℙ<GOAL>AEStronglyMeasurable (fun ω => (X ω - ∫ (x : Ω), X x) ^ 2) ℙ
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).ψ n = Polynomial.map (mapRingHom f) (W.ψ n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>normEDS ((mapRingHom (mapRingHom f)) W.ψ₂) (C ((mapRingHom f) W.Ψ₃)) (C ((mapRingHom f) W.preΨ₄)) n = normEDS ((mapRingHom (mapRingHom f)) W.ψ₂) ((mapRingHom (mapRingHom f)) (C W.Ψ₃)) ((mapRingHom (mapRingHom f)) (C W.preΨ₄)) n
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>x : m → 𝕜<VAR>y : n → 𝕜<VAR>inst✝ : Invertible D<VAR>hD : D.IsHermitian<GOAL>star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) = star ((D⁻¹ * Bᴴ) *ᵥ x + y) ᵥ* D ⬝ᵥ ((D⁻¹ * Bᴴ) *ᵥ x + y) + star x ᵥ* (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>x : m → 𝕜<VAR>y : n → 𝕜<VAR>inst✝ : Invertible D<VAR>hD : D.IsHermitian<GOAL>star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) = star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) + (star x ᵥ* A ⬝ᵥ x - star x ᵥ* (B * (D⁻¹ * Bᴴ)) ⬝ᵥ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>g : γ → α<VAR>Cf : ContinuousAt f (⨆ i, g i)<VAR>Mf : Monotone f<VAR>H : BddAbove (range g)<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>g : γ → α<VAR>Cf : ContinuousAt f (⨆ i, g i)<VAR>Mf : Monotone f<VAR>H : BddAbove (range g)<GOAL>sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : DecidableEq p<VAR>inst✝⁶ : DecidableEq q<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Fintype p<VAR>inst✝² : Fintype q<VAR>inst✝¹ : Fintype l<VAR>inst✝ : Invertible 2<GOAL>PD l R * ⅟2 • (PD l R)ᵀ = 1
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : DecidableEq p<VAR>inst✝⁶ : DecidableEq q<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Fintype p<VAR>inst✝² : Fintype q<VAR>inst✝¹ : Fintype l<VAR>inst✝ : Invertible 2<GOAL>fromBlocks (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • 1ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • 1ᵀ) = 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂μ, μ.densityToFinite x < ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>∀ᵐ (x : α) ∂μ.restrict s, μ.densityToFinite x < ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>∀ᵐ (x : α) ∂μ.toFinite.restrict s, μ.densityToFinite x < ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>∫⁻ (x : α) in s, μ.densityToFinite x ∂μ.toFinite ≠ ⊤
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>μ s ≠ ⊤
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hp0 : 0 ≤ p<VAR>hp1 : p ≤ 1<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ 2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hp0 : 0 ≤ 0<VAR>hp1 : 0 ≤ 1<GOAL>(∫⁻ (a : α), (f + g) a ^ 0 ∂μ) ^ (1 / 0) ≤ 2 ^ (1 / 0 - 1) * ((∫⁻ (a : α), f a ^ 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), g a ^ 0 ∂μ) ^ (1 / 0))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hp0 : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp : 0 < p<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ 2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>b : Basis ι ℝ E<GOAL>parallelepiped ⇑b = {x | ∀ (i : ι), (b.repr x) i ∈ Icc 0 1}