ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁵ : NormedField 𝕜<VAR>inst✝²⁴ : SeminormedAddCommGroup V<VAR>inst✝²³ : NormedSpace 𝕜 V<VAR>inst✝²² : PseudoMetricSpace P<VAR>inst✝²¹ : NormedAddTorsor V P<VAR>inst✝²⁰ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁹ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁸ : PseudoMetricSpace P₁<VAR>inst✝¹⁷ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁶ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁵ : NormedSpace 𝕜 V₁'<VAR>inst✝¹⁴ : MetricSpace P₁'<VAR>inst✝¹³ : NormedAddTorsor V₁' P₁'<VAR>inst✝¹² : SeminormedAddCommGroup V₂<VAR>inst✝¹¹ : NormedSpace 𝕜 V₂<VAR>inst✝¹⁰ : PseudoMetricSpace P₂<VAR>inst✝⁹ : NormedAddTorsor V₂ P₂<VAR>inst✝⁸ : SeminormedAddCommGroup V₃<VAR>inst✝⁷ : NormedSpace 𝕜 V₃<VAR>inst✝⁶ : PseudoMetricSpace P₃<VAR>inst✝⁵ : NormedAddTorsor V₃ P₃<VAR>inst✝⁴ : SeminormedAddCommGroup V₄<VAR>inst✝³ : NormedSpace 𝕜 V₄<VAR>inst✝² : PseudoMetricSpace P₄<VAR>inst✝¹ : NormedAddTorsor V₄ P₄<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>inst✝ : TopologicalSpace α<VAR>x y : P<GOAL>dist ((pointReflection 𝕜 x) y) y = ‖2‖ * dist x y
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>this : DecidableEq m := Classical.decEq m<GOAL>LinearMap.range M.vecMulLinear = span R (Set.range M)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>this : DecidableEq m := Classical.decEq m<GOAL>span R (Set.range fun x => Pi.single x 1 ᵥ* M) = span R (Set.range M)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>this : DecidableEq m := Classical.decEq m<GOAL>span R (Set.range fun x x_1 => let j := x_1; Pi.single x 1 ⬝ᵥ fun i => M i j) = span R (Set.range M)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsLindelof s<VAR>hc₁ : ∀ i ∈ b, IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i ∈ b, c i<GOAL>∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsLindelof s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<GOAL>∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsLindelof s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<VAR>d : Set ↑b<VAR>hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i<GOAL>∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsLindelof s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<VAR>d : Set ↑b<VAR>hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i<GOAL>s ⊆ ⋃ i ∈ Subtype.val '' d, c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsLindelof s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<VAR>d : Set ↑b<VAR>hd : d.Countable ∧ s ⊆ ⋃ i ∈ d, c ↑i<GOAL>s ⊆ ⋃ y ∈ d, c ↑y
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b✝¹ b' b₁ b₂ b₃ c c₁ c₂ : R<VAR>b✝ b : ℕ<VAR>x✝ : 0 < b + 1<GOAL>0 ^ (b + 1) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : NoZeroDivisors R<VAR>a : R<GOAL>a * a = 1 ↔ a = 1 ∨ a = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid M<VAR>N : Type u_5<VAR>inst✝ : Monoid N<VAR>f g : FreeMonoid α →* M<VAR>h : ∀ (x : α), f (of x) = g (of x)<VAR>l : FreeMonoid α<VAR>x : α<VAR>xs : FreeMonoid α<VAR>hxs : f xs = g xs<GOAL>f (of x * xs) = g (of x * xs)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<GOAL>(foldl (fun t h => h :: t) [] l).reverse = l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<GOAL>(foldr cons [] l.reverse).reverse = l
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<GOAL>∀ (x y : (MonoidAlgebra k G)ᵐᵒᵖ), __src✝.toFun (x * y) = __src✝.toFun x * __src✝.toFun y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<GOAL>∀ (x y : (MonoidAlgebra k G)ᵐᵒᵖ), ↑__src✝ (x * y) = ↑__src✝ x * ↑__src✝ y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<GOAL>∀ (x y : (MonoidAlgebra k G)ᵐᵒᵖ), __src✝ (x * y) = __src✝ x * __src✝ y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<GOAL>∀ (x y : (MonoidAlgebra k G)ᵐᵒᵖ), __src✝.toAddMonoidHom (x * y) = __src✝.toAddMonoidHom x * __src✝.toAddMonoidHom y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<GOAL>AddMonoidHom.mul.compr₂ __src✝.toAddMonoidHom = (AddMonoidHom.mul.comp __src✝.toAddMonoidHom).compl₂ __src✝.toAddMonoidHom
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>((((((AddMonoidHom.mul.compr₂ __src✝.toAddMonoidHom).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₁)) r₁).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₂)) r₂ = (((((((AddMonoidHom.mul.comp __src✝.toAddMonoidHom).compl₂ __src✝.toAddMonoidHom).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₁)) r₁).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₂)) r₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>(opAddEquiv.symm.trans ((mapRange.addEquiv opAddEquiv).trans (Finsupp.domCongr opEquiv))).toAddMonoidHom (opAddEquiv (Finsupp.single i₁ r₁) * opAddEquiv (Finsupp.single i₂ r₂)) = (opAddEquiv.symm.trans ((mapRange.addEquiv opAddEquiv).trans (Finsupp.domCongr opEquiv))).toAddMonoidHom (opAddEquiv (Finsupp.single i₁ r₁)) * (opAddEquiv.symm.trans ((mapRange.addEquiv opAddEquiv).trans (Finsupp.domCongr opEquiv))).toAddMonoidHom (opAddEquiv (Finsupp.single i₂ r₂))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>(Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₁ r₁) * opAddEquiv (Finsupp.single i₂ r₂)))) = (Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₁ r₁)))) * (Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₂ r₂))))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>(Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₂ r₂)) * unop (opAddEquiv (Finsupp.single i₁ r₁)))) = (Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₁ r₁)))) * (Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₂ r₂))))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>(Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (single (i₂ * i₁) (r₂ * r₁))) = (Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (Finsupp.single i₁ r₁)) * (Finsupp.domCongr opEquiv) ((mapRange.addEquiv opAddEquiv) (Finsupp.single i₂ r₂))
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) - (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>X * 1 ^ 2 * (4 * X ^ 3 + C W.b₂ * X ^ 2 + 2 * C W.b₄ * X + C W.b₆) - (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 = X ^ 4 - C W.b₄ * X ^ 2 - 2 * C W.b₆ * X - C W.b₈
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>⨅ r, ↑f ↑r = ↑f x
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>rightLim (↑f) x = ⨅ r, ↑f ↑r
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>𝓝[>] x ≠ ⊥
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>(𝓝[>] x).NeBot
<VAR>x : ℝ<GOAL>∀ (k : ℤ), arctan x ≠ (2 * ↑k + 1) * π / 2
<VAR>x : ℝ<VAR>this : ∃ k, arctan x = (2 * ↑k + 1) * π / 2<GOAL>False
<VAR>x : ℝ<VAR>k : ℤ<VAR>h : arctan x = (2 * ↑k + 1) * π / 2<GOAL>False
<VAR>x : ℝ<VAR>k : ℤ<VAR>h : arctan x = (2 * ↑k + 1) * π / 2<VAR>lb : -(π / 2) < arctan x<VAR>ub : arctan x < π / 2<GOAL>False
<VAR>x : ℝ<VAR>k : ℤ<VAR>h : arctan x = (2 * ↑k + 1) * π / 2<VAR>lb : -1 < 2 * ↑k + 1<VAR>ub : arctan x < π / 2<GOAL>False
<VAR>x : ℝ<VAR>k : ℤ<VAR>h : arctan x = (2 * ↑k + 1) * π / 2<VAR>lb : -1 < 2 * ↑k + 1<VAR>ub : 2 * ↑k + 1 < 1<GOAL>False
<VAR>x y c : ℝ<GOAL>(fun x => c) =o[atTop] log
<VAR>x y c : ℝ<GOAL>∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0
<VAR>x✝ y c x : ℝ<VAR>hx : 1 < x<GOAL>log x = 0 → c = 0
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))<GOAL>∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))<GOAL>∑ x ∈ Finset.range a, -f (x₀ + ↑(x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x
<VAR>n : ℤ<GOAL>↑n.toNat + ↑(-n).toNat = ‖n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Monoid α<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : MulAction α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosStrictMono α β<VAR>hb : 0 < b<VAR>h : a < 1<GOAL>a • b < b
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) '' Iic b = Iic (a + b)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin l.length<GOAL>l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin l.length<GOAL>l.get k = l.get ⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + n) % l.length, ⋯⟩
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin l.length<GOAL>↑k = ↑⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + n) % l.length, ⋯⟩
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin l.length<GOAL>↑k = (l.length - n % l.length + ↑k + n) % l.length
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin l.length<GOAL>↑k < l.length
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>k : Fin l.length<GOAL>n % l.length ≤ l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<VAR>h : s.encard ≤ ↑k<GOAL>∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<VAR>x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k<VAR>left✝ : s.Finite<VAR>n₀ : ℕ<VAR>hs : s.encard = ↑n₀<VAR>hle : n₀ ≤ k<GOAL>s.encard ≤ ↑k
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>b : R<VAR>ha : b * 0 ≠ 0<GOAL>b * 0 = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<GOAL>¬IsCorner ∅ x₁ y₁ x₂ y₂
<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 : Set R<VAR>a : R<VAR>x : M<GOAL>x ∈ torsionBySet R M {a} ↔ x ∈ torsionBy R M a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ X : CosimplicialObject C<VAR>X₀ : C<VAR>f : X₀ ⟶ X.obj [0]<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂<VAR>i j : SimplexCategory<VAR>g : i ⟶ j<GOAL>𝟙 X₀ ≫ f ≫ X.map ([0].const j 0) = (f ≫ X.map ([0].const i 0)) ≫ X.map g
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddMonoid τ<VAR>inst✝¹ : ContinuousAdd τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>t : τ<VAR>ht : Tendsto (fun x => x + t) f f<GOAL>ω f ϕ.toFun (ϕ.toFun t '' s) ⊆ ω f ϕ.toFun s
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddMonoid τ<VAR>inst✝¹ : ContinuousAdd τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>t : τ<VAR>ht : Tendsto (fun x => x + t) f f<GOAL>ω f (fun t_1 x => ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<GOAL>∀ (n : ℕ), (p.divX * X + C (p.coeff 0)).coeff n = p.coeff n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>hn : n ≠ 0<GOAL>conductor 1 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>hn : n ≠ 0<GOAL>FactorsThrough 1 1
<VAR>x n : ℂ<VAR>hx : x.arg ≠ π<GOAL>(starRingEnd ℂ) x ^ n = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)
<VAR>f fs : Code<VAR>k : Cont'<GOAL>codeSupp (f.cons fs) k = trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k)
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<GOAL>ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom (tensorHom f₁ f₂) f₃ j = ((f₁ i₁ ⊗ f₂ i₂) ⊗ f₃ i₃) ≫ ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>⇑h '' EMetric.closedBall x r = EMetric.closedBall (h x) r
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a b : α<VAR>l : List α<GOAL>foldl f a (b :: l) = foldr f a (b :: l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a b : α<VAR>l : List α<GOAL>f b (foldl f a l) = f b (foldr f a l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp 𝕜 2 μ)<GOAL>⟪indicatorConstLp 2 hs hμs 1, f⟫_𝕜 = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>f : ↥(Lp 𝕜 2 μ)<GOAL>⟪1, ∫ (x : α) in s, ↑↑f x ∂μ⟫_𝕜 = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hf : Integrable f ρ<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hf : Integrable f ρ<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hf : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>HasIntegral I l f vol (g I)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>∀ (ib : ℝ), 0 < ib → ∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ib
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∃ x_1, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑x_1 → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>H₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∃ x_1, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑x_1 → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>hl : l.bRiemann = false<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>s : Set (ι → ℝ)<VAR>hs : s.Countable<VAR>hlH : s.Nonempty → l.bHenstock = true<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) → x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε<VAR>δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }<VAR>Hδ₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ (ε : ℝ), 0 < ε → ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) → (l.bHenstock = true → x ∈ Box.Icc J) → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε