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>inst✝² : IsKilling K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α : Weight K (↥H) L<VAR>h : α.IsZero<VAR>x✝ : ↥H<GOAL>(-α) x✝ = 0 x✝
<VAR>n : ℕ<VAR>x a b : ℝ<VAR>m : ℕ<VAR>e₁ : n + 1 = m<VAR>h : |x| ≤ 1<VAR>e : |1 - a| ≤ b - |x| / ↑m * ((↑m + 1) / ↑m)<GOAL>|rexp x - expNear n x a| ≤ |x| ^ n / ↑n.factorial * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>e : α ≃ β<VAR>q : β → Prop<VAR>h : Computable ⇑e.symm<GOAL>q ≤₁ (q ∘ ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>e : α ≃ β<VAR>q : β → Prop<VAR>h : Computable ⇑e.symm<GOAL>q = (q ∘ ⇑e) ∘ ⇑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>e : α ≃ β<VAR>q : β → Prop<VAR>h : Computable ⇑e.symm<VAR>x✝ : β<GOAL>q x✝ = ((q ∘ ⇑e) ∘ ⇑e.symm) x✝
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hba : b ≤ a<VAR>hb : 0 < b<VAR>h : a / b = 0<GOAL>a = a % b
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>‖x‖ ≤ convexBodySumFun x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>(Finset.univ.sup' ⋯ fun w => (normAtPlace w) x) ≤ convexBodySumFun x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : InfinitePlace K<VAR>x✝ : w ∈ Finset.univ<GOAL>(normAtPlace w) x ≤ convexBodySumFun x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : InfinitePlace K<VAR>x✝ : w ∈ Finset.univ<GOAL>(normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x + ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : InfinitePlace K<VAR>x✝ : w ∈ Finset.univ<GOAL>(normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>w : InfinitePlace K<VAR>x✝ : w ∈ Finset.univ<GOAL>0 ≤ ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => x + ↑n
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<GOAL>μ.toSphere univ = ↑(dim E) * μ (ball 0 1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Iic s).card = ∏ i ∈ s.toFinset, (count i s + 1)
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)<GOAL>log (exp ℝ a) = a
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)<GOAL>cfc (fun x => Real.log (Real.exp x)) a = a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>x : X<GOAL>x ∈ range ⇑γ.symm ↔ x ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>x : X<GOAL>(∃ x_1, ∃ (h : x_1 ∈ I), γ.toFun ⟨1 - x_1, ⋯⟩ = x) ↔ ∃ x_1, ∃ (h : x_1 ∈ I), γ.toFun ⟨x_1, h⟩ = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y✝<VAR>a b : X<VAR>γ : Path a b<VAR>x : X<VAR>y : ℝ<VAR>hy : y ∈ I<VAR>hxy : γ.toFun ⟨y, hy⟩ = x<GOAL>1 - (1 - y) = y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Memℒp (s.indicator f) p μ ↔ Memℒp f p (μ.restrict s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : Odd n<GOAL>2 * (n / 2) + 1 = n
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : IsLocalization M S<VAR>R' : Type u_4<VAR>inst✝³ : CommRing R'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Algebra S R'<VAR>inst✝ : IsScalarTower R S R'<VAR>p : S[X]<VAR>x : R'<VAR>hx : (aeval x) p = 0<GOAL>(aeval x) (integerNormalization M p) = 0
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>T : Tape Γ<VAR>i : ℤ<GOAL>(move Dir.right T).nth i = T.nth (i + 1)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>T : Tape Γ<VAR>i : ℤ<GOAL>(move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>p : β → Prop<VAR>f : (b : β) → p b → α<VAR>a : β<VAR>l : List β<VAR>ihl : ∀ (h : ∀ (x : β), x ∈ l → p x), Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l<VAR>h : ∀ (x : β), x ∈ a :: l → p x<VAR>left✝ : p a<VAR>hl : ∀ (b : β), b ∈ l → p b<GOAL>Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>p : β → Prop<VAR>f : (b : β) → p b → α<VAR>a : β<VAR>l : List β<VAR>ihl : ∀ (h : ∀ (x : β), x ∈ l → p x), Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l<VAR>h : ∀ (x : β), x ∈ a :: l → p x<VAR>left✝ : p a<VAR>hl : ∀ (b : β), b ∈ l → p b<GOAL>Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l → ((∀ (a' : α) (x : β) (h_1 : x ∈ l), f x ⋯ = a' → R (f a ⋯) a') ↔ ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>(¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>(IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
<VAR>α : Type u_1<VAR>inst✝¹ : GeneralizedBooleanAlgebra α<VAR>inst✝ : DecidableEq α<VAR>a b✝ c : α<VAR>P : Finpartition a<VAR>b : α<GOAL>(image (fun x => x \ b) P.parts).sup id = a \ b
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<GOAL>h.finpartition.parts.card ≤ r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>l : r < h.finpartition.parts.card<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>l : r < h.finpartition.parts.card<VAR>z : Finset V<VAR>hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>l : r < h.finpartition.parts.card<VAR>z : Finset V<VAR>hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts<VAR>ncf : ¬G.CliqueFree z.card<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>l : r < h.finpartition.parts.card<VAR>z : Finset V<VAR>hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts<VAR>ncf : ¬G.CliqueFree h.finpartition.parts.card<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>h✝ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>hα : Countable α<VAR>x y : α<VAR>h : x ∈ measurableAtom y<GOAL>(fun a => (κ a).condKernel) x = (fun a => (κ a).condKernel) y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>inst✝ : SigmaFinite (μ.trim hm)<GOAL>0 ≤ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>0 ≤ᶠ[ae μ] ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>0 ≤ᶠ[ae μ] AEStronglyMeasurable'.mk (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>0 ≤ᶠ[ae (μ.trim hm)] AEStronglyMeasurable'.mk (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → (μ.trim hm) s_1 < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h) s_1 (μ.trim hm)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → (μ.trim hm) s_1 < ⊤ → 0 ≤ ∫ (x : α) in s_1, AEStronglyMeasurable'.mk (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h x ∂μ.trim hm
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : Field k<VAR>f : R →+* k<GOAL>IsCoprime (map f p) (map f q) ↔ IsCoprime p q
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<GOAL>|∫ (x : ℝ) in a..b, f x ∂μ| ≤ ∫ (x : ℝ) in a..b, |f x| ∂μ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : Linear R D<VAR>F : C ⥤ D<VAR>X Y Z : Free R C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>{ obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f ≫ g) = { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f ≫ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : Linear R D<VAR>F : C ⥤ D<VAR>X Y Z : Free R C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>{ obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (0 ≫ g) = { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map 0 ≫ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : Linear R D<VAR>F : C ⥤ D<VAR>X Y Z : Free R C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>∀ (f g_1 : (X ⟶ Y) →₀ R), { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f ≫ g) = { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map f ≫ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g → { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (g_1 ≫ g) = { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g_1 ≫ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g → { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map ((f + g_1) ≫ g) = { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (f + g_1) ≫ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u<VAR>inst✝² : Category.{v, u} D<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : Linear R D<VAR>F : C ⥤ D<VAR>X Y Z : Free R C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>∀ (a : X ⟶ Y) (b : R), { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single a b ≫ g) = { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map (single a b) ≫ { obj := fun X => F.obj X, map := fun {X Y} f => sum f fun f' r => r • F.map f' }.map g
<VAR>a b : Ordinal.{u_1}<VAR>l : a.IsLimit<VAR>hb : b ≠ 0<GOAL>(a ^ b).IsLimit
<VAR>a b : Ordinal.{u_1}<VAR>l : a.IsLimit<VAR>hb : b ≠ 0<VAR>e : b = 0<GOAL>(a ^ b).IsLimit
<VAR>a : Ordinal.{u_1}<VAR>l : a.IsLimit<VAR>b : Ordinal.{u_1}<VAR>hb : succ b ≠ 0<GOAL>(a ^ succ b).IsLimit
<VAR>a b : Ordinal.{u_1}<VAR>l : a.IsLimit<VAR>hb : b ≠ 0<VAR>l' : b.IsLimit<GOAL>(a ^ b).IsLimit
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : Invertible 2<VAR>p : Fin 2 → P<GOAL>centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : Invertible 2<VAR>p : Fin 2 → P<GOAL>centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
<VAR>n : ℕ<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
<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>i : ι<GOAL>res F U ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := i } = F.map (leSupr U i).op
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>a b c✝ c : α<VAR>h : c * a = b<GOAL>a * c = b
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>a b c✝ c : α<VAR>h : a * c = b<GOAL>a * c = b
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>s t : Cone F<VAR>h : IsLimit t<VAR>f f' g : s ⟶ t<GOAL>g = h.liftConeMorphism s
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>s t : Cone F<VAR>h : IsLimit t<VAR>f f' g : s ⟶ t<GOAL>g.hom = (h.liftConeMorphism s).hom
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<GOAL>Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
<VAR>a b m n p✝ p : ℕ<VAR>pp : Prime p<GOAL>Icc 1 ((factorization 0) p) = Finset.filter (fun i => p ^ i ∣ 0) (Ico 1 0)
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<GOAL>Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<VAR>x : ℕ<GOAL>x ∈ Icc 1 (n.factorization p) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<VAR>x : ℕ<GOAL>1 ≤ x → x ≤ n.factorization p → x < n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Closeds α<GOAL>∃ S, (∀ (k : { x // x ∈ S }), IsIrreducible ↑↑k) ∧ s = S.sup id
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>0 = lift.{v, u} a ↔ 0 = a
<VAR>c : Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>x✝.contains c = true ↔ c ∈ x✝.toString.data
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x y z : L<VAR>hx : x ∈ H.normalizer<VAR>hy : y ∈ Submodule.span R {x} ⊔ H.toSubmodule<VAR>hz : z ∈ Submodule.span R {x} ⊔ H.toSubmodule<GOAL>⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule