ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝² : LinearOrder γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f : α → γ<GOAL>(∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
<VAR>x y : ℂ<GOAL>cosh x - sinh x = cexp (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f✝ f : α × β → StieltjesFunction<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫ (b : β), ↑(f (a, b)) x ∂ν a = ((κ a) (univ ×ˢ Iic x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsUpperSet α<VAR>s : Set α<GOAL>IsClosed s ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b a : α<GOAL>∂ (￢￢a) = ∂ (￢a)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>X : Type u_4<VAR>inst✝¹² : Monoid M<VAR>S : Submonoid M<VAR>inst✝¹¹ : OreSet S<VAR>inst✝¹⁰ : MulAction M X<VAR>inst✝⁹ : SMul R X<VAR>inst✝⁸ : SMul R M<VAR>inst✝⁷ : IsScalarTower R M M<VAR>inst✝⁶ : IsScalarTower R M X<VAR>inst✝⁵ : SMul R' X<VAR>inst✝⁴ : SMul R' M<VAR>inst✝³ : IsScalarTower R' M M<VAR>inst✝² : IsScalarTower R' M X<VAR>inst✝¹ : SMul R R'<VAR>inst✝ : IsScalarTower R R' M<VAR>r : R<VAR>x : X<GOAL>r • (x /ₒ 1) = r • x /ₒ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>h : s.Finite<VAR>h' : s ∈ f<GOAL>∃ x ∈ s, f = pure x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>h : s.Finite<VAR>h' : ⋃ x ∈ s, {x} ∈ f<GOAL>∃ x ∈ s, f = pure x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>h : s.Finite<VAR>h' : ⋃ x ∈ s, {x} ∈ f<VAR>a : α<VAR>has : a ∈ s<VAR>haf : {a} ∈ f<GOAL>∃ x ∈ s, f = pure x
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>I : Type u_4<VAR>inst✝¹ : AddMonoid I<VAR>c : ComplexShape I<VAR>inst✝ : c.TensorSigns<GOAL>c.ε 0 = 1
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>rdropWhile p [x] = if p x = true then [] else [x]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≼i s<VAR>a✝ : α<VAR>h : Acc r a✝<VAR>a : α<VAR>x✝ : ∀ (y : α), r y a → Acc r y<VAR>ha : ∀ (y : α), r y a → Acc s (f y)<VAR>b : β<VAR>hb : s b (f a)<GOAL>Acc s b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≼i s<VAR>a✝ : α<VAR>h : Acc r a✝<VAR>a : α<VAR>x✝ : ∀ (y : α), r y a → Acc r y<VAR>ha : ∀ (y : α), r y a → Acc s (f y)<VAR>a' : α<VAR>hb : s (f a') (f a)<GOAL>Acc s (f a')
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>he : e ∈ M.closure X<GOAL>M.closure (insert e X) = M.closure 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>f : α →. β<VAR>x : α<GOAL>x ∈ f.Dom ↔ ∃ y, y ∈ f x
<VAR>θ ψ : Angle<VAR>h : 2 • θ = 2 • ψ<GOAL>|θ.sin| = |ψ.sin|
<VAR>θ ψ : Angle<VAR>h : θ = ψ ∨ θ = ψ + ↑π<GOAL>|θ.sin| = |ψ.sin|
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hfg : f =ᶠ[𝓝[≠] x] g<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1) • g z) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hfg : f =ᶠ[𝓝[≠] x] g<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>this : AnalyticAt 𝕜 (fun z => z - x) x<GOAL>AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1) • g z) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hfg : f =ᶠ[𝓝[≠] x] g<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>this : AnalyticAt 𝕜 (fun z => z - x) x<GOAL>(fun x_1 => (x_1 - x) • (x_1 - x) ^ m • f x_1) =ᶠ[𝓝 x] fun z => (z - x) ^ (m + 1) • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>this : AnalyticAt 𝕜 (fun z => z - x) x<GOAL>(fun x_1 => (x_1 - x) • (x_1 - x) ^ m • f x_1) =ᶠ[𝓝 x] fun z => (z - x) ^ (m + 1) • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>this : AnalyticAt 𝕜 (fun z => z - x) x<VAR>z : 𝕜<VAR>hz : z ∈ {x}ᶜ → f z = g z<GOAL>(z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>m : ℕ<VAR>z : 𝕜<VAR>hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, x ∈ {z}ᶜ → f x = g x<VAR>hf : AnalyticAt 𝕜 (fun z_1 => (z_1 - z) ^ m • f z_1) z<VAR>this : AnalyticAt 𝕜 (fun z_1 => z_1 - z) z<VAR>hz : z ∈ {z}ᶜ → f z = g z<GOAL>(z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = g x_1<VAR>m : ℕ<VAR>hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x<VAR>this : AnalyticAt 𝕜 (fun z => z - x) x<VAR>z : 𝕜<VAR>hz : z ∈ {x}ᶜ → f z = g z<VAR>hn : z ≠ x<GOAL>(z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>s : Set M<VAR>hs : s ⊆ ↑M'<VAR>hs' : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set M<VAR>ht : LinearIndependent (ι := ↑t) R (Submodule.Quotient.mk ∘ Subtype.val)<GOAL>LinearIndependent (ι := ↑(s ∪ t)) R Subtype.val
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'✝<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'✝<VAR>inst✝ : Module R M₁<VAR>M' : Submodule R M<VAR>s : Set M<VAR>hs : s ⊆ ↑M'<VAR>hs' : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set M<VAR>ht : LinearIndependent (ι := ↑t) R (Submodule.Quotient.mk ∘ Subtype.val)<GOAL>range (Sum.elim (fun x => ↑((s.embeddingOfSubset (↑M') hs) x)) Subtype.val) = s ∪ t
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>a + star a = 2 * ↑a.re
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>H K : Subgroup G<GOAL>closure ↑H ⊔ closure ↑K ≤ H ⊔ K
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑S<VAR>x : ↑R<GOAL>(((stalkIso (↑R) ((PrimeSpectrum.comap f) p)).inv ≫ PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p) ≫ (stalkIso (↑S) p).hom) ((algebraMap (↑R) (Localization.AtPrime ((PrimeSpectrum.comap f) p).asIdeal)) x) = (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) (f x)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑S<VAR>x : ↑R<GOAL>((localizationToStalk (↑R) ((PrimeSpectrum.comap f) p) ≫ PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p) ≫ stalkToFiberRingHom (↑S) p) ((algebraMap (↑R) (Localization.AtPrime ((PrimeSpectrum.comap f) p).asIdeal)) x) = (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) (f x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : DecidableEq A<VAR>inst✝ : One B<VAR>a : A<VAR>b b' : B<VAR>hb : b ≠ 1<VAR>hb' : b' ≠ 1<VAR>i j : A<GOAL>Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α✝ : Type u_12<VAR>β : Type u_13<VAR>inst✝⁴ : DecidableEq o<VAR>inst✝³ : Zero α✝<VAR>inst✝² : Zero β<VAR>α : Type u_14<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>(blockDiagonal' M)ᴴ = blockDiagonal' fun k => (M k)ᴴ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α✝ : Type u_12<VAR>β : Type u_13<VAR>inst✝⁴ : DecidableEq o<VAR>inst✝³ : Zero α✝<VAR>inst✝² : Zero β<VAR>α : Type u_14<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>(blockDiagonal' fun k => (M k)ᵀ).map star = blockDiagonal' fun k => (M k)ᵀ.map star
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<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>x : M<VAR>h : I.IsInteriorPoint x<GOAL>range ↑I ∈ 𝓝 (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<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>x : M<VAR>h : I.IsInteriorPoint x<GOAL>∃ t ⊆ range ↑I, IsOpen t ∧ ↑(extChartAt I x) x ∈ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MulHomClass F α β<VAR>m : F<VAR>s✝ t✝ : Set α<VAR>s t : Set β<VAR>hs : s ⊆ range ⇑m<VAR>ht : t ⊆ range ⇑m<VAR>a : α<VAR>ha : m a ∈ s<VAR>b : α<VAR>hb : m b ∈ t<GOAL>(fun x x_1 => x * x_1) (m a) (m b) ∈ range ⇑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>e : ι' ≃ ι<VAR>m : ι → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum (m ∘ ⇑e)) s = (sum m) 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 : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>f : A →ₐ[S] B<VAR>s : A → A → Prop<VAR>w : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>x : A<GOAL>((liftAlgHom S) ⟨f, w⟩) ((mkAlgHom S s) x) = f x
<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 : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>f : A →ₐ[S] B<VAR>s : A → A → Prop<VAR>w : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>x : A<GOAL>({ toFun := fun f' => { toFun := fun x => Quot.lift ⇑↑f' ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }, invFun := fun F => ⟨F.comp { toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨f, w⟩) ({ toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } x) = f x
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<GOAL>qrSign m n ^ 2 = 1
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁷ : Field 𝕜<VAR>inst✝¹⁶ : CharZero 𝕜<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup M<VAR>inst✝¹³ : Algebra 𝕜 R<VAR>inst✝¹² : Module 𝕜 M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module Rᵐᵒᵖ M<VAR>inst✝⁹ : IsCentralScalar R M<VAR>inst✝⁸ : IsScalarTower 𝕜 R M<VAR>inst✝⁷ : TopologicalSpace R<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalRing R<VAR>inst✝⁴ : TopologicalAddGroup M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝¹ : T2Space R<VAR>inst✝ : T2Space M<VAR>x : tsze R M<GOAL>(exp 𝕜 x).fst = exp 𝕜 x.fst
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h1 : 0 < a<VAR>h2 : a ≤ 1<GOAL>1 ≤ 1 / a
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>cons g w hmw hgr = (of i) g • w
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>CoprodI.of ((φ i) (cons g w hmw hgr).head) • (cons g w hmw hgr).toWord = CoprodI.of ((φ i) ((of i) g • w).head) • ((of i) g • w).toWord
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>∫ (x : E) in f '' s, g x ∂μ = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>∫ (x : ↑s), g (s.restrict f x) ∂Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|) = ∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>∫ (x : ↑s), (g ∘ f) ↑x ∂Measure.comap Subtype.val (μ.withDensity fun x => ↑|(f' x).det|.toNNReal) = ∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<GOAL>∫ (x : E) in s, |(f' x).det|.toNNReal • (g ∘ f) x ∂μ = ∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : E → F<VAR>x : E<GOAL>|(f' x).det|.toNNReal • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsBounded s<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsBounded s<VAR>r : ℝ<VAR>hr : s ⊆ Metric.ball 0 r<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsBounded s<VAR>r : ℝ<VAR>hr : s ⊆ Metric.ball 0 r<GOAL>∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsBounded s<VAR>r : ℝ<VAR>hr : s ⊆ (normSeminorm 𝕜 E).ball 0 r<GOAL>∀ (i : ℝ), 0 < i → Absorbs 𝕜 ((normSeminorm 𝕜 E).ball 0 i) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁✝ μ₂✝ μ₃ ν✝ ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>μ₁ μ₂ ν : Measure α<GOAL>μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁✝ μ₂✝ μ₃ ν✝ ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>μ₁ μ₂ ν : Measure α<VAR>h : μ₁ + μ₂ ≪ ν<GOAL>μ₁ ≪ ν ∧ μ₂ ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁✝ μ₂✝ μ₃ ν✝ ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>μ₁ μ₂ ν : Measure α<VAR>h : μ₁ ≪ ν ∧ μ₂ ≪ ν<GOAL>ν + ν ≪ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t✝ s : Set α<VAR>v : ℕ → Set α<VAR>hv : s ⊆ ⋃ n, v n<VAR>h'v : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).card = s.card + t.card - (s ∩ t).card
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>h : 0 ≤ ε<VAR>y : α<GOAL>y ∈ EMetric.closedBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20707, u_1} C<VAR>inst✝¹ : Category.{?u.20711, u_2} D<VAR>inst✝ : Category.{?u.20715, u_3} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>adj : F ⊣ G<VAR>x : D ⥤ C<VAR>x✝ : E<GOAL>(𝟙 (x.obj (G.obj x✝)) ≫ x.map (adj.unit.app (G.obj x✝)) ≫ 𝟙 (x.obj (G.obj (F.obj (G.obj x✝))))) ≫ 𝟙 (x.obj (G.obj (F.obj (G.obj x✝)))) ≫ 𝟙 (x.obj (G.obj (F.obj (G.obj x✝)))) ≫ x.map (G.map (adj.counit.app x✝)) ≫ 𝟙 (x.obj (G.obj x✝)) = 𝟙 (x.obj (G.obj x✝))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20707, u_1} C<VAR>inst✝¹ : Category.{?u.20711, u_2} D<VAR>inst✝ : Category.{?u.20715, u_3} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>adj : F ⊣ G<VAR>x : E ⥤ C<VAR>x✝ : D<GOAL>(𝟙 (x.obj (F.obj x✝)) ≫ x.map (F.map (adj.unit.app x✝)) ≫ 𝟙 (x.obj (F.obj (G.obj (F.obj x✝))))) ≫ 𝟙 (x.obj (F.obj (G.obj (F.obj x✝)))) ≫ 𝟙 (x.obj (F.obj (G.obj (F.obj x✝)))) ≫ x.map (adj.counit.app (F.obj x✝)) ≫ 𝟙 (x.obj (F.obj x✝)) = 𝟙 (x.obj (F.obj x✝))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>x y : L<VAR>hx : IsAlgebraic K x<VAR>h_ev : (Polynomial.aeval y) (minpoly K x) = 0<GOAL>minpoly K y = minpoly K x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>x y : L<VAR>hx : IsAlgebraic K x<VAR>h_ev : (Polynomial.aeval y) (minpoly K x) = 0<VAR>hy : IsAlgebraic K y<GOAL>minpoly K y = minpoly K x
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : NormedGroup E<VAR>inst✝ : NormedGroup F<VAR>a b : E<VAR>h : ‖a / b‖ ≤ 0<GOAL>a = b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>thickening δ (thickening δ E)ᶜ ⊆ Eᶜ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>h : ¬hausdorffEdist s u = ⊤<GOAL>¬hausdorffEdist t u = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist t s ≠ ⊤<VAR>h : ¬hausdorffEdist s u = ⊤<GOAL>¬hausdorffEdist t u = ⊤
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>p : K[X]<VAR>hsplit : Splits (RingHom.id K) p<GOAL>p = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod
<VAR>R : Type u_1<VAR>inst✝¹ : AddMonoidWithOne R<VAR>inst✝ : CharZero R<VAR>n : ℕ<GOAL>↑n = 1 ↔ n = 1
<VAR>A : Type u_1<VAR>B✝ : Type u_2<VAR>inst✝⁴ : Field A<VAR>inst✝³ : Ring B✝<VAR>inst✝² : Algebra A B✝<VAR>x✝ : B✝<VAR>B : Type u_3<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>a : A<GOAL>minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (X + C a)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C✝ K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>C : X → ℝ≥0<VAR>t : X → Set X<VAR>htn : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)<GOAL>dimH (f '' s) ≤ dimH s / ↑r