ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>Continuous ((f '' s).restrict ↑(hf.toPartialEquiv hc).symm)
<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>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<GOAL>MapsTo (hf.toPartialEquiv hc).invFun (hf.toPartialEquiv hc).target s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Algebra A B<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Nontrivial A<VAR>pb : PowerBasis A S<GOAL>(minpoly A pb.gen).degree = ↑pb.dim
<VAR>a b : ℕ<GOAL>↑a ⋖ ↑b ↔ a ⋖ b
<VAR>a b : ℕ<GOAL>↑a + 1 = ↑b ↔ a + 1 = b
<VAR>r θ : ℝ<VAR>hr : r ∈ Ioi 0<VAR>hθ : θ ∈ Ioo (-π) π<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) (r, θ) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
<VAR>r : ℝ<VAR>hr : r ∈ Ioi 0<VAR>hθ : 0 ∈ Ioo (-π) π<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) (r, 0) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
<VAR>r θ : ℝ<VAR>hr : r ∈ Ioi 0<VAR>hθ : θ ∈ Ioo (-π) π<VAR>h'θ : θ ≠ 0<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) (r, θ) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
<VAR>x y : ℝ<VAR>hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}<GOAL>(fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) (x, y) ∈ Ioi 0 ×ˢ Ioo (-π) π
<VAR>x y : ℝ<VAR>hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}<GOAL>0 < x ^ 2 + y ^ 2 ∧ (0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0)
<VAR>r θ : ℝ<VAR>hr : r ∈ Ioi 0<VAR>hθ : θ ∈ Ioo (-π) π<GOAL>(fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) ((fun p => (p.1 * cos p.2, p.1 * sin p.2)) (r, θ)) = (r, θ)
<VAR>r θ : ℝ<VAR>hr : r ∈ Ioi 0<VAR>hθ : θ ∈ Ioo (-π) π<GOAL>√((r * cos θ) ^ 2 + (r * sin θ) ^ 2) = r ∧ (Complex.equivRealProd.symm (r * cos θ, r * sin θ)).arg = θ
<VAR>x y : ℝ<VAR>a✝ : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) ((fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) (x, y)) = (x, y)
<VAR>x y : ℝ<VAR>a✝ : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}<VAR>A : √(x ^ 2 + y ^ 2) = Complex.abs (↑x + ↑y * Complex.I)<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) ((fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) (x, y)) = (x, y)
<VAR>x y : ℝ<VAR>a✝ : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}<VAR>A : √(x ^ 2 + y ^ 2) = Complex.abs (↑x + ↑y * Complex.I)<VAR>Z : ↑(Complex.abs (↑x + ↑y * Complex.I)) * (Complex.cos ↑(↑x + ↑y * Complex.I).arg + Complex.sin ↑(↑x + ↑y * Complex.I).arg * Complex.I) = ↑x + ↑y * Complex.I<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) ((fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) (x, y)) = (x, y)
<VAR>x y : ℝ<VAR>a✝ : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}<VAR>A : √(x ^ 2 + y ^ 2) = Complex.abs (↑x + ↑y * Complex.I)<VAR>Z : ↑(Complex.abs (↑x + ↑y * Complex.I) * cos (↑x + ↑y * Complex.I).arg) + ↑(Complex.abs (↑x + ↑y * Complex.I) * sin (↑x + ↑y * Complex.I).arg) * Complex.I = ↑x + ↑y * Complex.I<GOAL>(fun p => (p.1 * cos p.2, p.1 * sin p.2)) ((fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg)) (x, y)) = (x, y)
<GOAL>ContinuousOn ↑{ toFun := fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg), invFun := fun p => (p.1 * cos p.2, p.1 * sin p.2), source := {q | 0 < q.1} ∪ {q | q.2 ≠ 0}, target := Ioi 0 ×ˢ Ioo (-π) π, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ } { toFun := fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg), invFun := fun p => (p.1 * cos p.2, p.1 * sin p.2), source := {q | 0 < q.1} ∪ {q | q.2 ≠ 0}, target := Ioi 0 ×ˢ Ioo (-π) π, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.source
<GOAL>ContinuousOn (fun x => (Complex.equivRealProd.symm x).arg) { toFun := fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg), invFun := fun p => (p.1 * cos p.2, p.1 * sin p.2), source := {q | 0 < q.1} ∪ {q | q.2 ≠ 0}, target := Ioi 0 ×ˢ Ioo (-π) π, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.source
<VAR>A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane<GOAL>ContinuousOn (fun x => (Complex.equivRealProd.symm x).arg) { toFun := fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg), invFun := fun p => (p.1 * cos p.2, p.1 * sin p.2), source := {q | 0 < q.1} ∪ {q | q.2 ≠ 0}, target := Ioi 0 ×ˢ Ioo (-π) π, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.source
<VAR>A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane<VAR>z : ℂ<VAR>hz : z ∈ Complex.slitPlane<GOAL>ContinuousWithinAt Complex.arg Complex.slitPlane z
<VAR>A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane<GOAL>ContinuousOn ⇑Complex.equivRealProd.symm { toFun := fun q => (√(q.1 ^ 2 + q.2 ^ 2), (Complex.equivRealProd.symm q).arg), invFun := fun p => (p.1 * cos p.2, p.1 * sin p.2), source := {q | 0 < q.1} ∪ {q | q.2 ≠ 0}, target := Ioi 0 ×ˢ Ioo (-π) π, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.source
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<GOAL>EMetric.diam ((convexHull ℝ) s) = EMetric.diam s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>y : E<VAR>hy : y ∈ (convexHull ℝ) s<GOAL>edist x y ≤ EMetric.diam s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>y : E<VAR>hy : y ∈ (convexHull ℝ) s<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>y' : E<VAR>hy' : y' ∈ s<VAR>H : dist x y ≤ dist x' y'<GOAL>edist x y ≤ EMetric.diam s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>y : E<VAR>hy : y ∈ (convexHull ℝ) s<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>y' : E<VAR>hy' : y' ∈ s<VAR>H : dist x y ≤ dist x' y'<GOAL>ENNReal.ofReal (dist x y) ≤ EMetric.diam s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>y : E<VAR>hy : y ∈ (convexHull ℝ) s<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>y' : E<VAR>hy' : y' ∈ s<VAR>H : dist x y ≤ dist x' y'<GOAL>ENNReal.ofReal (dist x' y') ≤ EMetric.diam s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s✝ t s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull ℝ) s<VAR>y : E<VAR>hy : y ∈ (convexHull ℝ) s<VAR>x' : E<VAR>hx' : x' ∈ s<VAR>y' : E<VAR>hy' : y' ∈ s<VAR>H : dist x y ≤ dist x' y'<GOAL>edist x' y' ≤ EMetric.diam s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G✝ : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>G : Type u_9<VAR>inst✝ : LinearOrderedAddCommGroup G<VAR>f : ι → G<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>|∑ i ∈ s, f i| = ∑ i ∈ s, f i
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁷ : CommRing P<VAR>inst✝⁶ : Algebra R P<VAR>loc : IsLocalization S P<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field K'<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I✝ J : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>I : Ideal R<GOAL>↑I = 1 ↔ I = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α → β<VAR>hf : ∀ i ∈ s, Integrable (f i) μ<GOAL>Integrable (fun a => ∑ i ∈ s, f i a) μ
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>a₁ a₂ : Fin n<VAR>ha : ⟨a₁, a₂⟩ ∈ ↑(finPairsLT n)<VAR>b₁ b₂ : Fin n<VAR>hb : ⟨b₁, b₂⟩ ∈ ↑(finPairsLT n)<VAR>h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩<GOAL>⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>a₁ a₂ : Fin n<VAR>ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst<VAR>b₁ b₂ : Fin n<VAR>hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst<VAR>h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩<GOAL>⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>a₁ a₂ : Fin n<VAR>ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst<VAR>b₁ b₂ : Fin n<VAR>hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst<VAR>h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩<VAR>this : ¬b₁ < b₂<GOAL>⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>a₁ a₂ b₁ b₂ : Fin n<VAR>ha : b₁ < b₂<VAR>hb : b₂ < b₁<VAR>this : b₂ ≤ b₁<VAR>h✝¹ : f b₁ < f b₂<VAR>h✝ : f b₁ ≤ f b₂<VAR>h : a₁ = b₂ ∧ a₂ = b₁<GOAL>b₂ = b₁ ∧ b₁ = b₂
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>a₁ a₂ b₁ b₂ : Fin n<VAR>ha : b₁ < b₂<VAR>hb : b₂ < b₁<VAR>this : b₂ ≤ b₁<VAR>h✝¹ : f b₂ ≤ f b₁<VAR>h✝ : f b₂ < f b₁<VAR>h : a₂ = b₁ ∧ a₁ = b₂<GOAL>b₂ = b₁ ∧ b₁ = b₂
<VAR>α✝ : Type u_1<VAR>l₁ l₂ : List α✝<VAR>x✝ : l₁.reverse <:+ l₂.reverse<VAR>r : List α✝<VAR>e : r ++ l₁.reverse = l₂.reverse<GOAL>l₁ ++ r.reverse = l₂
<VAR>α✝ : Type u_1<VAR>l₁ l₂ : List α✝<VAR>x✝ : l₁ <+: l₂<VAR>r : List α✝<VAR>e : l₁ ++ r = l₂<GOAL>r.reverse ++ l₁.reverse = l₂.reverse
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<GOAL>((leftRegular G ⊗ X).ρ g ≫ fun g => (g.1, X.ρ g.1⁻¹ g.2)) = (fun g => (g.1, X.ρ g.1⁻¹ g.2)) ≫ (leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>((leftRegular G ⊗ X).ρ g ≫ fun g => (g.1, X.ρ g.1⁻¹ g.2)) (x₁, x₂) = ((fun g => (g.1, X.ρ g.1⁻¹ g.2)) ≫ (leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g) (x₁, x₂)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>(((leftRegular G ⊗ X).ρ g ≫ fun g => (g.1, X.ρ g.1⁻¹ g.2)) (x₁, x₂)).2 = (((fun g => (g.1, X.ρ g.1⁻¹ g.2)) ≫ (leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g) (x₁, x₂)).2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>(X.ρ (g * x₁)⁻¹ * X.ρ g) x₂ = X.ρ (x₁, x₂).1⁻¹ (x₁, x₂).2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : G<GOAL>((leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g ≫ fun g => (g.1, X.ρ g.1 g.2)) = (fun g => (g.1, X.ρ g.1 g.2)) ≫ (leftRegular G ⊗ X).ρ g
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>((leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g ≫ fun g => (g.1, X.ρ g.1 g.2)) (x₁, x₂) = ((fun g => (g.1, X.ρ g.1 g.2)) ≫ (leftRegular G ⊗ X).ρ g) (x₁, x₂)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>(((leftRegular G ⊗ { V := X.V, ρ := 1 }).ρ g ≫ fun g => (g.1, X.ρ g.1 g.2)) (x₁, x₂)).2 = (((fun g => (g.1, X.ρ g.1 g.2)) ≫ (leftRegular G ⊗ X).ρ g) (x₁, x₂)).2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>((((leftRegular G).ρ g ⊗ { V := X.V, ρ := 1 }.ρ g) ≫ fun g => (g.1, X.ρ g.1 g.2)) (x₁, x₂)).2 = (((fun g => (g.1, X.ρ g.1 g.2)) ≫ ((leftRegular G).ρ g ⊗ X.ρ g)) (x₁, x₂)).2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>X.ρ ((leftRegular G).ρ g x₁) x₂ = X.ρ g (X.ρ x₁ x₂)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>X.ρ (g * x₁) x₂ = X.ρ g (X.ρ x₁ x₂)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g x₁ : G<VAR>x₂ : X.V<GOAL>(X.ρ g * X.ρ x₁) x₂ = X.ρ g (X.ρ x₁ x₂)
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<GOAL>({ hom := fun g => (g.1, X.ρ g.1⁻¹ g.2), comm := ⋯ } ≫ { hom := fun g => (g.1, X.ρ g.1 g.2), comm := ⋯ }).hom = (𝟙 (leftRegular G ⊗ X)).hom
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>x : (leftRegular G ⊗ X).V<GOAL>({ hom := fun g => (g.1, X.ρ g.1⁻¹ g.2), comm := ⋯ } ≫ { hom := fun g => (g.1, X.ρ g.1 g.2), comm := ⋯ }).hom x = (𝟙 (leftRegular G ⊗ X)).hom x
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>x : (leftRegular G ⊗ X).V<GOAL>(({ hom := fun g => (g.1, X.ρ g.1⁻¹ g.2), comm := ⋯ } ≫ { hom := fun g => (g.1, X.ρ g.1 g.2), comm := ⋯ }).hom x).2 = ((𝟙 (leftRegular G ⊗ X)).hom x).2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>x : (leftRegular G ⊗ X).V<GOAL>(X.ρ x.1 * X.ρ x.1⁻¹) x.2 = x.2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<GOAL>({ hom := fun g => (g.1, X.ρ g.1 g.2), comm := ⋯ } ≫ { hom := fun g => (g.1, X.ρ g.1⁻¹ g.2), comm := ⋯ }).hom = (𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })).hom
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>x : (leftRegular G ⊗ { V := X.V, ρ := 1 }).V<GOAL>({ hom := fun g => (g.1, X.ρ g.1 g.2), comm := ⋯ } ≫ { hom := fun g => (g.1, X.ρ g.1⁻¹ g.2), comm := ⋯ }).hom x = (𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })).hom x
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>x : (leftRegular G ⊗ { V := X.V, ρ := 1 }).V<GOAL>(({ hom := fun g => (g.1, X.ρ g.1 g.2), comm := ⋯ } ≫ { hom := fun g => (g.1, X.ρ g.1⁻¹ g.2), comm := ⋯ }).hom x).2 = ((𝟙 (leftRegular G ⊗ { V := X.V, ρ := 1 })).hom x).2
<VAR>V : Type (u + 1)<VAR>inst✝¹ : LargeCategory V<VAR>G✝ : MonCat<VAR>G : Type u<VAR>inst✝ : Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>x : (leftRegular G ⊗ { V := X.V, ρ := 1 }).V<GOAL>(X.ρ x.1⁻¹ * X.ρ x.1) x.2 = x.2
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<GOAL>StrictAntiOn (deriv f) S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>toSubmodule S * toSubmodule S = toSubmodule S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>toSubmodule S * toSubmodule S ≤ toSubmodule S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>toSubmodule S ≤ toSubmodule S * toSubmodule S
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b : α<GOAL>|a| = |a - b + b|
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ ∅ ⊆ ⋃ x ∈ t, closedBall x ε<GOAL>∃ t ⊆ ∅, t.Countable ∧ ∅ ⊆ closure t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<VAR>T : ℕ → Set α<VAR>hTc : ∀ (n : ℕ), (T n).Countable<VAR>hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹<VAR>f : ℝ≥0∞ → α → α<VAR>hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s<VAR>hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<VAR>T : ℕ → Set α<VAR>hTc : ∀ (n : ℕ), (T n).Countable<VAR>hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹<VAR>f : ℝ≥0∞ → α → α<VAR>hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s<VAR>hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)<GOAL>s ⊆ closure (⋃ n, f (↑n)⁻¹ '' T n)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x✝ y z : α<VAR>ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<VAR>T : ℕ → Set α<VAR>hTc : ∀ (n : ℕ), (T n).Countable<VAR>hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹<VAR>f : ℝ≥0∞ → α → α<VAR>hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s<VAR>hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)<VAR>x : α<VAR>hx : x ∈ s<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<GOAL>∃ y ∈ ⋃ n, f (↑n)⁻¹ '' T n, edist x y < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x✝ y z : α<VAR>ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<VAR>T : ℕ → Set α<VAR>hTc : ∀ (n : ℕ), (T n).Countable<VAR>hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹<VAR>f : ℝ≥0∞ → α → α<VAR>hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s<VAR>hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)<VAR>x : α<VAR>hx : x ∈ s<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < ε / 2<GOAL>∃ y ∈ ⋃ n, f (↑n)⁻¹ '' T n, edist x y < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x✝ y✝ z : α<VAR>ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<VAR>T : ℕ → Set α<VAR>hTc : ∀ (n : ℕ), (T n).Countable<VAR>hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹<VAR>f : ℝ≥0∞ → α → α<VAR>hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s<VAR>hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)<VAR>x : α<VAR>hx : x ∈ s<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < ε / 2<VAR>y : α<VAR>hyn : y ∈ T n<VAR>hyx : x ∈ closedBall y (↑n)⁻¹<GOAL>∃ y ∈ ⋃ n, f (↑n)⁻¹ '' T n, edist x y < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x✝ y✝ z : α<VAR>ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ s<VAR>T : ℕ → Set α<VAR>hTc : ∀ (n : ℕ), (T n).Countable<VAR>hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹<VAR>f : ℝ≥0∞ → α → α<VAR>hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s<VAR>hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)<VAR>x : α<VAR>hx : x ∈ s<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < ε / 2<VAR>y : α<VAR>hyn : y ∈ T n<VAR>hyx : x ∈ closedBall y (↑n)⁻¹<GOAL>edist x (f (↑n)⁻¹ y) < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>ht : IntegrableOn f t μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>ht : IntegrableOn f t μ<VAR>H : IntegrableOn f (s ∪ t) μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>ht : IntegrableOn f t μ<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>f' : X → E := AEStronglyMeasurable.mk f ⋯<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : orderOf a ^ 2 ∣ n<GOAL>a • approxOrderOf A n δ = approxOrderOf A n δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : orderOf a ^ 2 ∣ n<GOAL>⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n<GOAL>⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n<VAR>f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b => ⟨a * ↑b, ⋯⟩<GOAL>⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ