ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>0 < Nat.card α ↔ Nonempty α
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>I : Finset ι<VAR>hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I<GOAL>∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>I : Finset ι<VAR>hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I<VAR>x : X<VAR>hx : (support fun i => (ρ i) x) ⊆ ↑I<VAR>x_in : x ∈ s<GOAL>∑ i ∈ I, (ρ i) x = 1
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>I : Finset ι<VAR>hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I<VAR>x : X<VAR>hx : (support fun i => (ρ i) x) ⊆ ↑I<VAR>x_in : x ∈ s<VAR>this : ∑ᶠ (i : ι), (ρ i) x = ∑ i ∈ I, (ρ i) x<GOAL>∑ i ∈ I, (ρ i) x = 1
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R M<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : _root_.Finite n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>bM : Basis m R M<VAR>bN : Basis n R N<VAR>j : m<VAR>i i' : n<VAR>j' : m<GOAL>(toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = stdBasisMatrix i j 1 i' j'
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R M<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : _root_.Finite n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>bM : Basis m R M<VAR>bN : Basis n R N<VAR>j : m<VAR>i i' : n<VAR>j' : m<VAR>hij : ¬(i = i' ∧ j = j')<GOAL>Pi.single i (Pi.single j' 1 j) i' = 0
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R M<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : _root_.Finite n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>bM : Basis m R M<VAR>bN : Basis n R N<VAR>j : m<VAR>i i' : n<VAR>j' : m<VAR>hij : ¬i = i' ∨ ¬j = j'<GOAL>Pi.single i (Pi.single j' 1 j) i' = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter γ<VAR>p : α × γ × γ → Prop<VAR>h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x<GOAL>∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter γ<VAR>p : α × γ × γ → Prop<VAR>h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x<VAR>t : α → Prop<VAR>ht : ∀ᶠ (x : α) in f, t x<VAR>s : γ × γ → Prop<VAR>hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y<VAR>hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)<GOAL>∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix p m R<GOAL>B * (A * Aᴴ) = 0 ↔ B * A = 0
<VAR>b x y : ℝ<VAR>k : ℕ<VAR>hx : 0 < x<GOAL>logb b (x ^ k) = ↑k * logb b x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<GOAL>StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>x✝ : Measurable f ∧ IsSeparable (range f)<VAR>Hm : Measurable f<VAR>Hsep : IsSeparable (range f)<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>x✝ : Measurable f ∧ IsSeparable (range f)<VAR>Hm : Measurable f<VAR>Hsep : IsSeparable (range f)<VAR>this : SecondCountableTopology ↑(range f)<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>x✝ : Measurable f ∧ IsSeparable (range f)<VAR>Hm : Measurable f<VAR>Hsep : IsSeparable (range f)<VAR>this : SecondCountableTopology ↑(range f)<VAR>Hm' : StronglyMeasurable (rangeFactorization f)<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s * t)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (t * s)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : WalkingParallelPair ⥤ TopCat<VAR>U : Set ↑(colimit F)<GOAL>IsOpen U ↔ IsOpen (⇑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : WalkingParallelPair ⥤ TopCat<VAR>U : Set ↑(colimit F)<GOAL>(∀ (j : WalkingParallelPair), IsOpen (⇑(colimit.ι F j) ⁻¹' U)) ↔ IsOpen (⇑(colimit.ι F WalkingParallelPair.one) ⁻¹' U)
<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 a' : α<VAR>b : M<VAR>inst✝ : Unique α<VAR>b' : M<GOAL>single a b = single a' b' ↔ b = b'
<VAR>x y : ℝ<VAR>hxy : x ≤ y<GOAL>↑x ≤ ↑y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : Preorder G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a • c < b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : Preorder G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a • d < b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : Preorder G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>¬b • d ≤ a • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : Preorder G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<VAR>hbad : b • d ≤ a • d<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : Preorder G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<VAR>hbad : b • d ≤ a • d<VAR>h : b ≤ a<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : Preorder G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b ∧ ¬b ≤ a<VAR>h₂ : c ≤ d<VAR>hbad : b • d ≤ a • d<VAR>h : b ≤ a<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>sublistsLen 1 [] = map (fun x => [x]) [].reverse
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>a : α<VAR>s : List α<VAR>ih : sublistsLen 1 s = map (fun x => [x]) s.reverse<GOAL>sublistsLen 1 (a :: s) = map (fun x => [x]) (a :: s).reverse
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>a : α<VAR>s : List α<VAR>ih : sublistsLen 1 s = map (fun x => [x]) s.reverse<GOAL>map (fun x => [x]) s.reverse ++ map (cons a) [[]] = map (fun x => [x]) s.reverse ++ map (fun x => [x]) [a]
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>h : R ⊆ E<GOAL>freeOn E ↾ R = freeOn R
<VAR>V : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup V<VAR>inst✝ : NormedSpace ℝ V<VAR>K✝ L✝ K L : ConvexBody V<GOAL>EMetric.hausdorffEdist ↑K ↑L ≠ ⊤
<VAR>n m l : ℕ<GOAL>Ico n m ∩ Ico m l = []
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s✝ s s' : Set (Sym2 V)<GOAL>(G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>{x | ∃ k, beattySeq' r k = x}ᶜ = {x | ∃ k, beattySeq s k = x}
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<GOAL>x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a<GOAL>x ≤ limsup u f
<GOAL>WithBot.some ∘ WithTop.some ⁻¹' Ioi ⊥ = univ
<GOAL>WithTop.some ⁻¹' (WithBot.some ⁻¹' Ioi ⊥) = univ
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>x y : α<GOAL>f * swap x y = swap (f x) (f y) * f
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<GOAL>LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>i : ℕ<VAR>x : α<VAR>l : List α<GOAL>(i, x) ∈ l.enum ↔ l.get? i = some x
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#↑{f | Surjective f} = 0 ↔ lift.{v, u} #α < lift.{u, v} #β' ∨ #α ≠ 0 ∧ #β' = 0
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ ¬#β' = 0) ∧ Nonempty (β' ↪ α)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<GOAL>CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ 𝓝 x
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZeta (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>k : ℕ<VAR>hk : k.succ ≠ 0<GOAL>hurwitzZetaOdd (↑x) (1 - 2 * ↑k.succ) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s✝ t✝ u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>s t : Colex α<GOAL>s < t ↔ ∃ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s✝ t✝ u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>s t : Colex α<GOAL>(∀ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex) ∧ s ≠ t ↔ ∃ (h : s ≠ t), (s.ofColex ∆ t.ofColex).max' ⋯ ∈ t.ofColex
<VAR>x : ℝ≥0∞<VAR>z : ℝ<GOAL>x.toReal ^ z = (x ^ z).toReal
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝³ : HasImage f<VAR>inst✝² : HasCokernel (image.ι f)<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : Epi (factorThruImage f)<GOAL>image.ι f ≫ cokernel.π f = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝³ : HasImage f<VAR>inst✝² : HasCokernel (image.ι f)<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : Epi (factorThruImage f)<VAR>w : f ≫ cokernel.π f = 0<GOAL>image.ι f ≫ cokernel.π f = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝³ : HasImage f<VAR>inst✝² : HasCokernel (image.ι f)<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : Epi (factorThruImage f)<VAR>w : (factorThruImage f ≫ image.ι f) ≫ cokernel.π f = 0<GOAL>image.ι f ≫ cokernel.π f = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝³ : HasImage f<VAR>inst✝² : HasCokernel (image.ι f)<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : Epi (factorThruImage f)<VAR>w : image.ι f ≫ cokernel.π f = 0<GOAL>image.ι f ≫ cokernel.π f = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝³ : HasImage f<VAR>inst✝² : HasCokernel (image.ι f)<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : Epi (factorThruImage f)<GOAL>f ≫ cokernel.π (image.ι f) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝³ : HasImage f<VAR>inst✝² : HasCokernel (image.ι f)<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : Epi (factorThruImage f)<GOAL>(factorThruImage f ≫ image.ι f) ≫ cokernel.π (image.ι f) = 0
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>s : Set α<GOAL>(c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>s : Set α<VAR>this : Nonempty { t // s ⊆ ⋃ i, t i }<GOAL>(c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>s : Set α<VAR>this : Nonempty { t // s ⊆ ⋃ i, t i }<GOAL>c * ⨅ x, ∑' (n : ℕ), m (↑x n) = ⨅ x, c * ∑' (i : ℕ), m (↑x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommSemigroup G<VAR>a b c d : G<GOAL>a * b * (c * d) = a * c * (b * d)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Finset α<VAR>a b : α<GOAL>{b}.preimage (fun x => a * x) ⋯ = {a⁻¹ * b}
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f : G → E<VAR>g : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>hf' : ∀ (x : G), f (g * x) = -f x<GOAL>∫ (x : G), f x ∂μ = 0
<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1), ↑((n + 1).choose k) • bernoulli k = (monomial n) (↑n + 1)
<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1 - 0), ∑ k_1 ∈ range (n + 1 - (0 + k)), ↑((n + 1).choose (0 + k + k_1)) • (monomial (0 + k)) (_root_.bernoulli (0 + k + k_1 - (0 + k)) * ↑((0 + k + k_1).choose (0 + k))) = (monomial n) (↑n + 1)
<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), ∑ x_1 ∈ range (n + 1 - x), ↑((n + 1).choose (x + x_1)) • (monomial x) (_root_.bernoulli x_1 * ↑((x + x_1).choose x)) = (monomial n) ↑n + (monomial n) 1
<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), ∑ x_1 ∈ range (n + 1 - x), (monomial x) (↑((n + 1).choose (x + x_1)) * ↑((x + x_1).choose x) * _root_.bernoulli x_1) = (monomial n) ↑n + (monomial n) 1
<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), ∑ x_1 ∈ range (n + 1 - x), (↑((n + 1 - x).choose x_1) * _root_.bernoulli x_1) • (monomial x) ↑((n + 1).choose x) = (monomial n) ↑n + (monomial n) 1
<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = (monomial n) ↑n + (monomial n) 1
<VAR>n : ℕ<GOAL>(∑ i ∈ range (n + 1 - n), ↑((n + 1 - n).choose i) * _root_.bernoulli i) • (monomial n) ↑((n + 1).choose n) + ∑ x ∈ range n, (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = (monomial n) ↑n + (monomial n) 1
<VAR>n : ℕ<GOAL>∑ x ∈ range n, (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = 0
<VAR>n : ℕ<GOAL>∀ x ∈ range n, (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = 0
<VAR>n : ℕ<VAR>f : ∀ x ∈ range n, ¬n + 1 - x = 1<GOAL>∀ x ∈ range n, (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = 0
<VAR>n : ℕ<VAR>f : ∀ x ∈ range n, ¬n + 1 - x = 1<VAR>x : ℕ<VAR>hx : x ∈ range n<GOAL>(∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) = 0
<VAR>n : ℕ<VAR>f : ∀ x ∈ range n, ¬n + 1 - x = 1<VAR>x : ℕ<VAR>hx : x ∈ range n<GOAL>(if n + 1 - x = 1 then 1 else 0) • (monomial x) ↑((n + 1).choose x) = 0
<VAR>n : ℕ<VAR>f : ∀ x ∈ range n, ¬n + 1 - x = 1<VAR>x : ℕ<VAR>hx : x ∈ range n<VAR>g : (if n + 1 - x = 1 then 1 else 0) = 0<GOAL>(if n + 1 - x = 1 then 1 else 0) • (monomial x) ↑((n + 1).choose x) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<GOAL>IsBoundedLinearMap 𝕜 fun x => x.1
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>x : E × F<GOAL>‖(LinearMap.fst 𝕜 E F) x‖ ≤ 1 * ‖x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>x : E × F<GOAL>‖(LinearMap.fst 𝕜 E F) x‖ ≤ ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>h : ∀ x ∈ s, f x ∈ t<GOAL>(t.biUnion fun a => filter (fun c => f c = a) s) = s
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h : a < b<GOAL>#↑(Ioo a b) = 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h : a < b<GOAL>𝔠 ≤ #↑(Ioo a b)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h : a < b<VAR>h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)<GOAL>𝔠 ≤ #↑(Ioo a b)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h : a < b<VAR>h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)<GOAL>𝔠 ≤ #↑((fun x => x - a) '' Ioo a b)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h : a < b<VAR>h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)<GOAL>𝔠 ≤ #↑(Ioo 0 (b - a))
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)<VAR>h : 0 < b - a<GOAL>𝔠 ≤ #↑(Ioo 0 (b - a))
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)<VAR>h : 0 < b - a<VAR>h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))<GOAL>𝔠 ≤ #↑(Ioo 0 (b - a))
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a b : ℝ<VAR>h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)<VAR>h : 0 < b - a<VAR>h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))<GOAL>𝔠 ≤ #↑(Inv.inv '' Ioo 0 (b - a))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ico a b) (Ico (a + d) (b + d))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball 1 δ * s = thickening δ s
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this : LocallyCompactSpace H<GOAL>∀ᵐ (x : M) ∂μ, f x = 0