ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α →ₛ E<VAR>hfi : Integrable (↑f) μ<GOAL>integral μ f = ∫ (x : α), ↑f x ∂μ
<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>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α →ₛ E<VAR>hfi : Integrable (↑f) μ<GOAL>integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (Lp.simpleFunc.toLp f ⋯))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>I : Ideal R<VAR>a b : R<VAR>S ι✝ : Type v<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>ι' : Type w<VAR>x : ι → R<VAR>hi : ∀ (i : ι), x i ∈ I<VAR>f : (ι → R) →ₗ[R] ι' → R<VAR>i : ι'<GOAL>f x i ∈ I
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.succ<VAR>i✝ : Fin n✝<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>m n : ℕ<VAR>α : Type u_1<VAR>xs : Fin m → α<VAR>ys : Fin n → α<VAR>i : Fin (m + n)<GOAL>append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (cast ⋯ i)
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.succ<VAR>i✝ : Fin n✝<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>m n : ℕ<VAR>α : Type u_1<VAR>xs : Fin m → α<VAR>ys : Fin n → α<VAR>i : Fin (m + n)<GOAL>append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (cast ⋯ i.rev)
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.succ<VAR>i✝ : Fin n✝<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>m n : ℕ<VAR>α : Type u_1<VAR>xs : Fin m → α<VAR>ys : Fin n → α<VAR>i : Fin (m + n)<GOAL>append xs ys i = append (ys ∘ rev) (xs ∘ rev) (cast ⋯ i.rev)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>(insert a b s).keys = a :: s.keys.erase a
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>I : Nonempty ι<VAR>s : Set ((i : ι) → β i)<VAR>hs : s ∈ Function.Embedding.sets β<VAR>ms : ∀ a ∈ Function.Embedding.sets β, s ⊆ a → a = s<VAR>h : ¬∃ i, ∀ (y : β i), ∃ x ∈ s, x i = y<GOAL>∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsLUB s a<GOAL>b < a ↔ ∃ c ∈ s, b < c
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<GOAL>(∅.weightedVSub p) w = 0
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
<VAR>a : UnitAddCircle<VAR>this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)<GOAL>Tendsto (fun s => (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
<VAR>a : UnitAddCircle<VAR>this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)<GOAL>(fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) =ᶠ[𝓝[≠] 1] fun s => (s - 1) * hurwitzZetaEven a s
<VAR>a : UnitAddCircle<VAR>this : Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>(s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>T : TopologicalSpace α<VAR>F : Realizer α<GOAL>TopologicalSpace.IsTopologicalBasis (range F.F.f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>T : TopologicalSpace α<VAR>F : Realizer α<VAR>this : TopologicalSpace.IsTopologicalBasis (range F.F.f)<GOAL>TopologicalSpace.IsTopologicalBasis (range F.F.f)
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝ : CommRing R<VAR>a b c : lib R X<VAR>h : Rel R X a b<GOAL>Rel R X (a - c) (b - c)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<GOAL>(mkMetric fun x => ⊤) = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<GOAL>(mkMetric fun x => ⊤).toOuterMeasure = ⊤.toOuterMeasure
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => f ≫ x<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => f ≫ x<VAR>g : Y ⟶ X<VAR>hg : f ≫ g = 𝟙 X<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (T : C), Function.Bijective fun x => f ≫ x<VAR>g : Y ⟶ X<VAR>hg : f ≫ g = 𝟙 X<GOAL>(fun x => f ≫ x) (g ≫ f) = (fun x => f ≫ x) (𝟙 Y)
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<GOAL>a.natAbs = b.natAbs ↔ a * a = b * b
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<GOAL>a.natAbs = b.natAbs ↔ ↑a.natAbs = ↑b.natAbs
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝ : CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<GOAL>h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝ : CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<GOAL>(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯) ⟨{ toFun := fun i => Additive.ofMul ⟨(fun x => ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩) ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>W X Y Z : C<GOAL>(α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>l : Line α ι<VAR>v : ι' → α<VAR>x : α<GOAL>(fun x i => ((l.horizontal v).idxFun i).getD x) x = Sum.elim ((fun x i => (l.idxFun i).getD x) x) v
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i✝ : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>l : Line α ι<VAR>v : ι' → α<VAR>x : α<VAR>i : ι ⊕ ι'<GOAL>(fun x i => ((l.horizontal v).idxFun i).getD x) x i = Sum.elim ((fun x i => (l.idxFun i).getD x) x) v i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Ico a b) = Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Ico a b) ⊆ Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>Icc a b ⊆ closure (Ico a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedField 𝕜'<VAR>c c' c₁✝ c₂✝ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>inst✝ : l.NeBot<VAR>c₁ : E''<VAR>c₂ : F''<GOAL>((fun x => c₁) =Θ[l] fun x => c₂) ↔ (c₁ = 0 ↔ c₂ = 0)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : ↥(integralClosure R A)<VAR>p : R[X]<VAR>hpm : p.Monic<VAR>hpx : eval₂ (algebraMap R A) (↑x) p = 0<GOAL>↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<GOAL>2 • v = 0 ↔ v = 0
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<VAR>this : NoZeroSMulDivisors ℕ M<GOAL>2 • v = 0 ↔ v = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>Disjoint N N' ↔ Disjoint ↑N ↑N'
<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>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : IsScalarTower K L F<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : Algebra.IsSeparable K F<VAR>inst✝ : FiniteDimensional K F<VAR>pb : PowerBasis K L<GOAL>∏ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = (∏ σ : L →ₐ[K] E, σ pb.gen) ^ finrank L F
<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>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : IsScalarTower K L F<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : Algebra.IsSeparable K F<VAR>inst✝ : FiniteDimensional K F<VAR>pb : PowerBasis K L<VAR>this : FiniteDimensional L F<GOAL>∏ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = (∏ σ : L →ₐ[K] E, σ pb.gen) ^ finrank L F
<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>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : IsScalarTower K L F<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : Algebra.IsSeparable K F<VAR>inst✝ : FiniteDimensional K F<VAR>pb : PowerBasis K L<VAR>this✝ : FiniteDimensional L F<VAR>this : Algebra.IsSeparable L F<GOAL>∏ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = (∏ σ : L →ₐ[K] E, σ pb.gen) ^ finrank L F
<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>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : IsScalarTower K L F<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : Algebra.IsSeparable K F<VAR>inst✝ : FiniteDimensional K F<VAR>pb : PowerBasis K L<VAR>this✝¹ : FiniteDimensional L F<VAR>this✝ : Algebra.IsSeparable L F<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>∏ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = (∏ σ : L →ₐ[K] E, σ pb.gen) ^ finrank L F
<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>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : IsScalarTower K L F<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : Algebra.IsSeparable K F<VAR>inst✝ : FiniteDimensional K F<VAR>pb : PowerBasis K L<VAR>this✝¹ : FiniteDimensional L F<VAR>this✝ : Algebra.IsSeparable L F<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>∏ a : L →ₐ[K] E, ∏ s : F →ₐ[L] E, ⟨a, s⟩.fst pb.gen = ∏ x : L →ₐ[K] E, x pb.gen ^ finrank L F
<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>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : IsScalarTower K L F<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : Algebra.IsSeparable K F<VAR>inst✝ : FiniteDimensional K F<VAR>pb : PowerBasis K L<VAR>this✝¹ : FiniteDimensional L F<VAR>this✝ : Algebra.IsSeparable L F<VAR>this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb<GOAL>∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen
<VAR>x : ℂ<VAR>n : ℤ<VAR>hlt : -π < ↑n * x.arg<VAR>hle : ↑n * x.arg ≤ π<VAR>y : ℂ<GOAL>x ^ (↑n * y) = (x ^ n) ^ y
<VAR>x : ℂ<VAR>n : ℤ<VAR>hlt : -π < x.arg * ↑n<VAR>hle : x.arg * ↑n ≤ π<VAR>y : ℂ<GOAL>x ^ (↑n * y) = (x ^ n) ^ y
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>A B : SpecialLinearGroup n R<VAR>inst✝ : Nontrivial R<VAR>g : SpecialLinearGroup n R<GOAL>(↑g).det ≠ 0
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>A B : SpecialLinearGroup n R<VAR>inst✝ : Nontrivial R<VAR>g : SpecialLinearGroup n R<GOAL>1 ≠ 0
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsNat e n<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log e
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsNat e n<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log ↑n
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsNat e n<VAR>w : Nat.blt 1 n = true<GOAL>1 < ↑n
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<GOAL>swap x y ∈ closure S ↔ x ∈ orbit (↥(closure S)) y
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<VAR>hf : x ∈ orbit (↥(closure S)) y<GOAL>swap x y ∈ closure S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<VAR>hf : x ∈ orbit (↥(closure S)) y<VAR>h : swap x y ∉ closure S<GOAL>False
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<VAR>hf : x ∈ orbit (↥(closure S)) y<VAR>h : swap x y ∉ closure S<VAR>this : ∃ σ ∈ S, ∃ a ∈ {x | swap x y ∈ closure S}, σ • a ∉ {x | swap x y ∈ closure S}<GOAL>False
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<VAR>hf✝ : x ∈ orbit (↥(closure S)) y<VAR>h : swap x y ∉ closure S<VAR>f : Equiv.Perm α<VAR>hf : f ∈ S<GOAL>f⁻¹ ∈ S
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<VAR>hf : x ∈ orbit (↥(closure S)) y<VAR>h : swap x y ∉ closure S<VAR>z : α<VAR>hz : z ∈ {x | swap x y ∈ closure S}<GOAL>z ∈ orbit (↥(closure S)) x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ f ∈ S, f.IsSwap<VAR>x y : α<VAR>hf : x ∈ orbit (↥(closure S)) y<VAR>h : swap x y ∉ closure S<GOAL>y ∈ {x | swap x y ∈ closure S}
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝³ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>inst✝² : Fintype I<VAR>inst✝¹ : Nonempty I<VAR>inst✝ : DecidableEq I<GOAL>(∃ μ, ∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (IsCoprime on s)
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝³ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>inst✝² : Fintype I<VAR>inst✝¹ : Nonempty I<VAR>inst✝ : DecidableEq I<GOAL>Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i => s ↑i)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>x : F<VAR>hx : x ≠ 0<GOAL>(x • f).natSepDegree = f.natSepDegree
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s : Set α<VAR>hs : SupClosed s<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<GOAL>t.inf' ht id ⊔ u.inf' hu id ∈ infClosure s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s : Set α<VAR>hs : SupClosed s<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<GOAL>((t ×ˢ u).inf' ⋯ fun i => id i.1 ⊔ id i.2) ∈ infClosure s
<VAR>a✝ b✝ : Prop<VAR>α : Sort u_1<VAR>a b : α<VAR>p : Prop<GOAL>p ∧ a = b ↔ p ∧ b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>lsub f = 0 ↔ IsEmpty ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : lsub f = 0<VAR>i : ι<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : lsub f = 0<VAR>i : ι<VAR>this : 0 < lsub f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : lsub f = 0<VAR>i : ι<VAR>this : 0 < 0<GOAL>False
<VAR>α : Type u_1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s t : Finset (ZMod p)<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>min p (s.card + t.card - 1) ≤ (s + t).card
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℝ<VAR>hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x x_1 => x ≤ x_1) x b<GOAL>(fun x => rexp ((f x).arg * (g x).im)) =Θ[l] fun x => 1
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℝ<VAR>hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x x_1 => x ≤ x_1) x b<GOAL>∀ᶠ (x : ℝ) in Filter.map (fun x => |(f x).arg * (g x).im|) l, (fun x x_1 => x ≤ x_1) x (π * b)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℝ<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(g a).im| b<GOAL>∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(f a).arg * (g a).im| (π * b)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℝ<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(g a).im| b<VAR>x : α<VAR>hx : (fun x x_1 => x ≤ x_1) |(g x).im| b<GOAL>(fun x x_1 => x ≤ x_1) |(f x).arg * (g x).im| (π * b)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>b : ℝ<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) |(g a).im| b<VAR>x : α<VAR>hx : (fun x x_1 => x ≤ x_1) |(g x).im| b<GOAL>(fun x x_1 => x ≤ x_1) (|(f x).arg| * |(g x).im|) (π * b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>re ⟪x, x⟫_𝕜 = ‖x‖ ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ<VAR>B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>F✝ : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α✝<VAR>inst✝⁵ : PseudoEMetricSpace β✝<VAR>inst✝⁴ : FunLike F✝ α✝ β✝<VAR>α : Type u_7<VAR>β : Type u_8<VAR>F : Type u_6<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>hxy : dist x y ≠ 0<VAR>hr : dist (f x) (f y) = ↑r * dist x y<GOAL>↑(nndist (f x) (f y)) = ↑(r * nndist x y)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α : Ext X Y n<GOAL>(-α).hom = -α.hom
<VAR>R : Type u_1<VAR>inst✝⁵ : AddCommGroupWithOne R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : Nontrivial R<VAR>m n : ℤ<GOAL>↑n < 0 ↔ n < 0
<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 : α<VAR>m : ℤ<GOAL>toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<GOAL>↑‖c‖₊ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)