ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedSemiring R<VAR>inst✝⁴ : FloorSemiring R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : OpensMeasurableSpace R<VAR>f : α → R<VAR>n : R<GOAL>MeasurableSet (ceil ⁻¹' {⌈n⌉₊})
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>h : constantCoeff Φ = 0<VAR>n : ℕ<GOAL>constantCoeff (wittStructureRat p Φ n) = 0
<VAR>X✝ : Type w<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : UCompactlyGeneratedSpace X✝<VAR>X Y : CompactlyGenerated<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<VAR>x : (forget CompactlyGenerated).obj X<GOAL>({ toFun := ⇑f, continuous_toFun := ⋯ } ≫ { toFun := ⇑f.symm, continuous_toFun := ⋯ }) x = (𝟙 X) x
<VAR>X✝ : Type w<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : UCompactlyGeneratedSpace X✝<VAR>X Y : CompactlyGenerated<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<VAR>x : (forget CompactlyGenerated).obj Y<GOAL>({ toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ { toFun := ⇑f, continuous_toFun := ⋯ }) x = (𝟙 Y) x
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>‖a‖ ≤ ‖b‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>|a| ≤ |b|
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>a ⊔ -a ≤ |b|
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>- -a ⊔ -a ≤ |b|
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>-(-a ⊓ a) ≤ |b|
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>-(-a ⊓ a) ≤ b ⊔ -b
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b : α<VAR>h : b ⊓ -b ≤ a ⊓ -a<GOAL>-(-a ⊓ a) ≤ - -b ⊔ -b
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : ι → Type u_3<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (x : ι) → Ω → β x<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>iCondIndepFun m' hm' m f μ ↔ ∀ (s : Finset ι) {g : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (g i)) → μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : ι → Type u_3<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (x : ι) → Ω → β x<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>iCondIndep m' hm' (fun x => MeasurableSpace.comap (f x) (m x)) μ ↔ ∀ (s : Finset ι) {g : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (g i)) → μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>β : ι → Type u_3<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (x : ι) → Ω → β x<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s✝ s : Set α<VAR>f : α → G<GOAL>eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s✝ s : Set α<VAR>f : α → G<VAR>x : α<GOAL>(fun x => ↑‖s.indicator f x‖₊) x ≤ (fun x => ↑‖f x‖₊) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s✝ s : Set α<VAR>f : α → G<VAR>x : α<GOAL>s.indicator (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>p q : X ⊕ Y<VAR>x : X<VAR>y : Y<GOAL>Sum.dist p q = glueDist (fun x_1 => ⋯.some) (fun x => ⋯.some) 1 p q
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>nz : v ≠ 0<GOAL>finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>nz : v ≠ 0<GOAL>span K {v} = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>x : α →₀ R<GOAL>(Finsupp.total α M R 0) x = 0
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<GOAL>∫⁻ (a : α), ∫⁻ (t : ℝ) in Ioc 0 (f a), ENNReal.ofReal (g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<GOAL>∫⁻ (a : α), ∫⁻ (a_1 : ℝ), (Ioc 0 (f a)).indicator (fun t => ENNReal.ofReal (g t)) a_1 ∂volume ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<GOAL>∫⁻ (y : ℝ), ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) y ∂μ ∂volume = ∫⁻ (a : ℝ), (Ioi 0).indicator (fun t => μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<GOAL>AEMeasurable (Function.uncurry fun a => (Ioc 0 (f a)).indicator fun t => ENNReal.ofReal (g t)) (μ.prod volume)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<VAR>aux₂ : (Function.uncurry fun x y => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) y) = {p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)<GOAL>AEMeasurable ({p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)) (μ.prod volume)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<VAR>g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t<VAR>integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)<VAR>aux₂ : (Function.uncurry fun x y => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) y) = {p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)<VAR>mble₀ : MeasurableSet {p | p.2 ∈ Ioc 0 (f p.1)}<GOAL>AEMeasurable ({p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)) (μ.prod volume)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝² : Denumerable α✝<VAR>inst✝¹ : Denumerable β✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : Denumerable α<VAR>e : β ≃ α<VAR>n : ℕ<VAR>this : Denumerable β := ofEquiv α e<GOAL>ofNat β n = e.symm (ofNat α n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝² : Denumerable α✝<VAR>inst✝¹ : Denumerable β✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : Denumerable α<VAR>e : β ≃ α<VAR>n : ℕ<VAR>this : Denumerable β := ofEquiv α e<GOAL>decode n = some (e.symm (ofNat α n))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝² : Denumerable α✝<VAR>inst✝¹ : Denumerable β✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : Denumerable α<VAR>e : β ≃ α<VAR>n : ℕ<VAR>this : Denumerable β := ofEquiv α e<GOAL>Option.map (⇑e.symm) (decode n) = some (e.symm (ofNat α n))
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>h₁ : ∀ x ∈ s, f₁ x = f x<GOAL>HasFTaylorSeriesUpToOn n f₁ p s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>h₁ : ∀ x ∈ s, f₁ x = f x<VAR>x : E<VAR>hx : x ∈ s<GOAL>(p x 0).uncurry0 = f₁ x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>h₁ : ∀ x ∈ s, f₁ x = f x<VAR>x : E<VAR>hx : x ∈ s<GOAL>(p x 0).uncurry0 = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>⨆ i, f ⟨i, ⋯⟩ = iSup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>(range fun i => f ⟨i, ⋯⟩) = range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>(range fun i => f ⟨i, ⋯⟩) ⊆ range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>p : ι → Prop<VAR>f : Subtype p → α<VAR>hp : ∀ (i : ι), p i<GOAL>range f ⊆ range fun i => f ⟨i, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>π : α → Type u_11<VAR>ι : α → Type u_12<VAR>t : (a : α) → ι a → Set (π a)<VAR>x✝ : (i : α) → π i<GOAL>(x✝ ∈ ⋃ x, univ.pi fun a => t a (x a)) ↔ x✝ ∈ univ.pi fun a => ⋃ j, t a j
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>comap (↑(opLinearEquiv R).symm) (M * N) = comap (↑(opLinearEquiv R).symm) N * comap (↑(opLinearEquiv R).symm) M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>I : SimpleGraph γ<VAR>x y : (α × β) × γ<GOAL>(G □ (H □ I)).Adj ((Equiv.prodAssoc α β γ) x) ((Equiv.prodAssoc α β γ) y) ↔ (G □ H □ I).Adj x y
<VAR>m n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<VAR>i : Fin (n + 1)<GOAL>cons a f i.rev = snoc (f ∘ rev) a i
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<GOAL>mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<GOAL>Setoid.r a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>i : ι<GOAL>∀ {x : M}, x ∈ S i → x ∈ iSup S
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>i : ι<VAR>this : S i ≤ iSup S<GOAL>∀ {x : M}, x ∈ S i → x ∈ iSup S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformInducing f<GOAL>comap (fun x => ((⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) x.2)) (𝓤 (α →ᵤ[𝔖] β)) = 𝓤 (α →ᵤ[𝔖] γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ<GOAL>comap (fun x => ((⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) x.2)) (𝓤 (α →ᵤ[𝔖] β)) = 𝓤 (α →ᵤ[𝔖] γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ<GOAL>comap (Prod.map (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖))) (𝓤 (α →ᵤ[𝔖] β)) = 𝓤 (α →ᵤ[𝔖] γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : 𝓤 γ = 𝓤 γ<GOAL>𝓤 (α →ᵤ[𝔖] γ) = 𝓤 (α →ᵤ[𝔖] γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : 𝓤 γ = 𝓤 γ<GOAL>UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖) = uniformSpace α γ 𝔖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : 𝓤 γ = 𝓤 γ<GOAL>UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖) = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β 𝔖)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<GOAL>modPart p r < ↑p
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<GOAL>↑p = |↑p|
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<GOAL>↑p ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<GOAL>(a :: l).prod = foldl (fun x x_1 => x * x_1) (a * 1) l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝² : Add α<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : LeftDistribClass α<VAR>a b : α<GOAL>a * (b + 1) = a * b + a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : Semiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>x✝ : Γ<GOAL>((single 0) r * x).coeff x✝ = (r • x).coeff x✝
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.reverse.next ⋯ x ⋯ = s.prev hs x hx
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x : E<VAR>a b : 𝕜<GOAL>Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun x => c • x) t s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x : E<VAR>a b : 𝕜<GOAL>(∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun x => c⁻¹ • x) t s) ↔ ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun x => c • x) t s
<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<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<GOAL>Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
<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<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) * Cardinal.lift.{v, w} (sepDegree (↥(separableClosure F E)) K) = Cardinal.lift.{v, w} (sepDegree F K)<GOAL>Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
<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<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) * Cardinal.lift.{v, w} (sepDegree (↥(separableClosure F E)) K) = Cardinal.lift.{v, w} (sepDegree F K)<VAR>this : IsPurelyInseparable (↥(separableClosure F E)) E<GOAL>Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<GOAL>induced f inst✝¹ ≤ Preorder.topology α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>x : α<GOAL>𝓝 x ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>x : α<GOAL>(⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x})) ⊓ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤ (⨅ b ∈ {x_1 | f x_1 < f x}, 𝓟 {x | f b < f x}) ⊓ ⨅ b ∈ {x_1 | f x < f x_1}, 𝓟 {x | f x < f b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>x a : α<VAR>ha : a ∈ {x_1 | f x_1 < f x}<GOAL>⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x}) ≤ 𝓟 {x | f a < f x}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>x a : α<VAR>ha : a ∈ {x_1 | f x < f x_1}<GOAL>⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤ 𝓟 {x | f x < f a}
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<VAR>U : (Opens ↑↑X)ᵒᵖ<GOAL>(𝟙 X).c.app U = X.presheaf.map (𝟙 U)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<VAR>U : (Opens ↑↑X)ᵒᵖ<GOAL>(𝟙 X.presheaf).app U = 𝟙 (X.presheaf.obj U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<GOAL>↑s = ∅ ↔ s = ⊤
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<GOAL>reflect 1 X = 1