ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>(∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))) → HasFPowerSeriesAt f p z₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>(∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y 0 < ε → HasSum (fun n => y ^ n • p.coeff n) (f (z₀ + y))) → HasFPowerSeriesAt f p z₀
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<GOAL>(AdjoinRoot.isAdjoinRoot f).root = root f
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : SecondCountableTopology α<VAR>hclosed : IsClosed C<GOAL>∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : SecondCountableTopology α<VAR>hclosed : IsClosed C<VAR>b : Set (Set α)<VAR>bct : b.Countable<VAR>left✝ : ∅ ∉ b<VAR>bbasis : IsTopologicalBasis b<GOAL>∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>Kg : ℝ≥0<VAR>g : β → γ<VAR>hg : AntilipschitzWith Kg g<VAR>Kf : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith Kf f<VAR>x y : α<GOAL>↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑(Kf * Kg) * edist ((g ∘ f) x) ((g ∘ f) y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>Kg : ℝ≥0<VAR>g : β → γ<VAR>hg : AntilipschitzWith Kg g<VAR>Kf : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith Kf f<VAR>x y : α<GOAL>↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<GOAL>(coeff R n) X = if n = 1 then 1 else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x<GOAL>map (Embedding.subtype p) (Iio a) = Iio ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Iio ↑a)) = Iio ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ < y ↔ x < y ^ z
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : LieAlgebra K L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : IsKilling R L<GOAL>LinearMap.ker (killingForm R L) = ⊥
<VAR>α : Type u<VAR>β : Type u_1<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>1 < a / b ↔ b < a
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => x - ↑n
<VAR>R✝ : Type u_1<VAR>r : R✝<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>a b : S<VAR>hb : IsUnit ((aeval b) P)<VAR>hab : IsNilpotent (a - b)<GOAL>IsUnit ((aeval a) P)
<VAR>R✝ : Type u_1<VAR>r : R✝<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>a b : S<VAR>hb : IsUnit ((aeval b) P)<VAR>hab : IsNilpotent (a - b)<GOAL>IsUnit ((aeval b) P + ((aeval a) P - (aeval b) P))
<VAR>R✝ : Type u_1<VAR>r : R✝<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>a b : S<VAR>hb : IsUnit ((aeval b) P)<VAR>hab : IsNilpotent (a - b)<GOAL>IsNilpotent ((aeval a) P - (aeval b) P)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o : Option α<VAR>a m : α<VAR>tl : List α<VAR>hd : α<GOAL>(foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) → (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l : List α<VAR>o : Option α<VAR>a m : α<VAR>tl : List α<VAR>hd : α<GOAL>(foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) → ¬Option.rec (some hd) (fun val => if r hd val then some hd else some val) (foldl (argAux r) o tl) = none
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in atTop, p x<GOAL>∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in atTop, p x<VAR>S : Set α<VAR>hSf : S.Finite<VAR>hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x<GOAL>∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in atTop, p x<VAR>S : Set α<VAR>hSf : S.Finite<VAR>hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x<VAR>x : α<VAR>hx : x ∈ ⋂ i, (fun x => Ici ↑x) i<VAR>y : α<VAR>hy : x ≤ y<GOAL>p y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in atTop, p x<VAR>S : Set α<VAR>hSf : S.Finite<VAR>x y : α<VAR>hy : x ≤ y<VAR>hS : ∀ ⦃x : α⦄, (∀ i ∈ S, x ∈ Ici i) → p x<VAR>hx : ∀ (i : ↑S), x ∈ Ici ↑i<GOAL>p y
<VAR>z : ℂ<GOAL>abs z ^ 2 - z.im ^ 2 = z.re ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>ι : Type u_5<VAR>inst✝ : One β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>(fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[atTop] fun x => (iUnion s).mulIndicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>ι : Type u_5<VAR>inst✝ : One β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>(fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[atTop] fun x => (⋃ t, ⋃ i ∈ t, s i).mulIndicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>ι : Type u_5<VAR>inst✝ : One β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>Monotone fun i => ⋃ i_1 ∈ i, s i_1
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D<VAR>c : C<VAR>d : D<VAR>F : C ⥤ D<VAR>f : (evaluationLeftAdjoint D c).obj d ⟶ F<VAR>x : C<VAR>g : c ⟶ x<GOAL>(Sigma.ι (fun x => d) g ≫ Sigma.desc fun h => (Sigma.ι (fun x => d) (𝟙 c) ≫ f.app c) ≫ F.map h) = Sigma.ι (fun x => d) g ≫ f.app x
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : 0 ≤ z<GOAL>1 ≤ x ^ z
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx : 1 ≤ x<VAR>hz : 0 ≤ z<GOAL>1 ^ z ≤ x ^ z
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(∃'θ).Realize v xs ↔ ∃ a, θ.Realize v (snoc xs a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<GOAL>variationOnFromTo f s a b = -variationOnFromTo f s b a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>ab : a < b<GOAL>variationOnFromTo f s a b = -variationOnFromTo f s b a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a : α<GOAL>variationOnFromTo f s a a = -variationOnFromTo f s a a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>ba : b < a<GOAL>variationOnFromTo f s a b = -variationOnFromTo f s b a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i✝ : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝ : CommSemiring α<VAR>s : Finset ι<VAR>i : ι<VAR>f g h : ι → α<VAR>hi : i ∈ s<VAR>h1 : g i + h i = f i<VAR>h2 : ∀ j ∈ s, j ≠ i → g j = f j<VAR>h3 : ∀ j ∈ s, j ≠ i → h j = f j<GOAL>∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i
<VAR>k G : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Group G<VAR>A✝ A : Rep k G<VAR>inst✝ : A.IsTrivial<GOAL>oneCoboundaries A = ⊥
<VAR>k G : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Group G<VAR>A✝ A : Rep k G<VAR>inst✝ : A.IsTrivial<GOAL>LinearMap.range (LinearMap.codRestrict (oneCocycles A) 0 ⋯) = ⊥
<VAR>n : ℤ<GOAL>χ₄ ↑n = χ₄ ↑(n % 4)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>m n : ZNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>m n : ZNum<GOAL>¬↑n < ↑m ↔ m ≤ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>S : F →L[𝕜] E<GOAL>IsSelfAdjoint ((adjoint S).comp (T.comp S))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : adjoint T = T<VAR>S : F →L[𝕜] E<GOAL>adjoint ((adjoint S).comp (T.comp S)) = (adjoint S).comp (T.comp S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : adjoint T = T<VAR>S : F →L[𝕜] E<GOAL>((adjoint S).comp T).comp S = (adjoint S).comp (T.comp S)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ LinearMap.range S.f = LinearMap.ker S.g
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>LinearMap.ker S.g ≤ LinearMap.range S.f ↔ LinearMap.range S.f = LinearMap.ker S.g
<VAR>k : ℤ<VAR>a : Fin 2 → ℤ<GOAL>DifferentiableOn ℂ (fun z => (↑(a 0) * z + ↑(a 1)) ^ (-k)) {z | 0 < z.im}
<VAR>k : ℤ<VAR>a : Fin 2 → ℤ<VAR>ha : a ≠ 0<GOAL>DifferentiableOn ℂ (fun z => (↑(a 0) * z + ↑(a 1)) ^ (-k)) {z | 0 < z.im}
<VAR>k : ℤ<GOAL>DifferentiableOn ℂ (fun z => (↑(0 0) * z + ↑(0 1)) ^ (-k)) {z | 0 < z.im}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>ι : Type u_4<VAR>F : ι → β → α<VAR>inst✝ : CompactSpace β<VAR>h : Equicontinuous F<GOAL>UniformEquicontinuous F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>ι : Type u_4<VAR>F : ι → β → α<VAR>inst✝ : CompactSpace β<VAR>h : Continuous (⇑UniformFun.ofFun ∘ Function.swap F)<GOAL>UniformEquicontinuous F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>ι : Type u_4<VAR>F : ι → β → α<VAR>inst✝ : CompactSpace β<VAR>h : Continuous (⇑UniformFun.ofFun ∘ Function.swap F)<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n m : ℕ<GOAL>(trunc n 0).coeff m = Polynomial.coeff 0 m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n m : ℕ<GOAL>(if m < n then 0 else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : Zero β<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>f g : α →ₛ β<VAR>H : f ≤ g<VAR>hs : MeasurableSet s<VAR>x : α<GOAL>↑(f.restrict s) x ≤ ↑(g.restrict s) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝¹ : Zero β<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>f g : α →ₛ β<VAR>H : f ≤ g<VAR>hs : ¬MeasurableSet s<GOAL>f.restrict s ≤ g.restrict s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>s : Set E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<GOAL>Balanced 𝕜 ((convexHull ℝ) s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>s : Set E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<GOAL>Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull ℝ) s}
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>s : Set E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>x : E<VAR>hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull ℝ) s}<VAR>y : E<VAR>hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull ℝ) s}<VAR>u v : ℝ<VAR>hu : 0 ≤ u<VAR>hv : 0 ≤ v<VAR>huv : u + v = 1<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>a • (u • x + v • y) ∈ (convexHull ℝ) s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>s : Set E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>x : E<VAR>hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull ℝ) s}<VAR>y : E<VAR>hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull ℝ) s}<VAR>u v : ℝ<VAR>hu : 0 ≤ u<VAR>hv : 0 ≤ v<VAR>huv : u + v = 1<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>u • a • x + v • a • y ∈ (convexHull ℝ) s
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<GOAL>#(α ≃ β') = #(α → β')
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<VAR>e : α ≃ β'<GOAL>#(α ≃ β') = #(α → β')
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<VAR>e : α ≃ β'<VAR>e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')<GOAL>#(α ≃ β') = #(α → β')
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<VAR>e : α ≃ β'<VAR>e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')<VAR>e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')<GOAL>#(α ≃ β') = #(α → β')
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>leq : lift.{v, u} #α = lift.{u, v} #β'<VAR>e : α ≃ β'<VAR>e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')<VAR>e₂ : lift.{max u v, u} #(α → α) = #(α → β')<GOAL>#(α ≃ β') = #(α → β')
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a b c : ⨁ (i : ι), A i<GOAL>a * b * c = a * (b * c)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a b c : ⨁ (i : ι), A i<GOAL>(compHom (mulHom A)).comp (mulHom A) = ((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a b c : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<VAR>bi : ι<VAR>bx : A bi<VAR>ci : ι<VAR>cx : A ci<GOAL>(((((((compHom (mulHom A)).comp (mulHom A)).comp (of A ai)) ax).comp (of A bi)) bx).comp (of A ci)) cx = (((((((compHom flipHom) ((compHom (mulHom A).flip).comp (mulHom A))).flip.comp (of A ai)) ax).comp (of A bi)) bx).comp (of A ci)) cx
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a b c : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<VAR>bi : ι<VAR>bx : A bi<VAR>ci : ι<VAR>cx : A ci<GOAL>((mulHom A) (((mulHom A) ((of A ai) ax)) ((of A bi) bx))) ((of A ci) cx) = ((mulHom A) ((of A ai) ax)) (((mulHom A) ((of A bi) bx)) ((of A ci) cx))
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>a b c : ⨁ (i : ι), A i<VAR>ai : ι<VAR>ax : A ai<VAR>bi : ι<VAR>bx : A bi<VAR>ci : ι<VAR>cx : A ci<GOAL>(of A (ai + bi + ci)) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul ax bx) cx) = (of A (ai + (bi + ci))) (GradedMonoid.GMul.mul ax (GradedMonoid.GMul.mul bx cx))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<VAR>h : SurjOn f E N.E<GOAL>(N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ InjOn f B ∧ B ⊆ E
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f g : α → β<VAR>s : Multiset α<VAR>h : ∀ x ∈ s, f x = g x<GOAL>map f s = map g s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f g : α → β<VAR>a✝ : List α<VAR>h : ∀ x ∈ Quot.mk Setoid.r a✝, f x = g x<GOAL>map f (Quot.mk Setoid.r a✝) = map g (Quot.mk Setoid.r a✝)
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>ss : TM2.Supports M S<VAR>l' : Λ'<VAR>h : l' ∈ trSupp M S<GOAL>TM1.SupportsStmt (trSupp M S) (tr M l')
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>S : Finset Λ<VAR>ss : TM2.Supports M S<VAR>l' : Λ'<VAR>h : l' ∈ trSupp M S<GOAL>∀ (q : Stmt₂), TM2.SupportsStmt S q → (∀ x ∈ trStmts₁ q, x ∈ trSupp M S) → TM1.SupportsStmt (trSupp M S) (trNormal q) ∧ ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l')
<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>g : E → F<VAR>c✝ : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>𝕜' : Type u_6<VAR>inst✝³ : NormedRing 𝕜'<VAR>inst✝² : Module 𝕜' F<VAR>inst✝¹ : BoundedSMul 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>↑↑((c • L).compLp f) =ᶠ[ae μ] ↑↑(c • L.compLp f)
<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>g : E → F<VAR>c✝ : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>𝕜' : Type u_6<VAR>inst✝³ : NormedRing 𝕜'<VAR>inst✝² : Module 𝕜' F<VAR>inst✝¹ : BoundedSMul 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(fun a => (c • L) (↑↑f a)) =ᶠ[ae μ] ↑↑(c • L.compLp f)
<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>g : E → F<VAR>c✝ : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>𝕜' : Type u_6<VAR>inst✝³ : NormedRing 𝕜'<VAR>inst✝² : Module 𝕜' F<VAR>inst✝¹ : BoundedSMul 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(fun a => (c • L) (↑↑f a)) =ᶠ[ae μ] c • ↑↑(L.compLp f)
<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>g : E → F<VAR>c✝ : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>𝕜' : Type u_6<VAR>inst✝³ : NormedRing 𝕜'<VAR>inst✝² : Module 𝕜' F<VAR>inst✝¹ : BoundedSMul 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<VAR>x : α<VAR>hx : ↑↑(L.compLp f) x = (fun a => L (↑↑f a)) x<GOAL>(fun a => (c • L) (↑↑f a)) x = (c • ↑↑(L.compLp f)) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i : Fin b.length<GOAL>(a.blocks.splitWrtComposition b)[↑i].length = b.blocksFun i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>a : Composition n<VAR>b : Composition a.length<VAR>i : Fin b.length<GOAL>b.blocks[↑i] = b.blocksFun i
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>f : A →ₗ[R] A'<GOAL>Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<GOAL>gp.a = 1 ∧ ∃ z, gp.b = ↑z
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<VAR>ifp : IntFractPair K<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp<GOAL>gp.a = 1 ∧ ∃ z, gp.b = ↑z