ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯<GOAL>⨆ k ∈ Ioo (-q) (-p), weightSpace M (k • -χ₁ + χ₂) = ⨆ i ∈ ⇑e.symm '' Ioo p q, weightSpace M (e i • χ₁ + χ₂)
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Countable ((l : ℕ) × L.Functions l)<VAR>s : L.Substructure M<GOAL>s.CG ↔ Countable ↥s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Countable ((l : ℕ) × L.Functions l)<VAR>s : L.Substructure M<GOAL>s.CG → Countable ↥s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Countable ((l : ℕ) × L.Functions l)<VAR>s : Set M<VAR>h : s.Countable<GOAL>Countable ↥((closure L).toFun s)
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>h'f : Integrable (𝓕 f) volume<VAR>v : V<VAR>hv : ContinuousAt f v<GOAL>𝓕 (𝓕⁻ f) v = f v
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>h'f : Integrable (𝓕 f) volume<VAR>v : V<VAR>hv : ContinuousAt f v<GOAL>𝓕⁻ (𝓕 f) v = f v
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re<GOAL>IntervalIntegrable (fun x => ↑x ^ r) volume a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re<GOAL>∀ (c : ℝ), IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re<VAR>this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re<VAR>this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c<VAR>c : ℝ<VAR>hc : 0 ≤ c<GOAL>IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re<VAR>this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => ↑x ^ r) volume 0 c<VAR>c : ℝ<VAR>hc : c ≤ 0<GOAL>IntervalIntegrable (fun x => ↑x ^ r) volume 0 c
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>y ≤ -x ↔ x ≤ -y
<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✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>a ∈ sphere 1 r ↔ ‖a‖ = r
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.preΨ n).natDegree ≤ (n.natAbs ^ 2 - if Even n then 4 else 1) / 2
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>p.restriction.Monic ↔ p.Monic
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>p.restriction.coeff p.natDegree = 1 ↔ ↑(p.restriction.coeff p.natDegree) = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : s =ᶠ[𝓝 x] t<GOAL>HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : s =ᶠ[𝓝 x] t<GOAL>(fun t => x + t • v) ⁻¹' s =ᶠ[𝓝 0] (fun t => x + t • v) ⁻¹' t
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : s =ᶠ[𝓝 x] t<VAR>F : 𝕜 → E := fun t => x + t • v<GOAL>(fun t => x + t • v) ⁻¹' s =ᶠ[𝓝 0] (fun t => x + t • v) ⁻¹' t
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : s =ᶠ[𝓝 x] t<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>B : ContinuousAt F 0<GOAL>(fun t => x + t • v) ⁻¹' s =ᶠ[𝓝 0] (fun t => x + t • v) ⁻¹' t
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : s =ᶠ[𝓝 x] t<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>B : ContinuousAt F 0<VAR>this : s =ᶠ[𝓝 (F 0)] t<GOAL>(fun t => x + t • v) ⁻¹' s =ᶠ[𝓝 0] (fun t => x + t • v) ⁻¹' t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P : StructuredArrow S T<VAR>f : P ⟶ A<VAR>hf : Mono f<VAR>q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))<VAR>hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom<GOAL>liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P : StructuredArrow S T<VAR>f : P ⟶ A<VAR>hf : Mono f<VAR>q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))<VAR>hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom<GOAL>mk q ≅ P
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P : StructuredArrow S T<VAR>f : P ⟶ A<VAR>hf : Mono f<VAR>q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))<VAR>hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom<GOAL>?i.hom ≫ f = homMk (projectSubobject (Subobject.mk f)).arrow hq
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>Orthonormal ℝ ⇑(e.toBasis.adjustToOrientation x)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<GOAL>∀ (i : ι), (e.toBasis.adjustToOrientation x) i = e i ∨ (e.toBasis.adjustToOrientation x) i = -e i
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>ht : ↑s.card < t.card • b<GOAL>∃ y ∈ t, ↑(filter (fun x => f x = y) s).card < b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>ht : ∑ a ∈ s, 1 < t.card • b<GOAL>∃ y ∈ t, ∑ a ∈ filter (fun x => f x = y) s, 1 < b
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>IsIso ((ΓSpec.adjunction.unit.app X).val.c.app (op (PrimeSpectrum.basicOpen f)))
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>IsIso ((ΓSpec.adjunction.unit.app X).val.c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op)
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>Function.Bijective ⇑((ΓSpec.adjunction.unit.app X).val.c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op)
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>IsLocalization ?M ((forget CommRingCat).obj (((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f))))
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>IsLocalization ?M ((forget CommRingCat).obj (X.presheaf.obj (op (X.basicOpen f))))
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>RingHom.comp ((ΓSpec.adjunction.unit.app X).val.c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op) (algebraMap ?R ((forget CommRingCat).obj (((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f))))) = algebraMap ?R ((forget CommRingCat).obj (X.presheaf.obj (op (X.basicOpen f))))
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>Type ?u.208387
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>CommSemiring ?R
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>Submonoid ?R
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>Algebra ?R ((forget CommRingCat).obj (((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f))))
<VAR>X✝ Y : Scheme<VAR>f✝ : X✝ ⟶ Y<VAR>X : Scheme<VAR>inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op ⊤))<GOAL>Algebra ?R ((forget CommRingCat).obj (X.presheaf.obj (op (X.basicOpen f))))
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>m : M<VAR>p : ι →₀ R<VAR>i : ι<GOAL>((finsuppScalarRight R M ι) (m ⊗ₜ[R] p)) i = (p.sum fun i n => Finsupp.single i (n • m)) i
<VAR>α : Type u_1<VAR>inst✝² : Nontrivial α<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : NoZeroDivisors α<VAR>h : IsRegular 0<GOAL>False
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>S : Set (Set α)<VAR>Sct : S.Countable<VAR>Sp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<GOAL>HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>S : Set (Set α)<VAR>Sct : S.Countable<VAR>Sp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<GOAL>∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, ∃ v, p v ∧ Subtype.val ⁻¹' v = s
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>S : Set (Set α)<VAR>Sct : S.Countable<VAR>Sp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<GOAL>∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, x ∈ s ↔ y ∈ s) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>t : Set α<VAR>S : Set (Set α)<VAR>Sct : S.Countable<VAR>Sp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<VAR>x y : ↑t<VAR>hxy : ∀ s ∈ {x | ∃ s ∈ S, Subtype.val ⁻¹' s = x}, x ∈ s ↔ y ∈ s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : ℚ<VAR>x y : E<GOAL>inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : ℚ<VAR>x y : E<VAR>this : ↑r.den ≠ 0<GOAL>inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : ℚ<VAR>x y : E<VAR>this : ↑r.den ≠ 0<GOAL>inner_ 𝕜 ((↑r.den * (↑↑r.num / ↑↑r.den)) • x) y = ↑r.den * ((starRingEnd 𝕜) (↑↑r.num / ↑↑r.den) * inner_ 𝕜 x y)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : ℚ<VAR>x y : E<VAR>this : ↑r.den ≠ 0<GOAL>inner_ 𝕜 ((↑r.den * (↑r.num / ↑r.den)) • x) y = ↑r.den * (↑r.num / ↑r.den * inner_ 𝕜 x y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>s t : Set α<VAR>ht : IsOpen t<GOAL>frontier (s ∩ t) ∩ t = frontier s ∩ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f p : Perm α<GOAL>p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f p : Perm α<VAR>l : List (Perm α)<VAR>hl : l.Nodup<VAR>hl' : l.toFinset = f.cycleFactorsFinset<GOAL>p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f p : Perm α<VAR>l : List (Perm α)<VAR>hl : l.Nodup<VAR>hl' : l.toFinset = f.cycleFactorsFinset<GOAL>p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f p : Perm α<VAR>l : List (Perm α)<VAR>hl : l.Nodup<VAR>hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f<GOAL>p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<VAR>k : Fin ([n + 1].len + 1)<GOAL>j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<VAR>k : Fin ([n + 1].len + 1)<VAR>hik : k ≤ i<GOAL>j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<VAR>k : Fin ([n + 1].len + 1)<VAR>hik : i < k<GOAL>j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
<VAR>K : Type u_1<VAR>inst✝¹⁵ : NormedLinearOrderedField K<VAR>inst✝¹⁴ : HasSolidNorm K<VAR>inst✝¹³ : FloorRing K<VAR>E✝ : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace K E✝<VAR>inst✝¹⁰ : FiniteDimensional K E✝<VAR>inst✝⁹ : ProperSpace E✝<VAR>L✝ : AddSubgroup E✝<VAR>inst✝⁸ : DiscreteTopology ↥L✝<VAR>ι : Type u_3<VAR>hs : IsZlattice K L✝<VAR>b✝ : Basis ι ℤ ↥L✝<VAR>E : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>L : AddSubgroup E<VAR>inst✝⁴ : DiscreteTopology ↥L<VAR>inst✝³ : IsZlattice ℝ L<VAR>inst✝² : _root_.Finite ι<VAR>b : Basis ι ℤ ↥L<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>μ : MeasureTheory.Measure E<GOAL>MeasureTheory.IsAddFundamentalDomain (↥L) (Zspan.fundamentalDomain (Basis.ofZlatticeBasis ℝ L b)) μ
<VAR>K : Type u_1<VAR>inst✝¹⁵ : NormedLinearOrderedField K<VAR>inst✝¹⁴ : HasSolidNorm K<VAR>inst✝¹³ : FloorRing K<VAR>E✝ : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace K E✝<VAR>inst✝¹⁰ : FiniteDimensional K E✝<VAR>inst✝⁹ : ProperSpace E✝<VAR>L✝ : AddSubgroup E✝<VAR>inst✝⁸ : DiscreteTopology ↥L✝<VAR>ι : Type u_3<VAR>hs : IsZlattice K L✝<VAR>b✝ : Basis ι ℤ ↥L✝<VAR>E : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>L : AddSubgroup E<VAR>inst✝⁴ : DiscreteTopology ↥L<VAR>inst✝³ : IsZlattice ℝ L<VAR>inst✝² : _root_.Finite ι<VAR>b : Basis ι ℤ ↥L<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>x✝ : E<GOAL>L = (span ℤ (Set.range ⇑(Basis.ofZlatticeBasis ℝ L b))).toAddSubgroup
<VAR>K : Type u_1<VAR>inst✝¹⁵ : NormedLinearOrderedField K<VAR>inst✝¹⁴ : HasSolidNorm K<VAR>inst✝¹³ : FloorRing K<VAR>E✝ : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace K E✝<VAR>inst✝¹⁰ : FiniteDimensional K E✝<VAR>inst✝⁹ : ProperSpace E✝<VAR>L✝ : AddSubgroup E✝<VAR>inst✝⁸ : DiscreteTopology ↥L✝<VAR>ι : Type u_3<VAR>hs : IsZlattice K L✝<VAR>b✝ : Basis ι ℤ ↥L✝<VAR>E : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>L : AddSubgroup E<VAR>inst✝⁴ : DiscreteTopology ↥L<VAR>inst✝³ : IsZlattice ℝ L<VAR>inst✝² : _root_.Finite ι<VAR>b : Basis ι ℤ ↥L<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZlatticeBasis ℝ L b))).toAddSubgroup<VAR>e_2✝ : NormedAddGroup.toAddGroup = AddCommGroup.toAddGroup<GOAL>L = (span ℤ (Set.range ⇑(Basis.ofZlatticeBasis ℝ L b))).toAddSubgroup
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>v : Fin 0 → E<GOAL>(pf 0) v = f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>v : Fin 0 → E<VAR>v_eq : v = fun i => 0<GOAL>(pf 0) v = f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>v : Fin 0 → E<VAR>v_eq : v = fun i => 0<VAR>zero_mem : 0 ∈ EMetric.ball 0 r<GOAL>(pf 0) v = f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>v : Fin 0 → E<VAR>v_eq : v = fun i => 0<VAR>zero_mem : 0 ∈ EMetric.ball 0 r<VAR>this : ∀ (i : ℕ), i ≠ 0 → ((pf i) fun j => 0) = 0<GOAL>(pf 0) v = f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<VAR>v : Fin 0 → E<VAR>v_eq : v = fun i => 0<VAR>zero_mem : 0 ∈ EMetric.ball 0 r<VAR>this : ∀ (i : ℕ), i ≠ 0 → ((pf i) fun j => 0) = 0<VAR>A : f (x + 0) = (pf 0) fun x => 0<GOAL>(pf 0) v = f x
<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✝¹ m : MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>sigma_finite_sets : ℕ → Set α := spanningSets μ<VAR>norm_sets : ℕ → Set α := fun n => {x | f x ≤ ↑n}<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = univ
<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✝¹ m : MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>sigma_finite_sets : ℕ → Set α := spanningSets μ<VAR>norm_sets : ℕ → Set α := fun n => {x | f x ≤ ↑n}<VAR>norm_sets_spanning : ⋃ n, norm_sets n = univ<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = univ
<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✝¹ m : MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>sigma_finite_sets : ℕ → Set α := spanningSets μ<VAR>norm_sets : ℕ → Set α := fun n => {x | f x ≤ ↑n}<VAR>norm_sets_spanning : ⋃ n, norm_sets n = univ<VAR>sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n<VAR>h_meas : ∀ (n : ℕ), MeasurableSet (sets n)<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = univ
<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✝¹ m : MeasurableSpace α<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>sigma_finite_sets : ℕ → Set α := spanningSets μ<VAR>norm_sets : ℕ → Set α := fun n => {x | f x ≤ ↑n}<VAR>norm_sets_spanning : ⋃ n, norm_sets n = univ<VAR>sets : ℕ → Set α := fun n => sigma_finite_sets n ∩ norm_sets n<VAR>h_meas : ∀ (n : ℕ), MeasurableSet (sets n)<VAR>h_finite : ∀ (n : ℕ), μ (sets n) < ⊤<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = univ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>t : Set ↑s<VAR>ht : IsClosed t<VAR>hs : IsClosed s<GOAL>IsClosed (Subtype.val '' t)