ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b✝ : Basis ι R M<VAR>c : Basis κ R M<VAR>s : Finset M<VAR>b : Basis { x // x ∈ s } R M<VAR>f : M →ₗ[R] M<VAR>this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)<GOAL>traceAux R ⋯.some = traceAux R b
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0∞<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0∞<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<VAR>h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0∞<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<VAR>h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)<VAR>h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0∞<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<VAR>h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)<VAR>h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p<GOAL>((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>(swap x y).support = { val := x ::ₘ y ::ₘ 0, nodup := ⋯ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>r : Set α<VAR>hinj : InjOn f r<VAR>hrs : r ⊆ s<GOAL>∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>r : Set α<VAR>hinj : InjOn f r<VAR>hrs : r ⊆ s<VAR>u : Set α<VAR>hru : r ⊆ u<VAR>hus : u ⊆ s<VAR>h : BijOn f u (f '' s)<GOAL>∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Subring R<VAR>f : R →+* S<GOAL>↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f : α → M<VAR>n : ℕ<GOAL>(∑ i ∈ range n, i) * 2 = ∑ i ∈ range n, i + ∑ i ∈ range n, (n - 1 - i)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f : α → M<VAR>n : ℕ<GOAL>∑ i ∈ range n, (n - 1) = n * (n - 1)
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocRing R✝<VAR>inst✝⁴ : Pow R✝ ℕ<VAR>inst✝³ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocRing R✝<VAR>inst✝⁴ : Pow R✝ ℕ<VAR>inst✝³ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) = (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocRing R✝<VAR>inst✝⁴ : Pow R✝ ℕ<VAR>inst✝³ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) = (k + 1) • (descPochhammer ℤ k).smeval r + ((X - ↑k) * descPochhammer ℤ k).smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : NonAssocRing R✝<VAR>inst✝⁴ : Pow R✝ ℕ<VAR>inst✝³ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r = k • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r + (r * (descPochhammer ℤ k).smeval r - (↑k).smeval r * (descPochhammer ℤ k).smeval r)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>ofDual (s.max' hs) = (image (⇑ofDual) s).min' ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>↑(ofDual (s.max' hs)) = ↑((image (⇑ofDual) s).min' ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<VAR>hs : s.Nonempty<GOAL>s.inf (WithTop.some ∘ fun x => ofDual x) = s.inf ((WithTop.some ∘ fun x => x) ∘ ⇑ofDual)
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<VAR>x✝ : UniformSpace α := ⊥<GOAL>UniformEmbedding f
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<VAR>x✝ : UniformSpace α := ⊥<VAR>this : DiscreteTopology α<GOAL>UniformEmbedding f
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>r s ε x : ℝ<VAR>hx : x ∈ B f K r s ε<GOAL>B f K r s ε ∈ 𝓝[>] x
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>r s ε x : ℝ<VAR>hx : x ∈ B f K r s ε<VAR>L : F<VAR>LK : L ∈ K<VAR>hL₁ : x ∈ A f L r ε<VAR>hL₂ : x ∈ A f L s ε<GOAL>B f K r s ε ∈ 𝓝[>] x
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>r s ε x : ℝ<VAR>hx : x ∈ B f K r s ε<VAR>L : F<VAR>LK : L ∈ K<VAR>hL₁ : x ∈ A f L r ε<VAR>hL₂ : x ∈ A f L s ε<VAR>y : ℝ<VAR>hy₁ : y ∈ A f L r ε<VAR>hy₂ : y ∈ A f L s ε<GOAL>y ∈ B f K r s ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>r s ε x : ℝ<VAR>hx : x ∈ B f K r s ε<VAR>L : F<VAR>LK : L ∈ K<VAR>hL₁ : x ∈ A f L r ε<VAR>hL₂ : x ∈ A f L s ε<VAR>y : ℝ<VAR>hy₁ : y ∈ A f L r ε<VAR>hy₂ : y ∈ A f L s ε<GOAL>∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>m : Multiset α<VAR>l : List α<GOAL>List.pmap mk l ⋯ = List.map (fun p => ⟨↑p, ⋯⟩) (List.pmap mk l ⋯)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>m : Multiset α<VAR>l : List α<GOAL>List.pmap mk l ⋯ = List.pmap (fun a_1 h => ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T3Space β<VAR>ι : Type u_5<VAR>s : ι → Set α<VAR>p : ι → Prop<VAR>x : α<VAR>h : (𝓝 x).HasBasis p s<VAR>f : α → β<VAR>hf : DenseInducing f<GOAL>(𝓝 (f x)).HasBasis p fun i => closure (f '' s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T3Space β<VAR>ι : Type u_5<VAR>s : ι → Set α<VAR>p : ι → Prop<VAR>x : α<VAR>h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t<VAR>f : α → β<VAR>hf : DenseInducing f<GOAL>∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : StronglyMeasurable f<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm f p (μ.trim hm) = eLpNorm f p μ
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>a : α<VAR>l : List β<GOAL>foldl (fun b x => f b) a l = f^[l.length] a
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : S ∈ rightTransversals ↑H<GOAL>Finite ↑S ↔ H.FiniteIndex
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : S ∈ rightTransversals ↑H<GOAL>Finite (G ⧸ H) ↔ H.FiniteIndex
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasForget₂ C Ab<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : (forget₂ C Ab).PreservesZeroMorphisms<VAR>S : ShortComplex C<VAR>x : ↑((forget₂ C Ab).obj S.X₁)<GOAL>((forget₂ C Ab).map S.g) (((forget₂ C Ab).map S.f) x) = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasForget₂ C Ab<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : (forget₂ C Ab).PreservesZeroMorphisms<VAR>S : ShortComplex C<VAR>x : ↑((forget₂ C Ab).obj S.X₁)<GOAL>0 x = 0
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>s \ ⋃₀ ↑I = ⋃₀ ↑(hC.diffFinset₀ hs hI)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S✝ : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>S : Submonoid N<VAR>h : S ≤ MonoidHom.mrange f<GOAL>map f (comap f S) = S
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : ℚ<GOAL>↑(fract x) = fract ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>b0 : b ≠ 0<VAR>h : a < b * succ c<GOAL>a / b ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>b0 : b ≠ 0<VAR>h : a < b * succ c<GOAL>sInf {o | a < b * succ o} ≤ c
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>S : IntermediateField E K := separableClosure E K<GOAL>adjoin E ↑(separableClosure F K) = S
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>S : IntermediateField E K := separableClosure E K<VAR>h : lift (adjoin E ↑(separableClosure F ↥S)) = lift ⊤<GOAL>adjoin E ↑(separableClosure F K) = S
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>S : IntermediateField E K := separableClosure E K<VAR>h : adjoin E (Subtype.val '' ↑(separableClosure F ↥S)) = S<GOAL>adjoin E ↑(separableClosure F K) = S
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>S : IntermediateField E K := separableClosure E K<VAR>h : adjoin E (Subtype.val '' ↑(separableClosure F ↥S)) = S<VAR>this : IsScalarTower F (↥S) K<GOAL>adjoin E ↑(separableClosure F K) = S
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>S : IntermediateField E K := separableClosure E K<VAR>h : adjoin E (Subtype.val '' ↑(separableClosure F ↥S)) = S<VAR>this : IsScalarTower F (↥S) K<GOAL>adjoin E ↑(IntermediateField.map (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K) (separableClosure F ↥(separableClosure E K))) = adjoin E (Subtype.val '' ↑(separableClosure F ↥S))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : α → ℝ≥0<VAR>hg : Summable g<VAR>i : α<VAR>hi : 0 < g i<GOAL>0 < ∑' (b : α), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : α → ℝ≥0<VAR>hg : Summable g<VAR>i : α<VAR>hi : 0 < g i<GOAL>∑' (x : ?m.316521), 0 < ∑' (b : α), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : α → ℝ≥0<VAR>hg : Summable g<VAR>i : α<VAR>hi : 0 < g i<GOAL>Type ?u.316518
<VAR>R : Type u<VAR>S : Type u'<VAR>M✝ : Type v<VAR>N : Type w<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Ring M<VAR>inst✝⁵ : Algebra K M<VAR>inst✝⁴ : Module.Free K M<VAR>inst✝³ : Module.Finite K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>#(M →ₐ[K] L) ≤ lift.{v, u_2} (Module.rank K M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M✝ : Type v<VAR>N : Type w<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Ring M<VAR>inst✝⁵ : Algebra K M<VAR>inst✝⁴ : Module.Free K M<VAR>inst✝³ : Module.Finite K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>#(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)
<VAR>R : Type u<VAR>S : Type u'<VAR>M✝ : Type v<VAR>N : Type w<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Ring M<VAR>inst✝⁵ : Algebra K M<VAR>inst✝⁴ : Module.Free K M<VAR>inst✝³ : Module.Finite K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_3<VAR>inst✝² : CommMonoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass S R M<VAR>a : R<VAR>x : M<VAR>x✝ : x ∈ __src✝.carrier<VAR>b : S<VAR>h : b • x = 0<GOAL>b • a • x = 0
<VAR>α : Type u_1<VAR>inst✝ : Semigroup α<VAR>s : Set α<VAR>a b : α<GOAL>a • b • s = (a * b) • s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>h : Measurable fun x => ↑(f x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a : α<GOAL>erase a 0 = 0
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module k V<VAR>inst✝⁶ : AffineSpace V P<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module k V₁<VAR>inst✝³ : AffineSpace V₁ P₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>v : V₁<VAR>s : AffineSubspace k P₁<GOAL>map f (v +ᵥ s) = f.linear v +ᵥ map f s
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module k V<VAR>inst✝⁶ : AffineSpace V P<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module k V₁<VAR>inst✝³ : AffineSpace V₁ P₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>v : V₁<VAR>s : AffineSubspace k P₁<GOAL>map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module k V<VAR>inst✝⁶ : AffineSpace V P<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module k V₁<VAR>inst✝³ : AffineSpace V₁ P₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>v : V₁<VAR>s : AffineSubspace k P₁<VAR>p✝ : P₁<GOAL>(f.comp ↑(AffineEquiv.constVAdd k P₁ v)) p✝ = ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) p✝
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Ico a b).card = ∏ i : ι, (Icc (a i) (b i)).card - 1
<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<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S R<VAR>inst✝ : IsScalarTower S R R<VAR>s : S<VAR>p : R[X]<VAR>x : R<GOAL>eval x (s • p) = s • eval x p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsHamiltonian<GOAL>p.length + 1 = Fintype.card α
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b c : α<GOAL>a ∈ [b, c] ↔ a = b ∨ a = c
<VAR>α : Type u_1<VAR>M : Type u<VAR>N : Type v<VAR>P : Type w<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>f : M →* N<VAR>g : M → Nˣ<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>f x * ↑((liftRight f g h) x)⁻¹ = 1
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht : ∀ (i : ι), SecondCountableTopology α<GOAL>SecondCountableTopology α
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X : C<GOAL>diag X ≫ σ = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>h : X ≃ₜ Y<VAR>h_iff : ∀ (x : X), p x ↔ q (h x)<GOAL>Continuous __spread✝⁻⁰.toFun
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>h : X ≃ₜ Y<VAR>h_iff : ∀ (x : X), p x ↔ q (h x)<GOAL>Continuous __spread✝⁻⁰.invFun
<VAR>a : ℂ<VAR>r : ℝ<GOAL>volume (Metric.closedBall a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>a₁ b₁ : ℝ<VAR>h₁ : a₁ ≤ b₁<VAR>a₂ b₂ : ℝ<VAR>Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])<VAR>Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])<VAR>Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume<VAR>h₂ : a₂ ≤ b₂<GOAL>∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>a₁ b₁ : ℝ<VAR>h₁ : a₁ ≤ b₁<VAR>a₂ b₂ : ℝ<VAR>h₂ : a₂ ≤ b₂<VAR>Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)<VAR>Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)<VAR>Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x<VAR>Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume<GOAL>∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>x : M<VAR>s : Set M<GOAL>span R (insert x s) = span R {x} ⊔ span R s
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : Rel r a b<GOAL>Rel r (a - c) (b - c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>q : α<VAR>hq : ¬IsUnit q<VAR>hq' : q ≠ 0<GOAL>Function.Injective fun n => q ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>q : α<VAR>hq : ¬IsUnit q<VAR>hq' : q ≠ 0<VAR>n m : ℕ<VAR>h : n < m<GOAL>¬IsUnit (q ^ (m - n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>q : α<VAR>hq : ¬IsUnit q<VAR>hq' : q ≠ 0<VAR>n m : ℕ<VAR>h : n < m<GOAL>q ^ m = q ^ n * q ^ (m - n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<GOAL>X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯).op
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s<GOAL>TendstoUniformlyOn F f l s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s<GOAL>∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q => (f q.2, F q.1 q.2)) ∘ x) atTop (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s<VAR>u : ℕ → ι × α<VAR>hu : Tendsto u atTop (l ×ˢ 𝓟 s)<GOAL>Tendsto ((fun q => (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)