ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>max (Ordinal.lsub fun i => ((powHalf 1).moveLeft i).birthday) (Ordinal.lsub fun i => ((powHalf 1).moveRight i).birthday) = 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : DivInvMonoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹<VAR>a b : G<GOAL>f (a / b) = f a / f b
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>cgf X μ 0 = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>x \ yᶜ = x ⊓ y
<VAR>x y z : ℂ<GOAL>cos z = cos ↑z.re * cosh ↑z.im - sin ↑z.re * sinh ↑z.im * I
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>m n : ℕ<VAR>s : Simplex k P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).reindex e.symm = s
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>g : N →* P<VAR>f : G →* N<GOAL>map g f.range = (g.comp f).range
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>g : N →* P<VAR>f : G →* N<GOAL>map g (map f ⊤) = map (g.comp f) ⊤
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIocDiv hp a (b - c) = toIocDiv hp (a + c) b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>x : N ⊗[R] M<GOAL>(rTensor M id) x = x
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x y : X<VAR>hoxy : ι R x = ι R y<GOAL>¬x = y → False
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n✝ n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>inst✝ : CharZero K<GOAL>minpoly ℤ μ ∣ cyclotomic n ℤ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n✝ n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>inst✝ : CharZero K<GOAL>(aeval μ) (cyclotomic n ℤ) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n : ℕ<VAR>hn : ¬restrict s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤ restrict 0 (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<GOAL>1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) + 1) < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i n.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>n : ℕ<VAR>hn : ¬restrict s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤ restrict 0 (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<GOAL>1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) + 1) < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²⁴ : Semiring R₁<VAR>inst✝²³ : Semiring R₂<VAR>inst✝²² : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>inst✝²¹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²⁰ : RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>inst✝¹⁹ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝¹⁸ : RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>inst✝¹⁷ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝¹⁶ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>inst✝¹³ : TopologicalSpace M₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹¹ : TopologicalSpace M'₁<VAR>inst✝¹⁰ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝⁹ : TopologicalSpace M₂<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁷ : TopologicalSpace M₃<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁵ : TopologicalSpace M₄<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : Module R₁ M'₁<VAR>inst✝¹ : Module R₂ M₂<VAR>inst✝ : Module R₃ M₃<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₂<GOAL>(⇑e ∘ ⇑e.symm) x = id x
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ✝ : IsPrimitiveRoot ζ ↑p<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))<GOAL>hζ✝.toInteger - 1 ∣ ↑↑p
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>s : Set (Ideal S)<GOAL>⨅ I ∈ s, comap f I = ⨅ I ∈ comap f '' s, I
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>(‖x.1‖ ^ 2 + ‖x.2‖ ^ 2) ^ (1 / ↑2) = (‖x.1‖ ^ 2 + ‖x.2‖ ^ 2) ^ (1 / 2)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>r ε : ℝ<VAR>L : F<VAR>x y z : ℝ<VAR>hy : y ∈ Icc x (x + r / 2)<VAR>hz : z ∈ Icc x (x + r / 2)<VAR>r' : ℝ<VAR>r'mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<GOAL>‖f z - f y - (z - y) • L‖ ≤ ε * r
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>r ε : ℝ<VAR>L : F<VAR>x y z : ℝ<VAR>hy : y ∈ Icc x (x + r / 2)<VAR>hz : z ∈ Icc x (x + r / 2)<VAR>r' : ℝ<VAR>r'mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<VAR>A : x + r / 2 ≤ x + r'<GOAL>‖f z - f y - (z - y) • L‖ ≤ ε * r
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>h : (g.comp f).Finite<VAR>this✝³ : Algebra A B := f.toAlgebra<VAR>this✝² : Algebra B C := g.toAlgebra<VAR>this✝¹ : Algebra A C := (g.comp f).toAlgebra<VAR>this✝ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C<VAR>this : Module.Finite A C := h<GOAL>g.Finite
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>x : L<VAR>hx : x ∈ LieAlgebra.center R L<VAR>y : L<GOAL>Commute ((toEnd R L M) x) ((toEnd R L M) y)
<VAR>x✝² x✝¹ : Scheme<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>IsPreimmersion x✝ ↔ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Embedding) ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x) x✝
<VAR>x✝² x✝¹ : Scheme<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>(Embedding ⇑x✝.val.base ∧ ∀ (x : ↑↑x✝².toPresheafedSpace), Function.Surjective ⇑(Scheme.Hom.stalkMap x✝ x)) ↔ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Embedding) ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x) x✝
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>f : M ≃[L] N<GOAL>f.symm.toHom.comp f.toHom = Hom.id L M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>n i j : ℕ<VAR>hxn : (toEnd R L M) x ^ n = 0<VAR>hIM : lowerCentralSeries R L M i ≤ I.lcs M j<GOAL>lowerCentralSeries R L M (i + n) ≤ I.lcs M (j + 1)
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>n i j : ℕ<VAR>hxn : (toEnd R L M) x ^ n = 0<VAR>hIM : lowerCentralSeries R L M i ≤ I.lcs M j<GOAL>∀ (l : ℕ), ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<VAR>hs : s ∈ 𝔖<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>{g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ 𝓝 f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<VAR>hs : s ∈ 𝔖<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>{g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : n.Coprime (orderOf x)<VAR>h0 : ¬orderOf x = 0<VAR>h1 : ¬orderOf x = 1<GOAL>∃ m, (x ^ n) ^ m = x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m✝ : ℕ<VAR>h✝ : n.Coprime (orderOf x)<VAR>h0 : ¬orderOf x = 0<VAR>h1 : ¬orderOf x = 1<VAR>m : ℕ<VAR>h : n * m % orderOf x = 1<GOAL>∃ m, (x ^ n) ^ m = x
<VAR>a b c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : b ∣ a<VAR>hb : b ≠ 0<VAR>d : ℕ<GOAL>c = a / b * d ↔ b * c = a * d
<VAR>a b c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : b ∣ a<VAR>hb : b ≠ 0<VAR>d : ℕ<VAR>this : b ∣ d * a<GOAL>c = a / b * d ↔ b * c = a * d
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>QuasiMeasurePreserving (fun x => r • x) μ μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>map (fun x => r • x) μ ≪ μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>b : ℤ<GOAL>⌈↑(b - 1)⌉ ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>b : ℤ<GOAL>b - 1 ≤ b
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (aeval (root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (aeval pb.gen) g = 0<VAR>x : AdjoinRoot g<GOAL>(pb.lift (root g) h₁) ((liftHom g pb.gen h₂) x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (aeval (root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (aeval pb.gen) g = 0<VAR>p✝ : R[X]<GOAL>(pb.lift (root g) h₁) ((liftHom g pb.gen h₂) ((mk g) p✝)) = (mk g) p✝
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (aeval (root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (aeval pb.gen) g = 0<VAR>x : S<VAR>a✝ : Nontrivial S<GOAL>(liftHom g pb.gen h₂) ((pb.lift (root g) h₁) x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>g : R[X]<VAR>pb : PowerBasis R S<VAR>h₁ : (aeval (root g)) (minpoly R pb.gen) = 0<VAR>h₂ : (aeval pb.gen) g = 0<VAR>a✝ : Nontrivial S<VAR>f : R[X]<VAR>_hf : f.natDegree < pb.dim<GOAL>(liftHom g pb.gen h₂) ((pb.lift (root g) h₁) ((aeval pb.gen) f)) = (aeval pb.gen) f
<VAR>b : EReal<VAR>h : 0 < b<VAR>h' : b ≠ ⊤<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<GOAL>(fun a => a / b) a < (fun a => a / b) a'
<VAR>b : EReal<VAR>h : 0 < b<VAR>h' : b ≠ ⊤<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<GOAL>a / b ≠ a' / b
<VAR>b : EReal<VAR>h : 0 < b<VAR>h' : b ≠ ⊤<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<VAR>hyp : a / b = a' / b<GOAL>False
<VAR>b : EReal<VAR>h : 0 < b<VAR>h' : b ≠ ⊤<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<VAR>hyp : a / b = a' / b<GOAL>a = a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (thickening R s) ≠ ⊤<VAR>h's : IsClosed s<GOAL>Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (thickening R s) ≠ ⊤<VAR>h's : IsClosed s<GOAL>s = closure s
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>φ : K →+* ℂ<VAR>h : (mk φ).IsComplex<GOAL>¬ComplexEmbedding.IsReal φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>((κ.comapRight hf) a) t = (κ a) (f '' t)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>b : Bicone f<VAR>i : b.IsBilimit<VAR>as✝ : J<GOAL>(∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as✝ } = 𝟙 b.pt ≫ b.toCone.π.app { as := as✝ }
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝ : Category.{v₁, u₂} ℰ<VAR>A : C ⥤ ℰ<VAR>P₁ P₂ : Cᵒᵖ ⥤ Type v₁<VAR>α : P₁ ⟶ P₂<VAR>j : P₁.Elementsᵒᵖ<VAR>T : Cᵒᵖ<VAR>f : ((functorToRepresentables P₁).obj j).obj T<GOAL>((coconeOfRepresentable P₁).ι.app j ≫ α).app T f = ((coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)).app T f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : IsOpenMap f<GOAL>IsOpen (range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : IsOpenMap f<GOAL>IsOpen (f '' univ)
<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>hc : 0 < c<GOAL>b / c < a ↔ b < c * a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Monoid R<VAR>inst✝ : StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>n : ℕ<GOAL>IsSelfAdjoint (x ^ n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>P x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>z : α<VAR>hz : z ∈ s<GOAL>∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>z : α<VAR>hz : z ∈ s<VAR>a : α<VAR>ha : P z a<VAR>h'a : a ∈ s<GOAL>P z a ∧ P a z
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<GOAL>Splits j (map i f) ↔ Splits (j.comp i) f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L := compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>f' : E.functor.obj X ⟶ E.functor.obj Y<GOAL>∃ φ, e.inv.app X ≫ f' ≫ e.hom.app Y = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L := compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>g : X ⟶ Y<GOAL>∃ φ, e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L := compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>g : W.LeftFraction X Y<GOAL>∃ φ, e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk g) ≫ e.hom.app Y = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L := compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W<VAR>g : W.LeftFraction X Y<GOAL>e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk g) ≫ e.hom.app Y = g.map L ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ ↔ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ
<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>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>f : α →₀ M<VAR>inst✝ : CommMonoid N<VAR>g : α → M → N<GOAL>(filter p f).prod g * (filter (fun a => ¬p a) f).prod g = f.prod g
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>s t : ℝ<VAR>hs : 0 ≤ s<VAR>ht : 0 ≤ t<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ (Icc 0 s)<VAR>φst : φ '' Icc 0 s = Icc 0 t<VAR>hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)<VAR>hf : HasUnitSpeedOn f (φ '' Icc 0 s)<GOAL>EqOn φ id (Icc 0 s)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>s t : ℝ<VAR>hs : 0 ≤ s<VAR>ht : 0 ≤ t<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ (Icc 0 s)<VAR>φst : φ '' Icc 0 s = Icc 0 t<VAR>hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)<VAR>hf : HasUnitSpeedOn f (φ '' Icc 0 s)<GOAL>id = fun y => y - 0 + φ 0