ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<VAR>key : α h = 2<GOAL>h = coroot α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<VAR>key : α h = 2<GOAL>∃ s, s • h = coroot α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<VAR>key : α h = 2<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'<VAR>hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<GOAL>∃ s, s • h = coroot α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<VAR>key : α h = 2<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'<VAR>hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>h_eq : h = ((killingForm K L) e) f • α'<GOAL>∃ s, s • h = coroot α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<VAR>key : α h = 2<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'<VAR>hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>h_eq : h = ((killingForm K L) e) f • α'<GOAL>(2 • (α α')⁻¹ * (((killingForm K L) e) f)⁻¹) • h = coroot α
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>h : ↥H<VAR>ht : IsSl2Triple (↑h) e f<VAR>key : α h = 2<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'<VAR>hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<VAR>h_eq : h = ((killingForm K L) e) f • α'<VAR>hef₀ : ((killingForm K L) e) f ≠ 0<GOAL>(2 • (α α')⁻¹ * (((killingForm K L) e) f)⁻¹) • h = coroot α
<VAR>k m n : ℕ+<GOAL>k.Coprime m → k.Coprime n → k.Coprime (m * n)
<VAR>k m n : ℕ+<GOAL>(↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)
<VAR>k m n : ℕ+<GOAL>(↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime (↑m * ↑n)
<VAR>s : ℂ<GOAL>completedCosZeta₀ 0 s = completedRiemannZeta₀ s
<VAR>Ω : Type u_1<VAR>ι✝ : Type u_2<VAR>β✝¹ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>β✝ : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>ι : Type u_10<VAR>β : ι → Type u_11<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<GOAL>iIndepFun m f μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝³ : Zero Γ<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : MulZeroOneClass R<VAR>inst✝ : Nontrivial R<GOAL>orderTop 1 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : AEStronglyMeasurable f (μ.trim hm)<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : AEStronglyMeasurable f (μ.trim hm)<GOAL>∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasProducts C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type v'<VAR>U : ι → Opens ↑X<GOAL>((Pi.lift fun i => F.map (leSupr U i).op) ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) = (Pi.lift fun i => F.map (leSupr U i).op) ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasProducts C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type v'<VAR>U : ι → Opens ↑X<VAR>x✝ : Discrete (ι × ι)<GOAL>((Pi.lift fun i => F.map (leSupr U i).op) ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫ limit.π (Discrete.functor fun p => F.obj (op (U p.1 ⊓ U p.2))) x✝ = ((Pi.lift fun i => F.map (leSupr U i).op) ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫ limit.π (Discrete.functor fun p => F.obj (op (U p.1 ⊓ U p.2))) x✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasProducts C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type v'<VAR>U : ι → Opens ↑X<VAR>x✝ : Discrete (ι × ι)<GOAL>F.map (leSupr U x✝.as.1).op ≫ F.map ((U x✝.as.1).infLELeft (U x✝.as.2)).op = F.map (leSupr U x✝.as.2).op ≫ F.map ((U x✝.as.1).infLERight (U x✝.as.2)).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasProducts C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type v'<VAR>U : ι → Opens ↑X<VAR>x✝ : Discrete (ι × ι)<GOAL>F.map ((leSupr U x✝.as.1).op ≫ ((U x✝.as.1).infLELeft (U x✝.as.2)).op) = F.map (leSupr U x✝.as.2).op ≫ F.map ((U x✝.as.1).infLERight (U x✝.as.2)).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasProducts C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type v'<VAR>U : ι → Opens ↑X<VAR>x✝ : Discrete (ι × ι)<GOAL>F.map ((leSupr U x✝.as.1).op ≫ ((U x✝.as.1).infLELeft (U x✝.as.2)).op) = F.map ((leSupr U x✝.as.2).op ≫ ((U x✝.as.1).infLERight (U x✝.as.2)).op)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>hp : p ≠ 0<GOAL>{x | p.IsRoot x}.Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M × N →ₗ[R] M<VAR>i : Injective ⇑f<VAR>x y : N<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M × N →ₗ[R] M<VAR>i : Injective ⇑f<VAR>x y : N<VAR>h : Injective ⇑(LinearMap.fst R M N)<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<GOAL>spectralRadius 𝕜 a ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<GOAL>↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))<GOAL>↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))<VAR>nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊<GOAL>↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))<VAR>nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊<VAR>hn : 0 < ↑(n + 1)<GOAL>↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))<VAR>nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊<VAR>hn : 0 < ↑(n + 1)<GOAL>↑‖k‖₊ = (fun x => x ^ (1 / ↑(n + 1))) ↑(‖k‖₊ ^ (n + 1))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))<VAR>nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊<VAR>hn : 0 < ↑(n + 1)<GOAL>↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (fun x => x ^ (1 / ↑(n + 1))) (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>n : ℕ<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))<VAR>nnnorm_pow_le : ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊<VAR>hn : 0 < ↑(n + 1)<GOAL>↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1)) = (↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊) ^ (1 / ↑(n + 1))
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{?u.40441, u_1} C<VAR>inst✝⁶ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁵ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁴ : TotalComplexShape c₂ c₁ c<VAR>inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝² : K.HasTotal c<VAR>inst✝¹ : K.flip.HasTotal c<VAR>inst✝ : DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>c₂.π c₁ c (i₂, i₁) = j
<VAR>α✝ β α : Type u<GOAL>1 < #α ↔ Nontrivial α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Set β₁<VAR>g₂ : Set α₂ → Set β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<GOAL>(f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t)) = f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s ×ˢ g₂ t)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atBot<GOAL>Tendsto (fun x => r * f x) l atTop ↔ r < 0
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>∫ (x : E), f.normed μ x ∂μ = 1
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>(∫ (x : E), ↑f x ∂μ)⁻¹ • ∫ (x : E), ↑f x ∂μ = 1
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<GOAL>IsAlgClosed k'
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<GOAL>∀ (p : k'[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<GOAL>∃ x, eval x p = 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<VAR>hpe : (map e.symm.toRingHom p).degree ≠ 0<GOAL>∃ x, eval x p = 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<VAR>hpe : (map e.symm.toRingHom p).degree ≠ 0<VAR>x : k<VAR>hx : (map (↑e.symm) p).IsRoot x<GOAL>∃ x, eval x p = 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<VAR>hpe : (map e.symm.toRingHom p).degree ≠ 0<VAR>x : k<VAR>hx : (map (↑e.symm) p).IsRoot x<GOAL>eval (e x) p = 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<VAR>hpe : (map e.symm.toRingHom p).degree ≠ 0<VAR>x : k<VAR>hx : eval x (map (↑e.symm) p) = 0<GOAL>eval (e x) p = 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<VAR>hpe : (map e.symm.toRingHom p).degree ≠ 0<VAR>x : k<VAR>hx : eval x (map (↑e.symm) p) = 0<GOAL>e.symm (eval (e x) p) = e.symm 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>hmp : p.Monic<VAR>hp : Irreducible p<VAR>hpe : (map e.symm.toRingHom p).degree ≠ 0<VAR>x : k<VAR>hx : eval x (map (↑e.symm) p) = 0<GOAL>e.symm (eval (e x) p) = eval x (map (↑e.symm) p)
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>k' : Type u<VAR>inst✝¹ : Field k'<VAR>e : k ≃+* k'<VAR>inst✝ : IsAlgClosed k<VAR>p : k'[X]<VAR>x : k<GOAL>e.symm (eval (e x) p) = eval x (map (↑e.symm) p)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hq : q ≠ 0<GOAL>(gcd p q).degree ≤ q.degree
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hq : q ≠ 0<GOAL>(gcd q p).degree ≤ q.degree
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : V<VAR>p : P<GOAL>Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>(1 + n).pred = n
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s : ↥S<GOAL>1 • 1 • 0 = 1 • s • 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : TopologicalSemiring A<VAR>inst✝⁸ : ContinuousStar A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>S : StarSubalgebra R A<VAR>inst✝² : FunLike F (↥S.topologicalClosure) B<VAR>inst✝¹ : AlgHomClass F R (↥S.topologicalClosure) B<VAR>inst✝ : StarAlgHomClass F R (↥S.topologicalClosure) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : ∀ (x : ↥S), φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : TopologicalSemiring A<VAR>inst✝⁸ : ContinuousStar A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>S : StarSubalgebra R A<VAR>inst✝² : FunLike F (↥S.topologicalClosure) B<VAR>inst✝¹ : AlgHomClass F R (↥S.topologicalClosure) B<VAR>inst✝ : StarAlgHomClass F R (↥S.topologicalClosure) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : ∀ (x : ↥S), φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)<VAR>this : ↑φ = ↑ψ<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : TopologicalSemiring A<VAR>inst✝⁸ : ContinuousStar A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>S : StarSubalgebra R A<VAR>inst✝² : FunLike F (↥S.topologicalClosure) B<VAR>inst✝¹ : AlgHomClass F R (↥S.topologicalClosure) B<VAR>inst✝ : StarAlgHomClass F R (↥S.topologicalClosure) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : ∀ (x : ↥S), φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)<VAR>this : ↑φ = ↑ψ<GOAL>⇑↑φ = ⇑ψ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsUpperSet ↑𝒜<VAR>hℬ : IsLowerSet ↑ℬ<GOAL>2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜ᶜ<VAR>hℬ : IsLowerSet ↑ℬ<GOAL>2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜ᶜ<VAR>hℬ : IsLowerSet ↑ℬ<VAR>this : 𝒜ᶜ.card * ℬ.card ≤ 2 ^ Fintype.card α * (𝒜ᶜ ∩ ℬ).card<GOAL>2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
<VAR>cmp✝ : ?m.5873 → ?m.5873 → Ordering<VAR>inst✝¹ : TransCmp cmp✝<VAR>x✝ : Sort ?u.5871<VAR>cmp : x✝ → x✝ → Ordering<VAR>inst✝ : TransCmp cmp<VAR>y z x : x✝<VAR>yz : cmp y z = Ordering.eq<GOAL>cmp x y = cmp x z
<VAR>xl xr : Type u<VAR>x x' : PGame<VAR>h : x ⧏ x'<GOAL>x.insertRight x' ≈ x
<VAR>xl xr : Type u<VAR>x x' : PGame<VAR>h : x ⧏ x'<GOAL>(-x).insertLeft (-x') ≈ -x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : DecidableEq M<VAR>P : A → Prop<VAR>f : M →ₗ[A] M<VAR>hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det<VAR>h1 : P 1<GOAL>P (LinearMap.det f)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : DecidableEq M<VAR>P : A → Prop<VAR>f : M →ₗ[A] M<VAR>hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det<VAR>h1 : P 1<GOAL>P ((if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) f)
<VAR>α : Type u<VAR>inst✝² : Monoid α<VAR>a : α<VAR>inst✝¹ inst✝ : Invertible a<GOAL>inst✝¹ = inst✝
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>↑m = lift.{u, v} x ↔ ↑m = x
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), f a * g a ^ (p - 1) ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0<GOAL>(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)