ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>q : α → Prop<GOAL>(∀ (i : ι), p i → ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivAt f f' x<VAR>hg : HasDerivAt g g' x<VAR>h : 0 < f x<GOAL>HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' Set.univ x<VAR>hg : HasDerivWithinAt g g' Set.univ x<VAR>h : 0 < f x<GOAL>HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>m_pos : 0 < ↑m<VAR>h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts<VAR>hs : s ∈ 𝒜<GOAL>↑(𝒜.sup id).card ≤ ↑𝒜.card * ↑s.card * ((↑m + 1) / ↑m)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>m_pos : 0 < ↑m<VAR>h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts<VAR>hs : s ∈ 𝒜<GOAL>↑(𝒜.biUnion id).card * ↑m ≤ ↑𝒜.card * (↑m + 1) * ↑s.card
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>m_pos : 0 < ↑m<VAR>h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts<VAR>hs : s ∈ 𝒜<GOAL>↑(𝒜.biUnion id).card ≤ ↑𝒜.card * (↑m + 1)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>m_pos : 0 < ↑m<VAR>h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts<VAR>hs : s ∈ 𝒜<GOAL>↑m ≤ ↑s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>b ∈ Ι a c → c ∈ Ι a b → b = c
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.65549, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Y' : C<VAR>f : X ⟶ Y'<VAR>s : Y ⟶ Y'<VAR>hs : W s<GOAL>(Q W).map f ≫ Qinv s hs = homMk (mk f s hs)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.65549, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Y' : C<VAR>f : X ⟶ Y'<VAR>s : Y ⟶ Y'<VAR>hs : W s<GOAL>homMk (ofHom W f) ≫ homMk (ofInv s hs) = homMk (mk f s hs)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.65549, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Y' : C<VAR>f : X ⟶ Y'<VAR>s : Y ⟶ Y'<VAR>hs : W s<GOAL>homMk ((ofHom W f).comp₀ (ofInv s hs) (ofHom W (𝟙 (ofHom W f).Y'))) = homMk (mk f s hs)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>H : SimpleGraph V<VAR>s s₁ s₂ : Set (Sym2 V)<GOAL>G.deleteEdges s = G ↔ Disjoint G.edgeSet s
<VAR>p : ℕ<GOAL>Nat.rec (unpair p).1 (fun y IH => IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>a : ℝ<GOAL>HasSum (fun n => a / 2 / 2 ^ n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>a : ℝ<GOAL>(fun n => a / 2 / 2 ^ n) = fun i => a / 2 * (1 / 2) ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>a : ℝ<GOAL>a = a / 2 * (1 - 1 / 2)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<GOAL>↑P.parts.offDiag.card ≤ 1 * ↑P.parts.card ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<GOAL>↑(P.parts.card * P.parts.card - P.parts.card) ≤ ↑P.parts.card ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<GOAL>P.parts.card * P.parts.card - P.parts.card ≤ P.parts.card * P.parts.card
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>inst✝² : Mul α<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Unique ι<VAR>a b : n → α<VAR>x✝ : n<GOAL>(col ι a * row ι b).diag x✝ = (a * b) x✝
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f g φ ψ : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) = -ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>f g φ ψ : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<GOAL>ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) = ShortComplex.homologyMap (-(shortComplexFunctor C c i).map φ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : Surjective m<GOAL>Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>s✝ t : Set ι<VAR>f✝ g✝ : ι → M₀<VAR>i : ι<VAR>s : Set ι<VAR>f g : ι → M₀<GOAL>(s.indicator fun i => f i * g i) = fun i => s.indicator f i * s.indicator g i
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>s✝ t : Set ι<VAR>f✝ g✝ : ι → M₀<VAR>i : ι<VAR>s : Set ι<VAR>f g : ι → M₀<VAR>x✝ : ι<GOAL>s.indicator (fun i => f i * g i) x✝ = s.indicator f x✝ * s.indicator g x✝
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroClass M₀<VAR>s✝ t : Set ι<VAR>f✝ g✝ : ι → M₀<VAR>i : ι<VAR>s : Set ι<VAR>f g : ι → M₀<VAR>x✝ : ι<VAR>h✝ : x✝ ∉ s<GOAL>0 = 0 * 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<GOAL>eval x p = p.sum fun e a => a * x ^ e
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<GOAL>(p.sum fun e a => (RingHom.id R) a * x ^ e) = p.sum fun e a => a * x ^ e
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i : ι<VAR>x : ↑((forget₂ C Ab).obj (K.X i))<VAR>hx : ((forget₂ C Ab).map (K.d i (c.next i))) x = 0<GOAL>((forget₂ C Ab).map (K.iCycles i)) (K.cyclesMk x (c.next i) ⋯ hx) = x
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : RegularSpace X✝<VAR>x : X✝<VAR>s : Set X✝<VAR>X : Type u_3<VAR>T : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ T, RegularSpace X<VAR>x✝ : TopologicalSpace X := sInf T<GOAL>RegularSpace X
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : RegularSpace X✝<VAR>x : X✝<VAR>s : Set X✝<VAR>X : Type u_3<VAR>T : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ T, RegularSpace X<VAR>x✝ : TopologicalSpace X := sInf T<VAR>this : ∀ (a : X), (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If => ⋂ i, If.snd i<GOAL>RegularSpace X
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : RegularSpace X✝<VAR>x : X✝<VAR>s : Set X✝<VAR>X : Type u_3<VAR>T : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ T, RegularSpace X<VAR>x✝ : TopologicalSpace X := sInf T<VAR>this : ∀ (a : X), (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If => ⋂ i, If.snd i<VAR>a : X<VAR>If : (I : Set ↑T) × (↑I → Set X)<VAR>hIf : If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)<VAR>i : ↑If.fst<GOAL>IsClosed (If.snd i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<GOAL>𝓝[univ] a = 𝓝 a
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S : Set (Submonoid M)<VAR>s : Submonoid M<VAR>hs : s ∈ S<GOAL>∀ {x : M}, x ∈ s → x ∈ sSup S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S : Set (Submonoid M)<VAR>s : Submonoid M<VAR>hs : s ∈ S<GOAL>s ≤ sSup S
<VAR>R : Type u_1<VAR>n✝ x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n
<VAR>R : Type u_1<VAR>n✝ x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑(padicValNat p (x ^ n - y ^ n)) = ↑(padicValNat p (x - y)) + ↑(padicValNat p n)
<VAR>R : Type u_1<VAR>n✝ x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
<VAR>R : Type u_1<VAR>n✝ x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>0 < n
<VAR>R : Type u_1<VAR>n✝ x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>0 < x - y
<VAR>R : Type u_1<VAR>n✝ x y p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp1 : Odd p<VAR>hyx : y < x<VAR>hxy : p ∣ x - y<VAR>hx : ¬p ∣ x<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>0 < x ^ n - y ^ n
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntervalIntegrable f μ b₁ b₂<VAR>ha : a ∈ [[b₁, b₂]]<VAR>x✝¹ : ℝ<VAR>x✝ : x✝¹ ∈ [[b₁, b₂]]<GOAL>ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) [[b₁, b₂]] x✝¹
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntervalIntegrable f μ b₁ b₂<VAR>ha : a ∈ [[b₁, b₂]]<VAR>x✝¹ : ℝ<VAR>x✝ : x✝¹ ∈ [[b₁, b₂]]<GOAL>IntervalIntegrable f μ (min a (b₁ ⊓ b₂)) (max a (b₁ ⊔ b₂))
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : IntervalIntegrable f μ b₁ b₂<VAR>ha : a ∈ [[b₁, b₂]]<VAR>x✝¹ : ℝ<VAR>x✝ : x✝¹ ∈ [[b₁, b₂]]<GOAL>IntervalIntegrable f μ (b₁ ⊓ b₂) (b₁ ⊔ b₂)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>a : Ordinal.{u}<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<GOAL>lift.{u, u} #ι < c
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>P X Y Z : C<VAR>f : P ⟶ X<VAR>g : P ⟶ Y<VAR>inst✝² : HasBinaryProduct X Y<VAR>inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)<VAR>inst✝ : PreservesLimit (pair X Y) G<GOAL>(iso G X Y).inv ≫ G.map prod.fst = prod.fst
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>P X Y Z : C<VAR>f : P ⟶ X<VAR>g : P ⟶ Y<VAR>inst✝² : HasBinaryProduct X Y<VAR>inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)<VAR>inst✝ : PreservesLimit (pair X Y) G<GOAL>𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Mul A<VAR>inst✝² : SMulWithZero R A<VAR>inst✝¹ : StarAddMonoid R<VAR>inst✝ : Star A<VAR>a : A<GOAL>IsSelfAdjoint ↑a ↔ IsSelfAdjoint a
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : z ≤ 0<GOAL>x ^ z ≤ 1
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : z ≤ 0<GOAL>1 = x ^ 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<VAR>Z : D<VAR>g g' : G.obj X ⟶ Z<GOAL>α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>p.degree = ↑n ↔ p.natDegree = n
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>degree 0 = ↑n ↔ natDegree 0 = n
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : p ≠ 0<GOAL>p.degree = ↑n ↔ p.natDegree = n
<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>ν μ : Measure α<VAR>f : α → E<VAR>hf : StronglyMeasurable f<VAR>a : α<GOAL>∫ (a : α) in {a}, f a ∂μ = (μ {a}).toReal • f a
<VAR>K : Type u_1<VAR>p : ℕ<VAR>inst✝² : Field K<VAR>inst✝¹ : ExpChar K p<VAR>inst✝ : PerfectRing K p<VAR>hp : Nat.Prime p<VAR>hchar✝ : CharP K p<VAR>f✝ : K[X]<VAR>hf : Irreducible f✝<GOAL>f✝.Separable
<VAR>K : Type u_1<VAR>p : ℕ<VAR>inst✝² : Field K<VAR>inst✝¹ : ExpChar K p<VAR>inst✝ : PerfectRing K p<VAR>hp : Nat.Prime p<VAR>hchar✝ : CharP K p<VAR>f✝ : K[X]<VAR>hf : Irreducible f✝<VAR>h : f✝.Separable<GOAL>f✝.Separable
<VAR>K : Type u_1<VAR>p : ℕ<VAR>inst✝² : Field K<VAR>inst✝¹ : ExpChar K p<VAR>inst✝ : PerfectRing K p<VAR>hp : Nat.Prime p<VAR>hchar✝ : CharP K p<VAR>g : K[X]<VAR>hf : Irreducible ((expand K p) g)<GOAL>((expand K p) g).Separable
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝¹ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ↪ β<VAR>inst✝ : Finite β<GOAL>A.Definable L ((fun g => g ∘ ⇑f) '' s)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<VAR>hn : n < (pmap f l h).length<GOAL>(pmap f l h).get ⟨n, hn⟩ = f (l.get ⟨n, ⋯⟩) ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<VAR>hn : n < (pmap f l h).length<GOAL>(pmap f l h)[n] = f l[n] ⋯
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ : L → R<VAR>m : M<GOAL>m ∈ weightSpace M χ ↔ ∀ (x : L), ∃ k, (((toEnd R L M) x - χ x • 1) ^ k) m = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L✝ L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>L : G ≃L[𝕜] G'<VAR>f : E → F →L[𝕜] G<VAR>x : E<GOAL>fderiv 𝕜 (fun x => (↑L).comp (f x)) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<VAR>s : σ<GOAL>X s ≠ 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<VAR>s : σ<GOAL>∃ d, coeff d (X s) ≠ 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<VAR>s : σ<GOAL>coeff (Finsupp.single s 1) (X s) ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : R[X]<GOAL>(↑f * ↑g).derivativeFun = ↑f * ↑(derivative g) + ↑g * ↑(derivative f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LE β<VAR>t c : Lex (α × β)<VAR>h : t ≤ c<GOAL>(ofLex t).1 ≤ (ofLex c).1
<VAR>α : Sort u_2<VAR>inst✝ : DecidableEq α<VAR>β : Sort u_1<VAR>i j : α<VAR>f : α → β<GOAL>f ∘ ⇑(swap i j) = update (update f j (f i)) i (f j)
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L (a + b + c), L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ = ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a + L b + L c, L (a * a) + L (a * b) + L (a * c) + (L (b * a) + L (b * b) + L (b * c)) + (L (c * a) + L (c * b) + L (c * c))⁆ = ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a + L b + L c, L (a * a) + L (a * b) + L (a * c) + (L (a * b) + L (b * b) + L (b * c)) + (L (a * c) + L (b * c) + L (c * c))⁆ = ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (a * c) + 2 • L (b * c)⁆
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a + L b + L c, L (a * a) + L (a * b) + L (a * c) + (L (a * b) + L (b * b) + L (b * c)) + (L (a * c) + L (b * c) + L (c * c))⁆ = ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + (L (a * b) + L (a * b)) + (L (a * c) + L (a * c)) + (L (b * c) + L (b * c))⁆
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (a * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L c, L (a * a)⁆ + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L c, L (a * b)⁆) + (⁅L a, L (a * c)⁆ + ⁅L b, L (a * c)⁆ + ⁅L c, L (a * c)⁆) + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L c, L (a * b)⁆ + (⁅L a, L (b * b)⁆ + ⁅L b, L (b * b)⁆ + ⁅L c, L (b * b)⁆) + (⁅L a, L (b * c)⁆ + ⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (⁅L a, L (a * c)⁆ + ⁅L b, L (a * c)⁆ + ⁅L c, L (a * c)⁆ + (⁅L a, L (b * c)⁆ + ⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆) + (⁅L a, L (c * c)⁆ + ⁅L b, L (c * c)⁆ + ⁅L c, L (c * c)⁆)) = ⁅L a, L (a * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L c, L (a * a)⁆ + (⁅L a, L (b * b)⁆ + ⁅L b, L (b * b)⁆ + ⁅L c, L (b * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L b, L (c * c)⁆ + ⁅L c, L (c * c)⁆) + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L c, L (a * b)⁆ + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L c, L (a * b)⁆)) + (⁅L a, L (a * c)⁆ + ⁅L b, L (a * c)⁆ + ⁅L c, L (a * c)⁆ + (⁅L a, L (a * c)⁆ + ⁅L b, L (a * c)⁆ + ⁅L c, L (a * c)⁆)) + (⁅L a, L (b * c)⁆ + ⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆ + (⁅L a, L (b * c)⁆ + ⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆))
<VAR>m n✝ n : ℤ<GOAL>Even (n * (n - 1))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a b : R<VAR>η : Type u_9<VAR>inst✝ : Nonempty η<VAR>s : η → Set A<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a b : R<VAR>η : Type u_9<VAR>inst✝ : Nonempty η<VAR>s : η → Set A<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), AlgebraicIndependent R Subtype.val<VAR>t : Set A<VAR>ht : t ⊆ ⋃ i, s i<VAR>ft : t.Finite<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a b : R<VAR>η : Type u_9<VAR>inst✝ : Nonempty η<VAR>s : η → Set A<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), AlgebraicIndependent R Subtype.val<VAR>t : Set A<VAR>ht : t ⊆ ⋃ i, s i<VAR>ft : t.Finite<VAR>I : Set η<VAR>fi : I.Finite<VAR>hI : t ⊆ ⋃ i ∈ I, s i<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a b : R<VAR>η : Type u_9<VAR>inst✝ : Nonempty η<VAR>s : η → Set A<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), AlgebraicIndependent R Subtype.val<VAR>t : Set A<VAR>ht : t ⊆ ⋃ i, s i<VAR>ft : t.Finite<VAR>I : Set η<VAR>fi : I.Finite<VAR>hI : t ⊆ ⋃ i ∈ I, s i<VAR>i : η<VAR>hi : ∀ i_1 ∈ fi.toFinset, s i_1 ⊆ s i<GOAL>AlgebraicIndependent R Subtype.val
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : FaithfulSMul G α<VAR>inst✝ : FaithfulSMul M α<VAR>m : M<GOAL>fixedBy α m = Set.univ ↔ m = 1
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : FaithfulSMul G α<VAR>inst✝ : FaithfulSMul M α<VAR>m : M<GOAL>(∀ (x : α), x ∈ fixedBy α m) ↔ (fun x => m • x) = fun x => 1 • x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ (p q : ℝ≥0), p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0<GOAL>AEMeasurable f μ