ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id ω)) μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x y : α<VAR>F : Set α<VAR>h : y ∈ connectedComponentIn F x<GOAL>connectedComponentIn F x = connectedComponentIn F y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x y : α<VAR>F : Set α<VAR>h : y ∈ connectedComponentIn F x<VAR>hx : x ∈ F<GOAL>connectedComponentIn F x = connectedComponentIn F y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x y : α<VAR>F : Set α<VAR>hx : x ∈ F<VAR>h : y ∈ Subtype.val '' connectedComponent ⟨x, hx⟩<GOAL>Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hx : x ∈ F<VAR>y : α<VAR>hy : y ∈ F<VAR>h2y : ⟨y, hy⟩ ∈ connectedComponent ⟨x, hx⟩<GOAL>Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F ↑⟨y, hy⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>s : Finset α<GOAL>(↑s).ncard = s.card
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<GOAL>mulRothNumber A = mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<GOAL>mulRothNumber A ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : s ⊆ A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<GOAL>mulRothNumber A ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<GOAL>mulRothNumber A ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<VAR>hfs : Set.InjOn f ↑s<GOAL>mulRothNumber A ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<VAR>hfs : Set.InjOn f ↑s<VAR>this : ThreeGPFree (f '' ↑s)<GOAL>mulRothNumber A ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<VAR>hfs : Set.InjOn f ↑s<VAR>this : ThreeGPFree ↑(image f s)<GOAL>mulRothNumber A ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<VAR>hfs : Set.InjOn f ↑s<VAR>this : ThreeGPFree ↑(image f s)<GOAL>(image f s).card ≤ mulRothNumber B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<VAR>hfs : Set.InjOn f ↑s<VAR>this : ThreeGPFree ↑(image f s)<GOAL>image f s ⊆ B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq β<VAR>A : Finset α<VAR>B : Finset β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 (↑A) (↑B) f<VAR>s : Finset α<VAR>hsA : ↑s ⊆ ↑A<VAR>hcard : s.card = mulRothNumber A<VAR>hs : ThreeGPFree ↑s<VAR>hfs : Set.InjOn f ↑s<VAR>this : ThreeGPFree ↑(image f s)<GOAL>f '' ↑s ⊆ ↑B
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>s : AList β<GOAL>a' ∈ replace a b s ↔ a' ∈ s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>inst✝ : S.HasHomology<GOAL>IsIso S.homologyπ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>inst✝ : S.HasHomology<VAR>this : IsIso S.leftHomologyπ<GOAL>IsIso S.homologyπ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter γ<GOAL>map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{?u.64473, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Mono S.f<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<GOAL>cyclesMap S.f i ≫ cyclesMap S.g i = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Mono S.f<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<VAR>this : Mono (S.map (eval C c i)).f<GOAL>(ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Mono S.f<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<VAR>this : Mono (S.map (eval C c i)).f<VAR>hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)<GOAL>(ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Mono S.f<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<VAR>this : Mono (S.map (eval C c i)).f<VAR>hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)<GOAL>IsLimit (KernelFork.ofι (ShortComplex.mk (cyclesMap S.f i) (cyclesMap S.g i) ⋯).f ⋯)
<VAR>m n✝ n : ℕ<GOAL>Nontrivial (ZMod n) ↔ n ≠ 1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<GOAL>HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥↑I → I = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<GOAL>(∀ (I : LieIdeal R L), IsSolvable R ↥↑I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥↑I → I = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R (Dual R N)<GOAL>(map e.flip.symm p).dualAnnihilator = map e p.dualCoannihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R (Dual R N)<VAR>this : IsReflexive R N<GOAL>(map e.flip.symm p).dualAnnihilator = map e p.dualCoannihilator
<VAR>x y : EReal<VAR>h1 : x ≠ ⊥ ∨ y ≠ ⊤<VAR>h2 : x ≠ ⊤ ∨ y ≠ ⊥<GOAL>-(x + y) = -x - y
<VAR>a✝¹ a✝ : ℝ<VAR>h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤<VAR>h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥<GOAL>-(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝
<VAR>α : Type u_1<VAR>inst✝² : OrderedRing α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<GOAL>Monotone fun n => Icc (-↑n) ↑n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>powersetCard (n + 1) (a ::ₘ ⟦l⟧) = powersetCard (n + 1) ⟦l⟧ + map (cons a) (powersetCard n ⟦l⟧)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<GOAL>dist (next^[n] f₁) (next^[n] f₂) ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>(↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this : |↑t - ↑v.t₀| ≤ v.tDist<GOAL>(↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂ ≤ (↑v.L * v.tDist) ^ n / ↑n ! * dist f₁ f₂
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p (m + n)).symm x) = (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hμν : ν ≪ μ<GOAL>essSup f ν ≤ essSup f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hμν : ν ≪ μ<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) (ae ν) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hμν : ν ≪ μ<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : f x ≤ x + ↑m<VAR>n : ℕ<GOAL>(⇑f)^[n] x ≤ x + ↑n * ↑m
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F : ℕᵒᵖ ⥤ Type u<VAR>c : Cone F<VAR>hc✝ : IsLimit c<VAR>hF✝ : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>hc : IsLimit c<VAR>hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)<VAR>this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)<GOAL>Function.Surjective (i.hom ≫ (limitCone F).π.app (Opposite.op 0))
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F : ℕᵒᵖ ⥤ Type u<VAR>c : Cone F<VAR>hc✝ : IsLimit c<VAR>hF✝ : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>hc : IsLimit c<VAR>hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)<VAR>this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)<GOAL>Function.Surjective ((limitCone F).π.app (Opposite.op 0))
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F : ℕᵒᵖ ⥤ Type u<VAR>c : Cone F<VAR>hc✝ : IsLimit c<VAR>hF✝ : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>hc : IsLimit c<VAR>hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)<VAR>this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)<GOAL>Function.Surjective i.hom
<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]<GOAL>X.natSepDegree = 1
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasStrictDerivAt c c' x<VAR>hu : HasStrictDerivAt u u' x<GOAL>HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G✝ : Type u_1<VAR>inst✝³ : NormedAddCommGroup G✝<VAR>inst✝² : NormedSpace 𝕜 G✝<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>G : Type u_2<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasStrictDerivAt c c' x<VAR>hu : HasStrictDerivAt u u' x<VAR>this : HasStrictDerivAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) x<GOAL>HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α ≃o β<VAR>s : Set α<VAR>x : α<GOAL>IsLUB (⇑f '' s) (f x) ↔ IsLUB s x
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<GOAL>Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<GOAL>Tendsto (fun a => ∑' (a_1 : { x // x ∉ a }), ↑(f ↑a_1)) atTop (𝓝 0)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>x y : R<GOAL>IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>x y : R<GOAL>(∃ a b, y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<GOAL>condexpL1 hm μ (c • f) = c • condexpL1 hm μ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<GOAL>∀ (c : 𝕜) (s : Set α) (x : F'), (condexpInd F' hm μ s) (c • x) = c • (condexpInd F' hm μ s) x
<VAR>θ : ℂ<GOAL>tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * ↑π / 2 ≠ θ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<GOAL>IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) s ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ⊤
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a b : R<VAR>h : IsCoprime a b<VAR>h' : a ^ 2 + b ^ 2 = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a b : R<VAR>h : IsCoprime a b<VAR>h' : a ^ 2 + b ^ 2 = 0<VAR>ha : a ^ 2 = 0<VAR>hb : b ^ 2 = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>b : R<VAR>hb : b ^ 2 = 0<VAR>h : IsCoprime 0 b<VAR>h' : 0 ^ 2 + b ^ 2 = 0<VAR>ha : 0 ^ 2 = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>ha hb : 0 ^ 2 = 0<VAR>h : IsCoprime 0 0<VAR>h' : 0 ^ 2 + 0 ^ 2 = 0<GOAL>False
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<GOAL>0 = 1 ↔ n = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>x : Filter α<VAR>y₁ y₂ : Filter β<GOAL>Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>Nat.card α = 0 ↔ IsEmpty α
<VAR>L : Language<VAR>L' : Language<GOAL>Language.empty.card = 0
<VAR>n : ℕ+<GOAL>↑(PrimeMultiset.ofNatList (↑n).primeFactorsList ⋯).prod = ↑n
<VAR>n : ℕ+<GOAL>(↑n).primeFactorsList.prod = ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : IsOpen s<GOAL>{x | gauge s x < 1} = s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : IsOpen s<GOAL>s ⊆ {x | gauge s x < 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₀ : 0 ∈ s<VAR>hs₂ : IsOpen s<GOAL>s = interior s
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>i j a : α<GOAL>(swap i j) ((swap i j) a) = a
<VAR>x y : ℝ<VAR>h : 0 < y<GOAL>√x = y ↔ y * y = x
<GOAL>Differentiable ℂ fun s => s.Gammaℝ⁻¹
<GOAL>Differentiable ℂ fun s => (↑π ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
<VAR>s : ℂ<GOAL>DifferentiableAt ℂ (fun s => ↑π ^ (-s / 2)) s
<GOAL>Differentiable ℂ fun s => (Gamma (s / 2))⁻¹
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>p q : MvPolynomial σ R<VAR>h : ∀ (x : σ → R), (eval x) p = (eval x) q<GOAL>p = q
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>p q : MvPolynomial σ R<VAR>h : ∀ (x : σ → R), (eval x) p = (eval x) q<GOAL>∀ (p : MvPolynomial σ R), (∀ (x : σ → R), (eval x) p = 0) → p = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>p : MvPolynomial σ R<VAR>h : ∀ (x : σ → R), (eval x) p = 0<GOAL>p = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>n : ℕ<VAR>f : Fin n → σ<VAR>hf : Function.Injective f<VAR>p : MvPolynomial (Fin n) R<VAR>h : ∀ (x : σ → R), (eval x) ((rename f) p) = 0<GOAL>(rename f) p = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>n : ℕ<VAR>f : Fin n → σ<VAR>hf : Function.Injective f<VAR>p : MvPolynomial (Fin n) R<VAR>h : ∀ (x : σ → R), (eval x) ((rename f) p) = 0<GOAL>p = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>n : ℕ<VAR>f : Fin n → σ<VAR>hf : Function.Injective f<VAR>p : MvPolynomial (Fin n) R<VAR>h : ∀ (x : σ → R), (eval x) ((rename f) p) = 0<GOAL>∀ (x : Fin n → R), (eval x) p = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>n : ℕ<VAR>f : Fin n → σ<VAR>hf : Function.Injective f<VAR>p : MvPolynomial (Fin n) R<VAR>h : ∀ (x : σ → R), (eval x) ((rename f) p) = 0<VAR>x : Fin n → R<GOAL>(eval x) p = 0
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>S.a + ↑η * S.b = S.a + S.b + λ * S.b
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>S.a + hζ.toInteger * S.b = S.a + S.b + λ * S.b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<GOAL>∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>r : Set α<VAR>hrs : r ⊆ ↑s<VAR>hr : Set.BijOn P.part r ↑P.parts<GOAL>∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>r : Finset α<VAR>hrs : ↑r ⊆ ↑s<VAR>hr : Set.BijOn P.part ↑r ↑P.parts<GOAL>∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d✝ k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>d : ℕ<VAR>x y : Fin n → ℕ<VAR>h : x ≤ y<GOAL>∑ i : Fin n, x i * d ^ ↑i ≤ ∑ i : Fin n, y i * d ^ ↑i
<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<GOAL>selfZPow x B 0 = 1
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f g : (a : α) → β a<VAR>a : α<VAR>b : β a<GOAL>f = update f a b ↔ f a = b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>sInf {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = a
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>sInf {c | ∀ a' < a, a' ⨳ 1 < c} = a
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>{c | ∀ a' < a, a' ⨳ 1 < c} = Set.Ici a