ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m n : ℤ<VAR>a b : α<VAR>ha : 1 < a<VAR>hn : 0 < n<GOAL>1 < a ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m : ℤ<VAR>a b : α<VAR>ha : 1 < a<VAR>n : ℕ<VAR>hn : 0 < ↑n<GOAL>1 < a ^ ↑n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m : ℤ<VAR>a b : α<VAR>ha : 1 < a<VAR>n : ℕ<VAR>hn : 0 < ↑n<GOAL>1 < a ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m : ℤ<VAR>a b : α<VAR>ha : 1 < a<VAR>n : ℕ<VAR>hn : 0 < ↑n<GOAL>n ≠ 0
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>i : Fin2 n<VAR>x : α i<VAR>p : Prop<GOAL>ofRepeat (TypeVec.const p α i x) ↔ p
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x y : ℕ<GOAL>x ≤ b ^ y ↔ clog b x ≤ y
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<VAR>ih : ∀ m < x, ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y<VAR>y : ℕ<GOAL>x ≤ b ^ y ↔ clog b x ≤ y
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<VAR>ih : ∀ m < x, ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y<VAR>n✝ : ℕ<GOAL>x ≤ b ^ (n✝ + 1) ↔ clog b x ≤ n✝ + 1
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<VAR>ih : ∀ m < x, ∀ {y : ℕ}, m ≤ b ^ y ↔ clog b m ≤ y<VAR>n✝ : ℕ<VAR>b_pos : 0 < b<GOAL>x ≤ b ^ (n✝ + 1) ↔ clog b x ≤ n✝ + 1
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>⇑(S.transitionMap n) ∘ ⇑(S.proj (n + 1)) = ⇑(S.proj n)
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>⇑(S.transitionMap n) ∘ ⇑(S.proj (n + 1)) = ⇑(S.proj (n + 1) ≫ S.diagram.map (Opposite.op (homOfLE ⋯)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<VAR>hp1_real : 1 ≤ p.toReal<GOAL>eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>hp1 : 1 ≤ p<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<VAR>hp1_real : 1 ≤ p.toReal<GOAL>eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>comap rexp atTop = atTop
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hs : s ⊆ support ↑f<GOAL>↑(extChartAt I c) '' s = closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hs : s ⊆ (extChartAt I c).source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut<GOAL>↑(extChartAt I c) '' s = closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hse : s ⊆ (extChartAt I c).source<VAR>hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut<GOAL>↑(extChartAt I c) '' s = closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hse : s ⊆ (extChartAt I c).source<VAR>hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut<GOAL>↑(extChartAt I c) '' s ⊆ closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>s : Set M<VAR>hse : s ⊆ (extChartAt I c).source<VAR>hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut<GOAL>closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s ⊆ ↑(extChartAt I c) '' s
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>x : G<GOAL>toUnits x ∈ H.units ↔ x ∈ H
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<GOAL>Continuous fun x => sSup (f x '' K)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>hf : Continuous ↿f<VAR>hK : IsCompact ∅<GOAL>Continuous fun x => sSup (f x '' ∅)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<VAR>h0K : K.Nonempty<GOAL>Continuous fun x => sSup (f x '' K)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<VAR>h0K : K.Nonempty<GOAL>∀ (x : γ), ContinuousAt (fun x => sSup (f x '' K)) x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<VAR>h0K : K.Nonempty<VAR>x : γ<GOAL>ContinuousAt (fun x => sSup (f x '' K)) x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<VAR>h0K : K.Nonempty<VAR>x : γ<VAR>y : β<VAR>hyK : y ∈ K<VAR>h2y : sSup ((fun y => f x y) '' K) = f x y<VAR>hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y<GOAL>ContinuousAt (fun x => sSup (f x '' K)) x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<VAR>h0K : K.Nonempty<VAR>x : γ<VAR>y : β<VAR>hyK : y ∈ K<VAR>h2y : sSup ((fun y => f x y) '' K) = f x y<VAR>hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y<GOAL>(∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<VAR>h0K : K.Nonempty<VAR>x : γ<VAR>y : β<VAR>hyK : y ∈ K<VAR>h2y : sSup ((fun y => f x y) '' K) = f x y<VAR>hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y<VAR>this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'<GOAL>(∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝³ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝² : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝¹ : RingHomIsometric σ₂₁<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>e : E ≃SL[σ₁₂] F<GOAL>Subsingleton E ∨ 0 < ‖↑e.symm‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝³ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝² : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝¹ : RingHomIsometric σ₂₁<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>e : E ≃SL[σ₁₂] F<VAR>_i : Subsingleton E<GOAL>Subsingleton E ∨ 0 < ‖↑e.symm‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝³ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝² : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝¹ : RingHomIsometric σ₂₁<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>e : E ≃SL[σ₁₂] F<VAR>_i : Nontrivial E<GOAL>Subsingleton E ∨ 0 < ‖↑e.symm‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hm : IsPeriodicPt f m x<VAR>hn : IsPeriodicPt f n x<GOAL>IsPeriodicPt f (m - n) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hm : IsPeriodicPt f m x<VAR>hn : IsPeriodicPt f n x<VAR>h : n ≤ m<GOAL>IsPeriodicPt f (m - n) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hm : IsPeriodicPt f m x<VAR>hn : IsPeriodicPt f n x<VAR>h : m ≤ n<GOAL>IsPeriodicPt f (m - n) x
<VAR>α : Type u_1<VAR>inst✝¹ : OrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>x : ↑(Icc 0 1)<GOAL>0 ≤ 1 - ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s t : Set α<VAR>h : s ∩ mulSupport f = t ∩ mulSupport f<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<GOAL>W.Equation ![X, Y, 1] ↔ W.toAffine.Equation X Y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<GOAL>![X, Y, 1] 1 ^ 2 * ![X, Y, 1] 2 + W.a₁ * ![X, Y, 1] 0 * ![X, Y, 1] 1 * ![X, Y, 1] 2 + W.a₃ * ![X, Y, 1] 1 * ![X, Y, 1] 2 ^ 2 = ![X, Y, 1] 0 ^ 3 + W.a₂ * ![X, Y, 1] 0 ^ 2 * ![X, Y, 1] 2 + W.a₄ * ![X, Y, 1] 0 * ![X, Y, 1] 2 ^ 2 + W.a₆ * ![X, Y, 1] 2 ^ 3 ↔ Y ^ 2 + W.toAffine.a₁ * X * Y + W.toAffine.a₃ * Y = X ^ 3 + W.toAffine.a₂ * X ^ 2 + W.toAffine.a₄ * X + W.toAffine.a₆
<VAR>p q r : ℕ+<VAR>H : 1 < sumInv {p, q, r}<VAR>S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}<VAR>hS : List.Sorted (fun x x_1 => x ≤ x_1) S<GOAL>(∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨ (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
<VAR>p q r : ℕ+<VAR>H : 1 < sumInv {p, q, r}<VAR>S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}<VAR>hS : List.Sorted (fun x x_1 => x ≤ x_1) S<VAR>hpqr : {p, q, r} = ↑S<GOAL>(∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨ (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
<VAR>p q r : ℕ+<VAR>S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}<VAR>H : 1 < sumInv ↑S<VAR>hS : List.Sorted (fun x x_1 => x ≤ x_1) S<VAR>hpqr : {p, q, r} = ↑S<GOAL>(∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
<VAR>p q r : ℕ+<VAR>S : List ℕ+ := sort (fun x x_1 => x ≤ x_1) {p, q, r}<VAR>H : 1 < sumInv ↑S<VAR>hS : List.Sorted (fun x x_1 => x ≤ x_1) S<VAR>hpqr : {p, q, r} = ↑S<GOAL>S.length = 3
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>hG : G.Colorable n<GOAL>G.chromaticNumber = ↑n ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C
<VAR>p q : Prop<VAR>α : Sort u_1<VAR>s✝ : α → Prop<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>s : Set β<GOAL>(∅ ≠ s) = s.Nonempty
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → E<VAR>x y : k<GOAL>slope (fun t => -f t) x y = -slope f x y
<VAR>s : Finset ℕ<VAR>m n p : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<GOAL>(m / m.gcd n).Coprime n
<VAR>s : Finset ℕ<VAR>m n p : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<VAR>this : (m / m.gcd n).Coprime (m.gcd n)<GOAL>(m / m.gcd n).Coprime n
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>h2 : Even l.length<VAR>b : Bool<GOAL>2 * count b l = l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>n : ℤ<VAR>x : α<GOAL>f (x + (2 * n + 1) • c) = -f x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Mono f<VAR>inst✝ : IsSplitEpi f<GOAL>f ≫ section_ f = 𝟙 X
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this : Encodable ↑d<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this✝ : Encodable ↑d<VAR>this : ∀ (x : ↑d), ∃ g, ‖g‖ ≤ 1 ∧ g ↑x = ↑‖↑x‖<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this : Encodable ↑d<VAR>s : ↑d → E →L[𝕜] 𝕜<VAR>hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this : Encodable ↑d<VAR>s : ↑d → E →L[𝕜] 𝕜<VAR>hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖<VAR>A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this : Encodable ↑d<VAR>s : ↑d → E →L[𝕜] 𝕜<VAR>hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖<VAR>A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0<VAR>hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this : Encodable ↑d<VAR>s : ↑d → E →L[𝕜] 𝕜<VAR>hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖<VAR>A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0<VAR>hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0<VAR>hf' : ∀ᵐ (x : α) ∂μ, ∀ (y : ↑d), (s y) (f x) = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>t : Set E<VAR>f : α → E<VAR>hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0<VAR>h't : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>d : Set E<VAR>d_count : d.Countable<VAR>hd : t ⊆ closure d<VAR>this : Encodable ↑d<VAR>s : ↑d → E →L[𝕜] 𝕜<VAR>hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖<VAR>A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0<VAR>hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0<VAR>hf' : ∀ᵐ (x : α) ∂μ, ∀ (y : ↑d), (s y) (f x) = 0<VAR>x : α<VAR>hx : ∀ (y : ↑d), (s y) (f x) = 0<VAR>h'x : f x ∈ t<GOAL>f x = 0 x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>hx : x.Compatible<VAR>Y₁✝ Y₂✝ Z✝ : C<VAR>g₁✝ : Z✝ ⟶ Y₁✝<VAR>g₂✝ : Z✝ ⟶ Y₂✝<VAR>f₁✝ : Y₁✝ ⟶ X<VAR>f₂✝ : Y₂✝ ⟶ X<VAR>h₁ : (generate R).arrows f₁✝<VAR>h₂ : (generate R).arrows f₂✝<VAR>comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝<GOAL>P.map g₁✝.op (x.sieveExtend f₁✝ h₁) = P.map g₂✝.op (x.sieveExtend f₂✝ h₂)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>hx : x.Compatible<VAR>Y₁✝ Y₂✝ Z✝ : C<VAR>g₁✝ : Z✝ ⟶ Y₁✝<VAR>g₂✝ : Z✝ ⟶ Y₂✝<VAR>f₁✝ : Y₁✝ ⟶ X<VAR>f₂✝ : Y₂✝ ⟶ X<VAR>h₁ : (generate R).arrows f₁✝<VAR>h₂ : (generate R).arrows f₂✝<VAR>comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝<GOAL>P.map (g₁✝ ≫ ⋯.choose).op (x ⋯.choose ⋯) = P.map (g₂✝ ≫ ⋯.choose).op (x ⋯.choose ⋯)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>hx : x.Compatible<VAR>Y₁✝ Y₂✝ Z✝ : C<VAR>g₁✝ : Z✝ ⟶ Y₁✝<VAR>g₂✝ : Z✝ ⟶ Y₂✝<VAR>f₁✝ : Y₁✝ ⟶ X<VAR>f₂✝ : Y₂✝ ⟶ X<VAR>h₁ : (generate R).arrows f₁✝<VAR>h₂ : (generate R).arrows f₂✝<VAR>comm : g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝<GOAL>(g₁✝ ≫ ⋯.choose) ≫ ⋯.choose = (g₂✝ ≫ ⋯.choose) ≫ ⋯.choose
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>r : R<VAR>A : (algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = C (C r)<VAR>B : (algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r = C r<GOAL>__src✝.toFun ((algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) = (algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hc : 0 < c<VAR>h : c < b<GOAL>a / b < a / c
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n ℝ<VAR>hM : M.PosDef<VAR>x : n → ℝ<VAR>hx : x ≠ 0<GOAL>0 < M.toQuadraticMap' x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n ℝ<VAR>hM : M.PosDef<VAR>x : n → ℝ<VAR>hx : x ≠ 0<GOAL>0 < x ⬝ᵥ M *ᵥ x
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hfc : ConcaveOn 𝕜 s f<VAR>hx : x ∈ s<GOAL>AntitoneOn (slope f x) (s \ {x})
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>hfc : ConcaveOn 𝕜 s f<VAR>hx : x ∈ s<GOAL>AntitoneOn ((-slope (-f)) x) (s \ {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b✝ a b : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hb : a ≠ b<GOAL>(cons a s ha).erase b = cons a (s.erase b) ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : DivInvMonoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹<VAR>a : G<VAR>n : ℕ<GOAL>f (a ^ ↑n) = f a ^ ↑n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : DivInvMonoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹<VAR>a : G<VAR>n : ℕ<GOAL>f (a ^ Int.negSucc n) = f a ^ Int.negSucc n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : ContinuousOn f s<VAR>hs : IsOpen s<VAR>hp : f ⁻¹' t ⊆ s<VAR>ht : IsOpen t<GOAL>IsOpen (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : ContinuousOn f s<VAR>hs : IsOpen s<VAR>hp : f ⁻¹' t ⊆ s<VAR>ht : IsOpen t<GOAL>f ⁻¹' t = s ∩ f ⁻¹' t