ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<VAR>this : ((Functor.const (J × K)).obj c.pt).map (f, 𝟙 k) ≫ c.π.app (j', k) = c.π.app (j, k) ≫ (uncurry.obj F).map (f, 𝟙 k)<GOAL>c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<VAR>this : 𝟙 c.pt ≫ c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k ≫ (F.obj j').map (𝟙 k)<GOAL>c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCones F<VAR>Q : (j : J) → IsLimit (D.obj j)<VAR>c : Cone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<VAR>this : c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k<GOAL>c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k
<VAR>α : Type u_1<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sSup (s / t) = sSup s / sInf t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>v✝ : Fin 0 → α<GOAL>(circulant v✝).IsSymm ↔ ∀ (i : Fin 0), v✝ (-i) = v✝ i
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>x✝ : OpensLeCover U<GOAL>{ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map (𝟙 x✝) = 𝟙 ({ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.obj x✝)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>x✝ : OpensLeCover U<GOAL>({ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map (𝟙 x✝)).left = (𝟙 ({ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.obj x✝)).left
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>x✝² x✝¹ x✝ : OpensLeCover U<VAR>f : x✝² ⟶ x✝¹<VAR>g : x✝¹ ⟶ x✝<GOAL>{ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map (f ≫ g) = { obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map f ≫ { obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>x✝² x✝¹ x✝ : OpensLeCover U<VAR>f : x✝² ⟶ x✝¹<VAR>g : x✝¹ ⟶ x✝<GOAL>({ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map (f ≫ g)).left = ({ obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map f ≫ { obj := fun V => { obj := { left := V.obj, right := { as := PUnit.unit }, hom := homOfLE ⋯ }, property := ⋯ }, map := fun {x x_1} g => Over.homMk g ⋯ }.map g).left
<VAR>α : Type u_1<VAR>b : Bool<VAR>n : PosNum<GOAL>↑(bit b n) = Nat.bit b ↑n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<GOAL>adjoin R {B.gen} = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<GOAL>Set.range ⇑B.basis ⊆ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<VAR>i : Fin B.dim<GOAL>B.basis i ∈ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B✝ : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : IsDomain B✝<VAR>inst✝¹ : Algebra A B✝<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>B : PowerBasis R S<VAR>i : Fin B.dim<GOAL>B.gen ^ ↑i ∈ ↑(Subalgebra.toSubmodule (adjoin R {B.gen}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : EDist α<VAR>x y : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(↑s).einfsep = s.offDiag.inf (uncurry edist)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>↑((Units.map ↑φ) E.Δ') = (E.map φ).Δ
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>↑φ E.Δ = φ E.Δ
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z a : K<VAR>h : ‖a‖ ≤ re a<GOAL>↑(re a) = a
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>finSepDegree F ↥⊥ = 1
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>fmeas : AEMeasurable f μ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδε : δ < ε<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδε : δ < ε<VAR>int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδε : δ < ε<VAR>int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>f_lt_g : ∀ (x : α), ↑(f x) < g x<VAR>gcont : LowerSemicontinuous g<VAR>gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδε : δ < ε<VAR>int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>f_lt_g : ∀ (x : α), ↑(f x) < g x<VAR>gcont : LowerSemicontinuous g<VAR>gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ<VAR>gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ⊤<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδε : δ < ε<VAR>int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>f_lt_g : ∀ (x : α), ↑(f x) < g x<VAR>gcont : LowerSemicontinuous g<VAR>gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ<VAR>gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : Integrable (fun x => ↑(f x)) μ<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0<VAR>εpos : 0 < ↑ε<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδε : δ < ε<VAR>int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>f_lt_g : ∀ (x : α), ↑(f x) < g x<VAR>gcont : LowerSemicontinuous g<VAR>gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ<VAR>gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ⊤<VAR>g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤<VAR>Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<GOAL>Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<VAR>this : Group.IsNilpotent G<GOAL>Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<VAR>this : Group.IsNilpotent G<GOAL>Nat.find ⋯ ≤ Group.nilpotencyClass H + 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<VAR>this : Group.IsNilpotent G<GOAL>lowerCentralSeries G (Group.nilpotencyClass H + 1) = ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<VAR>this : Group.IsNilpotent G<GOAL>Subgroup.map f (lowerCentralSeries G (Group.nilpotencyClass H)) = ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<VAR>this : Group.IsNilpotent G<GOAL>Subgroup.map f (lowerCentralSeries G (Group.nilpotencyClass H)) ≤ ⊥
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H✝ : Subgroup G<VAR>inst✝¹ : H✝.Normal<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ center G<VAR>hH : Group.IsNilpotent H<VAR>this : Group.IsNilpotent G<GOAL>lowerCentralSeries H (Group.nilpotencyClass H) ≤ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>hdeg : 1 < f.natDegree<GOAL>h.modByMonicHom h.root = X
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>inst✝³ : LinearOrder γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderClosedTopology γ<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>hfg : f ≤ᶠ[ae μ] g<GOAL>f ≤ᶠ[ae (μ.trim hm)] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>inst✝³ : LinearOrder γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderClosedTopology γ<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>hm : m ≤ m0<VAR>f g : β → γ<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>hfg : f ≤ᶠ[ae μ] g<GOAL>MeasurableSet {a | ¬f a ≤ g a}
<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<GOAL>DenseRange fun x => ⟦preStoneCechUnit x⟧
<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>this : Function.Surjective t2Quotient.mk<GOAL>DenseRange fun x => ⟦preStoneCechUnit x⟧
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : SupSet α<VAR>inst✝¹ : SupSet β<VAR>inst✝ : sSupHomClass F α β<VAR>f : F<VAR>g : (i : ι) → κ i → α<GOAL>f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<VAR>this : ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)<GOAL>fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<VAR>this : ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)<GOAL>fourierCoeffOn ⋯ (ofReal' ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>y : L<VAR>hy : y ∈ f.rootSet L<VAR>hf : f = 0<GOAL>IsIntegral K y
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>y : L<VAR>hy : y ∈ ∅<VAR>hf : f = 0<GOAL>IsIntegral K y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>Multiset.filter (fun n => 2 ≤ n) σ.partition.parts = σ.cycleType
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>a : ℕ<VAR>h : a ∈ Multiset.replicate (Fintype.card α - σ.support.card) 1<GOAL>¬2 ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>a : ℕ<VAR>h : a ∈ Multiset.replicate (Fintype.card α - σ.support.card) 1<GOAL>¬2 ≤ 1
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>a b : ℝ≥0<VAR>h : ↑a < ↑b<VAR>q : ℚ<VAR>haq : ↑a < ↑q<VAR>hqb : ↑q < ↑b<VAR>this : 0 ≤ ↑q<GOAL>a < (↑q).toNNReal ∧ (↑q).toNNReal < b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap R A) x) 1)) = Submodule.restrictScalars A (kerTotal R B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔ Submodule.span A (Set.range (⇑(Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) ∘ fun x => Finsupp.single ((algebraMap R A) x) 1)) = Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap R B) x) 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<VAR>x✝ : R<VAR>a✝ : B<GOAL>((⇑(Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) ∘ fun x => Finsupp.single ((algebraMap R A) x) 1) x✝) a✝ = (Finsupp.single ((algebraMap R B) x✝) 1) a✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : Algebra.IsSeparable K F<VAR>pb : PowerBasis K L<GOAL>∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : Algebra.IsSeparable K F<VAR>pb : PowerBasis K L<VAR>this : FiniteDimensional L F<GOAL>∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>inst✝¹ : FiniteDimensional K F<VAR>inst✝ : Algebra.IsSeparable K F<VAR>pb : PowerBasis K L<VAR>this✝ : FiniteDimensional L F<VAR>this : Algebra.IsSeparable L F<GOAL>∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen
<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₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : α → E<VAR>a : Filter α<GOAL>Tendsto (fun e => ‖f e / 1‖) a (𝓝 0) ↔ Tendsto (fun x => ‖f x‖) a (𝓝 0)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>x < sin (π / 2 * x)
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>f✝ : R[X]<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>inst✝ : Invertible x<VAR>N : ℕ<VAR>f : R[X]<VAR>hf : f.natDegree ≤ N<GOAL>eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>f✝ : R[X]<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring S<VAR>i : R →+* S<VAR>x : S<VAR>inst✝ : Invertible x<VAR>N : ℕ<VAR>f : R[X]<VAR>hf : f.natDegree ≤ N<GOAL>(fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) 0