ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<GOAL>↑q.den * ↑r.den * (q + r).num = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<GOAL>c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<GOAL>c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) = c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<GOAL>↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den ∨ c = 0
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<GOAL>¬c = 0 → ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<GOAL>↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q.num /. ↑q.den + r.num /. ↑r.den = s<GOAL>↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q + r = s<GOAL>↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q + r = s<GOAL>↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * s.num = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q + r = s<GOAL>s.num * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den = (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q + r = s<GOAL>s = ↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (x - y) y).sign = (o.oangle x y).sign
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : CompleteLattice α<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : IsLower α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsLower β<VAR>f : sInfHom α β<GOAL>Continuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : CompleteLattice α<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : IsLower α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsLower β<VAR>f : sInfHom α β<VAR>b : β<GOAL>IsClosed (⇑f ⁻¹' Ici b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : CompleteLattice α<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : IsLower α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsLower β<VAR>f : sInfHom α β<VAR>b : β<GOAL>⇑f ⁻¹' Ici b = Ici (sInf (⇑f ⁻¹' Ici b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : CompleteLattice α<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : IsLower α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsLower β<VAR>f : sInfHom α β<VAR>b : β<VAR>a : α<VAR>ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))<GOAL>b ≤ ↑f (sInf (⇑f ⁻¹' Ici b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : CompleteLattice α<VAR>inst✝⁴ : CompleteLattice β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : IsLower α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsLower β<VAR>f : sInfHom α β<VAR>b : β<VAR>a : α<VAR>ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))<GOAL>b ≤ sInf (⇑f '' (⇑f ⁻¹' Ici b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hg : Measurable g<GOAL>∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hg : Measurable g<GOAL>⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hg : Measurable g<VAR>i : β → ℝ≥0∞<VAR>hi : Measurable i<VAR>h'i : i ≤ f<GOAL>∫⁻ (a : β), i a ∂Measure.map g μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ fun a => f (g a)), ∫⁻ (a : α), g_1 a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hg : Measurable g<VAR>i : β → ℝ≥0∞<VAR>hi : Measurable i<VAR>h'i : i ≤ f<GOAL>∫⁻ (a : β), i a ∂Measure.map g μ ≤ ⨆ (_ : i ∘ g ≤ fun a => f (g a)), ∫⁻ (a : α), (i ∘ g) a ∂μ
<VAR>α✝ : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α✝<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>α : Type u_5<VAR>f : α → β →𝒄 γ<VAR>c✝ : Chain β<VAR>x : α<GOAL>(f x) (ωSup c✝) = ωSup (c✝.map { toFun := fun x y => (f y) x, monotone' := ⋯ }) x
<VAR>α✝ : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α✝<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>α : Type u_5<VAR>f : α → β →𝒄 γ<VAR>c✝ : Chain β<VAR>x : α<GOAL>ωSup (c✝.map ↑(f x)) = ωSup (c✝.map { toFun := fun x y => (f y) x, monotone' := ⋯ }) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>ht : IsLowerSet t<GOAL>Disjoint (↑(upperClosure s)) t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>ht : IsLowerSet t<GOAL>Disjoint s t → Disjoint (↑(upperClosure s)) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>ht : IsLowerSet t<GOAL>(∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCancelCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>inst✝ : DecidableEq (ι → μ)<VAR>hi : i ∉ s<VAR>n : μ<GOAL>(insert i s).piAntidiag n = (antidiagonal n).biUnion fun p => image (fun f j => f j + if j = i then p.1 else 0) (s.piAntidiag p.2)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r x : R<GOAL>x ∈ {r} + σ a ↔ x ∈ σ (↑ₐ r + a)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>inst✝² : ∀ (i : ι), K.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L.HasHomology i<VAR>inst✝ : ∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ'<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso φ
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>inst✝² : ∀ (i : ι), K.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L.HasHomology i<VAR>inst✝ : ∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ'<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso (φ ≫ φ')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : Nonempty ι<VAR>l : (i : ι) → Filter (α i)<VAR>hl : ∀ (i : ι), Cauchy (l i)<GOAL>Cauchy (Filter.pi l)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : Nonempty ι<VAR>l : (i : ι) → Filter (α i)<VAR>hl : ∀ (i : ι), Cauchy (l i)<VAR>this : ∀ (i : ι), (l i).NeBot<GOAL>Cauchy (Filter.pi l)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w x y : V<VAR>p : G.Walk x y<VAR>hp : ¬p.Nil<GOAL>x :: (p.tail hp).support = p.support
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>rightLim (↑f) x = ↑f x
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>ContinuousWithinAt (↑f) (Ici x) x
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y₁ Y₂ : C<VAR>f : Y₁ ⟶ Y₂<GOAL>𝟙 X ⊗ f = X ◁ f
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L✝ : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ : V → E<VAR>inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun v => VectorFourier.fourierSMulRight L f v) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L✝ : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ : V → E<VAR>inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L✝ : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ : V → E<VAR>inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>aux0 : Continuous fun p => p.1.smulRight p.2<GOAL>AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L✝ : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ : V → E<VAR>inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>μ : Measure V<VAR>hf : AEStronglyMeasurable f μ<VAR>aux0 : Continuous fun p => p.1.smulRight p.2<VAR>aux1 : AEStronglyMeasurable (fun v => (L v, f v)) μ<GOAL>AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>s : Multiset F[X]<VAR>hs : ∀ p ∈ s, IsSolvable p.Gal<GOAL>IsSolvable s.prod.Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>s : Multiset F[X]<VAR>hs : ∀ p ∈ s, IsSolvable p.Gal<GOAL>IsSolvable (Multiset.prod 0).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>s : Multiset F[X]<VAR>hs : ∀ p ∈ s, IsSolvable p.Gal<GOAL>∀ {a : F[X]} {s_1 : Multiset F[X]}, a ∈ s → s_1 ⊆ s → IsSolvable s_1.prod.Gal → IsSolvable (insert a s_1).prod.Gal
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>W₂ : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>Q₂ : Type u_8<VAR>inst✝¹⁶ : NormedAddCommGroup V<VAR>inst✝¹⁵ : MetricSpace P<VAR>inst✝¹⁴ : NormedAddTorsor V P<VAR>inst✝¹³ : NormedAddCommGroup W<VAR>inst✝¹² : MetricSpace Q<VAR>inst✝¹¹ : NormedAddTorsor W Q<VAR>inst✝¹⁰ : NormedAddCommGroup W₂<VAR>inst✝⁹ : MetricSpace Q₂<VAR>inst✝⁸ : NormedAddTorsor W₂ Q₂<VAR>inst✝⁷ : NormedField R<VAR>inst✝⁶ : NormedSpace R V<VAR>inst✝⁵ : NormedSpace R W<VAR>inst✝⁴ : NormedSpace R W₂<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : NormedSpace 𝕜 W₂<VAR>f : V →ᴬ[𝕜] W<VAR>g : W₂ →ᴬ[𝕜] V<GOAL>‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>W₂ : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>Q₂ : Type u_8<VAR>inst✝¹⁶ : NormedAddCommGroup V<VAR>inst✝¹⁵ : MetricSpace P<VAR>inst✝¹⁴ : NormedAddTorsor V P<VAR>inst✝¹³ : NormedAddCommGroup W<VAR>inst✝¹² : MetricSpace Q<VAR>inst✝¹¹ : NormedAddTorsor W Q<VAR>inst✝¹⁰ : NormedAddCommGroup W₂<VAR>inst✝⁹ : MetricSpace Q₂<VAR>inst✝⁸ : NormedAddTorsor W₂ Q₂<VAR>inst✝⁷ : NormedField R<VAR>inst✝⁶ : NormedSpace R V<VAR>inst✝⁵ : NormedSpace R W<VAR>inst✝⁴ : NormedSpace R W₂<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : NormedSpace 𝕜 W₂<VAR>f : V →ᴬ[𝕜] W<VAR>g : W₂ →ᴬ[𝕜] V<GOAL>‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ ∧ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ : ℝ → E<VAR>a✝ b✝ : ℝ<VAR>μ✝ : Measure ℝ<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<GOAL>IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : MulZeroClass M₀<VAR>s : Set M₀<GOAL>0 ∈ s.centralizer
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>i : X ≅ Y<VAR>j : Y ≅ Z<GOAL>(F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<VAR>hG : IsCoseparator G<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h<VAR>H : C<VAR>hH : H ∈ {G}<VAR>h : Y ⟶ H<GOAL>f ≫ h = g ≫ h
<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>f g : X ⟶ Y<VAR>H : C<VAR>h : Y ⟶ H<VAR>hG : IsCoseparator H<VAR>hfg : ∀ (h : Y ⟶ H), f ≫ h = g ≫ h<VAR>hH : H ∈ {H}<GOAL>f ≫ h = g ≫ h
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A : OrderTop α<VAR>hB : PartialOrder α<VAR>B : OrderTop α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊤ = ⊤
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A B : OrderTop α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊤ = ⊤
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A B : OrderTop α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊤ ≤ ⊤
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<GOAL>count K v 0 = 0
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>IsIntegralClosure ↥(adjoin ℤ {ζ}) ℤ K
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<GOAL>(∃ y, (algebraMap (↥(adjoin ℤ {ζ})) K) y = x) → IsIntegral ℤ 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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<VAR>this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<VAR>this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K<VAR>H : Algebra.discr ℚ ⇑B.basis • x ∈ adjoin ℤ {B.gen}<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<VAR>this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K<VAR>H : Algebra.discr ℚ ⇑B.basis • x ∈ adjoin ℤ {B.gen}<VAR>u : ℤˣ<VAR>n : ℕ<VAR>hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<VAR>this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K<VAR>u : ℤˣ<VAR>n : ℕ<VAR>H : (↑↑u * ↑↑p ^ n) • x ∈ adjoin ℤ {B.gen}<VAR>hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<VAR>this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K<VAR>u : ℤˣ<VAR>n : ℕ<VAR>hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n<VAR>H : u.inv • (↑↑u * ↑↑p ^ n) • x ∈ adjoin ℤ {B.gen}<GOAL>x ∈ adjoin ℤ {ζ}
<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} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>x : K<VAR>h : IsIntegral ℤ x<VAR>B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ<VAR>hint : IsIntegral ℤ B.gen<VAR>this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K<VAR>u : ℤˣ<VAR>n : ℕ<VAR>hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n<VAR>H : (algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}<GOAL>x ∈ adjoin ℤ {ζ}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>f : β → α<VAR>s : Set α<GOAL>Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ n ≥ N, f n ∈ s