ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>x : E<VAR>S : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection S<GOAL>‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ * ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ = ‖(orthogonalProjection S) x‖ * ‖(orthogonalProjection S) x‖ + ‖(orthogonalProjection Sᗮ) x‖ * ‖(orthogonalProjection Sᗮ) x‖
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.101327, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>S₁ S₂ : Split C<VAR>Φ : S₁ ⟶ S₂<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>(S₁.s.cofan (op [i])).inj (Splitting.IndexSet.id (op [i])) ≫ ((alternatingFaceMapComplex C).obj S₁.X).d i j ≫ ((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op [j])) = ((S₁.s.cofan (op [i])).inj (Splitting.IndexSet.id (op [i])) ≫ K[S₁.X].d i j ≫ S₁.s.πSummand (Splitting.IndexSet.id (op [j]))) ≫ Φ.f j
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.101327, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>S₁ S₂ : Split C<VAR>Φ : S₁ ⟶ S₂<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>(S₁.s.cofan (op [i])).inj (Splitting.IndexSet.id (op [i])) ≫ ((alternatingFaceMapComplex C).obj S₁.X).d i j ≫ ((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op [j])) = (S₁.s.cofan (op [i])).inj (Splitting.IndexSet.id (op [i])) ≫ K[S₁.X].d i j ≫ S₁.s.πSummand (Splitting.IndexSet.id (op [j])) ≫ Φ.f j
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.101327, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>S₁ S₂ : Split C<VAR>Φ : S₁ ⟶ S₂<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op [j])) = S₁.s.πSummand (Splitting.IndexSet.id (op [j])) ≫ Φ.f j
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.101327, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>S₁ S₂ : Split C<VAR>Φ : S₁ ⟶ S₂<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>∀ (A : Splitting.IndexSet (op [j])), (S₁.s.cofan (op [j])).inj A ≫ ((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op [j])) = (S₁.s.cofan (op [j])).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op [j])) ≫ Φ.f j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : Semiring R₁<VAR>inst✝¹⁷ : Semiring S₁<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : AddCommMonoid M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>inst✝¹⁰ : AddCommMonoid N₂<VAR>inst✝⁹ : Module R N₂<VAR>inst✝⁸ : Module S₁ N₂<VAR>inst✝⁷ : Module S₂ N₂<VAR>inst✝⁶ : SMulCommClass S₁ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ R N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂<GOAL>toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i => (stdBasis R₁ (fun x => R₁) i) 1) fun j => (stdBasis R₂ (fun x => R₂) j) 1) f) = f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : Semiring R₁<VAR>inst✝¹⁷ : Semiring S₁<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : AddCommMonoid M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>inst✝¹⁰ : AddCommMonoid N₂<VAR>inst✝⁹ : Module R N₂<VAR>inst✝⁸ : Module S₁ N₂<VAR>inst✝⁷ : Module S₂ N₂<VAR>inst✝⁶ : SMulCommClass S₁ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ R N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂<VAR>i : n<VAR>j : m<GOAL>((toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i => (stdBasis R₁ (fun x => R₁) i) 1) fun j => (stdBasis R₂ (fun x => R₂) j) 1) f)) ((Pi.basisFun R₁ n) i)) ((Pi.basisFun R₂ m) j) = (f ((Pi.basisFun R₁ n) i)) ((Pi.basisFun R₂ m) j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x✝ x : α<VAR>hx : x ∈ Icc a b<VAR>y : α<VAR>hy : y ∈ Icc a b<VAR>hxy : x < y<GOAL>projIcc a b h x < projIcc a b h y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>a : α<GOAL>insert a s ∪ t = s ∪ insert a t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>κ.compProdFun η a s = ∑' (n : ℕ), κ.compProdFun (η.seq n) a s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a = ∑' (n : ℕ), ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<VAR>this : ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a<GOAL>∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a = ∑' (n : ℕ), ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>hs : MeasurableSet s<VAR>this : ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a = ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a<GOAL>∀ (i : ℕ), AEMeasurable (fun b => ((η.seq i) (a, b)) {c | (b, c) ∈ s}) (κ a)
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>x : A<GOAL>x ∈ NonUnitalAlgebra.adjoin R (∅ ∪ star ∅) ↔ x = 0
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<VAR>r : F<GOAL>↑(C r) = HahnSeries.C r
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<VAR>r : F<GOAL>(ofPowerSeries ℤ F) ((PowerSeries.C F) r) = HahnSeries.C r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 0 s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>t • x ∈ s
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<GOAL>IsComplement {g} S ↔ S = univ
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>g : G<VAR>h : IsComplement {g} S<VAR>x : G<VAR>x✝ : x ∈ ⊤<GOAL>x ∈ S
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>x : G<VAR>x✝ : x ∈ ⊤<VAR>z : G<VAR>h : IsComplement {z} S<VAR>y : G<VAR>property✝ : y ∈ S<VAR>hy : (fun x => ↑x.1 * ↑x.2) (⟨z, ⋯⟩, ⟨y, property✝⟩) = z * x<GOAL>x ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<GOAL>μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ ⟂ₘ ν
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b c x✝¹ : R<VAR>x✝ : c ∣ 0<VAR>H : c ∣ x✝¹<GOAL>c ∣ gcd 0 x✝¹
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a✝ b✝ c a b : R<VAR>x✝ : a ≠ 0<VAR>IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a<VAR>ca : c ∣ a<VAR>cb : c ∣ b<GOAL>c ∣ gcd a b
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a✝ b✝ c a b : R<VAR>x✝ : a ≠ 0<VAR>IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a<VAR>ca : c ∣ a<VAR>cb : c ∣ b<GOAL>c ∣ gcd (b % a) a
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<GOAL>F.Initial
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<GOAL>∀ (d : D), IsCofiltered (CostructuredArrow F d)
<VAR>α : Type u_1<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ<VAR>h : (ENNReal.ofReal a).toReal = a<GOAL>0 ≤ (ENNReal.ofReal a).toReal
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<VAR>h : fract a = b<GOAL>0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a b : α<VAR>h₀ : 0 ≤ b<VAR>h₁ : b < 1<VAR>z : ℤ<VAR>hz : a - b = ↑z<GOAL>fract a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a b : α<VAR>h₀ : 0 ≤ b<VAR>h₁ : b < 1<VAR>z : ℤ<VAR>hz : a - b = ↑z<GOAL>a - b ≤ a ∧ a < a - b + 1
<VAR>x y a : ℝ<VAR>ha : 0 < a<GOAL>AntitoneOn (fun x => log x / x ^ a) {x | rexp (1 / a) ≤ x}
<VAR>x y a : ℝ<VAR>ha : 0 < a<GOAL>∀ ⦃a_1 : ℝ⦄, rexp (1 / a) ≤ a_1 → ∀ ⦃b : ℝ⦄, rexp (1 / a) ≤ b → a_1 ≤ b → log b / b ^ a ≤ log a_1 / a_1 ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<GOAL>log y / y ^ a ≤ log x / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<GOAL>log y / y ^ a ≤ log x / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<GOAL>log y / y ^ a ≤ log x / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<GOAL>log y / y ^ a ≤ log x / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>log y / y ^ a ≤ log x / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>log (y ^ 1) / y ^ a ≤ log x / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>log (y ^ 1) / y ^ a ≤ log (x ^ 1) / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>x ^ a ∈ {x | rexp 1 ≤ x}
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>y ^ a ∈ {x | rexp 1 ≤ x}
<VAR>x✝¹ y✝ a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hex : rexp (1 / a) ≤ x<VAR>y : ℝ<VAR>x✝ : rexp (1 / a) ≤ y<VAR>hxy : x ≤ y<VAR>x_pos : 0 < x<VAR>y_pos : 0 < y<VAR>x_nonneg : 0 ≤ x<VAR>y_nonneg : 0 ≤ y<GOAL>x ^ a ≤ y ^ a
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P<GOAL>midpoint ℝ p₁ p₂ ∈ perpBisector p₁ p₂
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>m n : ℤ<GOAL>bitwise or m n = m.lor n
<VAR>m n : ℕ<GOAL>Nat.bitwise (fun x y => !(x || !y)) m n = Nat.bitwise (fun a b => a && !b) n m
<VAR>m n : ℕ<GOAL>Nat.bitwise (fun x y => !(!x || y)) m n = Nat.bitwise (fun a b => a && !b) m n
<VAR>m n : ℕ<GOAL>Nat.bitwise (fun x y => !(!x || !y)) m n = m &&& n
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.95502, u_1} J<VAR>inst✝ : Category.{?u.96011, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>s : ↑(F.op ⋙ yoneda.obj X).sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ ↑s (op j') = ↑s (op j) ≫ 𝟙 X
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.95502, u_1} J<VAR>inst✝ : Category.{?u.96011, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>s : ↑(F.op ⋙ yoneda.obj X).sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ ↑s (op j') = ↑s (op j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.95502, u_1} J<VAR>inst✝ : Category.{?u.96011, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>τ : F ⟶ (const J).obj X<VAR>j j' : Jᵒᵖ<VAR>f : j ⟶ j'<GOAL>(F.op ⋙ yoneda.obj X).map f ((fun j => τ.app (unop j)) j) = (fun j => τ.app (unop j)) j'
<VAR>n r : ℕ<VAR>hr : r ≤ n / 2<GOAL>n.choose r ≤ n.choose (n / 2)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(nthRootsFinset n R).card = n
<VAR>r : List Char<VAR>it : Iterator<VAR>h : ValidFor [] r it<GOAL>ValidFor [] r it.prev
<VAR>r : List Char<VAR>it : Iterator<VAR>h : ValidFor [] r it<GOAL>ValidFor [] r { s := { data := r }, i := 0 }
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : PseudoEMetricSpace α✝<VAR>inst✝³ : PseudoEMetricSpace β✝<VAR>inst✝² : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : EMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<VAR>h : f x = f y<GOAL>x = y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>t✝ t₁ t₂ : TopologicalSpace α✝<VAR>t' : TopologicalSpace β✝<VAR>f : α✝ → β✝<VAR>g : β✝ → α✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>e : α ≃ β<VAR>t : TopologicalSpace α<VAR>U : Set β<GOAL>IsOpen U ↔ IsOpen U
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>t✝ t₁ t₂ : TopologicalSpace α✝<VAR>t' : TopologicalSpace β✝<VAR>f : α✝ → β✝<VAR>g : β✝ → α✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>e : α ≃ β<VAR>t : TopologicalSpace α<VAR>U : Set β<GOAL>(∃ t_1, IsOpen t_1 ∧ ⇑e.symm ⁻¹' t_1 = U) ↔ IsOpen (⇑e ⁻¹' U)
<VAR>p : ℝ[X]<VAR>hp : Irreducible p<GOAL>p.degree ≤ 2
<VAR>p : ℝ[X]<VAR>hp : Irreducible p<VAR>z : ℂ<VAR>hz : (aeval z) p = 0<GOAL>p.degree ≤ 2
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : α → F'<VAR>this : Module ℝ (α → F') := Pi.module α (fun x => F') ℝ<GOAL>μ[-f|m] =ᶠ[ae μ] -μ[f|m]
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>((gradedMul R 𝒜 ℬ) 1) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<GOAL>u ~[l] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<GOAL>0 =o[l] u
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝¹ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>inst✝ : FinitaryExtensive C<VAR>Y X : C<VAR>c : Cocone (pair X Y)<VAR>hc : IsColimit c<GOAL>IsVanKampenColimit c
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hp : p.IsMaximal<VAR>hQ : Subsingleton (S ⧸ P)<GOAL>inertiaDeg f p P = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hp : p.IsMaximal<VAR>hQ : Subsingleton (S ⧸ P)<VAR>this : P = ⊤<GOAL>inertiaDeg f p P = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>hp : p.IsMaximal<VAR>hQ : Subsingleton (S ⧸ ⊤)<GOAL>inertiaDeg f p ⊤ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =o[l] fun x => c • f' x) ↔ f =o[l] f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(f =o[l] fun x => c • f' x) ↔ f =o[l] f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(f =o[l] fun x => ‖c • f' x‖) ↔ f =o[l] f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(f =o[l] fun x => ‖c‖ * ‖f' x‖) ↔ f =o[l] f'
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>h₁ : s ⊆ t<VAR>h₂ : IsOpen t<GOAL>exterior s ⊆ t
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>h₁ : s ⊆ t<VAR>h₂ : IsOpen t<GOAL>⋂₀ {t | IsOpen t ∧ s ⊆ t} ⊆ t