ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : ¬ε = ⊤<VAR>hεpow : ε ^ p.toReal ≠ 0<VAR>hεpow' : ε ^ p.toReal ≠ ⊤<GOAL>ε ^ p.toReal * μ {x | ε ≤ ↑‖f x‖₊} ≤ eLpNorm f p μ ^ p.toReal
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<GOAL>HasMFDerivAt (I.prod I') I' Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<GOAL>HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I' x Prod.snd) (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I')) (↑(extChartAt (I.prod I') x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<VAR>this : ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x, (↑(extChartAt I' x.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod I') x).symm) y = y.2<GOAL>HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I' x Prod.snd) (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I')) (↑(extChartAt (I.prod I') x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>x : M × M'<VAR>this : ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x, (↑(extChartAt I' x.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod I') x).symm) y = y.2<GOAL>(↑(extChartAt I' x.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod I') x).symm) (↑(extChartAt (I.prod I') x) x) = (↑(extChartAt (I.prod I') x) x).2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>mulETransformLeft e⁻¹ x = (mulETransformRight e x.swap).swap
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : Archimedean α<VAR>x✝ y ε x : α<VAR>n : ℕ<VAR>h : x < ↑n<GOAL>x < ↑↑n
<VAR>n m : ℕ<GOAL>m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Prime p → p ∣ m → p < n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring α<VAR>a✝ b✝ a b : α<VAR>u : αˣ<GOAL>a /ₚ u - b = (a - b * ↑u) /ₚ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring α<VAR>a✝ b✝ a b : α<VAR>u : αˣ<GOAL>b = b * ↑u * ↑u⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>0 ≤ sign a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : 0 < a<GOAL>0 ≤ sign a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : 0 = a<GOAL>0 ≤ sign a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>h : a < 0<GOAL>0 ≤ sign a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<GOAL>((fun x => rexp (f x)) =o[l] fun x => rexp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop
<VAR>n : ℕ+<VAR>h : n < 2<GOAL>n = 1
<VAR>n : ℕ+<VAR>h : n < 2<GOAL>n ≤ 1
<VAR>n : ℕ+<VAR>h : n < 2<GOAL>1 ≤ n
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ≥0<VAR>c : R<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<GOAL>(c • μ) s = c • μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>l : a.IsLimit<VAR>b0 : 0 < b<GOAL>(a * b).IsLimit
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>l : a.IsLimit<VAR>b0 : 0 < 0<GOAL>(a * 0).IsLimit
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>l : a.IsLimit<VAR>b : Ordinal.{u_4}<VAR>b0 : 0 < succ b<GOAL>(a * succ b).IsLimit
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>l : a.IsLimit<VAR>b0 : 0 < b<VAR>lb : b.IsLimit<GOAL>(a * b).IsLimit
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(cyclotomic' n R).degree = ↑n.totient
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<GOAL>F.IsMittagLeffler ↔ ∀ (j : J), ∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a b : 𝕜<VAR>f : E →ᵃ[𝕜] F<VAR>h : a + b = 1<GOAL>f (a • x + b • y) = a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a b : 𝕜<VAR>f : E →ᵃ[𝕜] F<VAR>h : a + b = 1<GOAL>f (b • (y -ᵥ x) + x) = b • (f y -ᵥ f x) + f x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring k<VAR>inst✝¹ : Algebra R k<VAR>inst✝ : AddMonoid G<VAR>r : R<GOAL>(↑↑__src✝).toFun ((algebraMap R k) r) = (algebraMap R k[G]) r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring k<VAR>inst✝¹ : Algebra R k<VAR>inst✝ : AddMonoid G<VAR>r : R<VAR>x✝ : G<GOAL>((↑↑__src✝).toFun ((algebraMap R k) r)) x✝ = ((algebraMap R k[G]) r) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Multiset α<VAR>hs : s ≠ 0<GOAL>∀ (x : α), x ∈ (ofMultiset s hs).support ↔ x ∈ ↑s.toFinset
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) = (α_ (F.map f) (F.map g) (F.map h)).inv ≫ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : Tendsto (fun n => eLpNorm (f n) p μ) atTop (𝓝 0)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε<VAR>F : Fin N → α → β := fun n => f ↑n<VAR>hF : ∀ (n : Fin N), Memℒp (F n) p μ<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε<VAR>F : Fin N → α → β := fun n => f ↑n<VAR>hF : ∀ (n : Fin N), Memℒp (F n) p μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>h : zeroRootSubalgebra R L H = H<GOAL>(zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : IsClosed s<GOAL>IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : Disjoint u v<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : s ∩ (u ∩ v) = ∅<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : s ∩ (u ∩ v) = ∅<VAR>H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : s ∩ (u ∩ v) = ∅<VAR>H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∧ s ⊆ s<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : s ∩ (u ∩ v) = ∅<VAR>H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : s ∩ (u ∩ v) = ∅<VAR>H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v<GOAL>s ⊆ u ∩ s ∪ v ∩ s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : IsClosed s<VAR>H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v<VAR>u v : Set α<VAR>hu : IsClosed u<VAR>hv : IsClosed v<VAR>hss : s ⊆ u ∪ v<VAR>huv : s ∩ (u ∩ v) = ∅<VAR>H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v<GOAL>Disjoint (u ∩ s) (v ∩ s)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>f : M →ₗ[R] M'<VAR>hf_inj : ker f = ⊥<VAR>h : LinearIndependent R v<GOAL>Disjoint (span R (Set.range v)) (ker f)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>(algebraMap K E) (discr K ⇑pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>∏ x : Fin pb.dim, (∏ j ∈ Ioi x, ((e j) pb.gen - (e x) pb.gen)) ^ 2 = ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>inst✝ : Algebra.IsSeparable K L<VAR>i : Fin pb.dim<GOAL>(∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen)) ^ 2 = ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2
<VAR>a b✝ m n✝ p✝ n p b : ℕ<VAR>hb : n ≤ p ^ b<GOAL>n.factorization p ≤ b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<GOAL>(filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).card = s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>z : ∑ i ∈ P.parts, i.card = s.card<GOAL>(filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).card = s.card % P.parts.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>z : (filter (fun x => x.card = s.card / P.parts.card + 1) P.parts).card + P.parts.card * (s.card / P.parts.card) = s.card<GOAL>(filter (fun p => p.card = s.card / P.parts.card + 1) P.parts).card = s.card % P.parts.card
<VAR>m n : ℕ+<GOAL>(m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset
<VAR>m n : ℕ+<GOAL>(m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset
<VAR>m n : ℕ+<GOAL>m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset
<VAR>n a c : ℕ<GOAL>∃ n0, ∀ n ≥ n0, a * c ^ n < (n - 1)!
<VAR>n a c n0 : ℕ<VAR>hn : n0 > 1<VAR>h : ∀ n ≥ n0, (a * c) ^ n < (n - 1)!<GOAL>∃ n0, ∀ n ≥ n0, a * c ^ n < (n - 1)!
<VAR>n✝ a c n0 : ℕ<VAR>hn✝ : n0 > 1<VAR>h : ∀ n ≥ n0, (a * c) ^ n < (n - 1)!<VAR>n : ℕ<VAR>hn : n ≥ n0<GOAL>a * c ^ n ≤ (a * c) ^ n
<VAR>n✝ a c n0 : ℕ<VAR>hn✝ : n0 > 1<VAR>h : ∀ n ≥ n0, (a * c) ^ n < (n - 1)!<VAR>n : ℕ<VAR>hn : n ≥ n0<GOAL>a * c ^ n ≤ a ^ n * c ^ n
<VAR>n✝ a c n0 : ℕ<VAR>hn✝ : n0 > 1<VAR>h : ∀ n ≥ n0, (a * c) ^ n < (n - 1)!<VAR>n : ℕ<VAR>hn : n ≥ n0<GOAL>n ≠ 0
<VAR>x✝ : Unit<VAR>p : ℕ<GOAL>Nat.Partrec.Code.G (x✝, List.map (fun n => let a := ofNat (ℕ × Code) n; List.map (evaln a.1 a.2) (List.range a.1)) (List.range p)).2 = some (let a := ofNat (ℕ × Code) p; List.map (evaln a.1 a.2) (List.range a.1))
<VAR>x✝ : Unit<VAR>p : ℕ<GOAL>List.map (fun n => Nat.rec Option.none (fun n_1 n_ih => rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) n let y ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cg) n Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) x) (fun cf cg x x => Nat.rec (Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) (unpair n).1) (fun n_2 n_ih => do let i ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 n_2) Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i))) (unpair n).2) (fun cf x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) n Nat.rec (some (unpair n).2) (fun n_2 n_ih => Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 ((unpair n).2 + 1))) x) (ofNat Code (unpair p).2)) (unpair p).1) (List.range (unpair p).1) = List.map (evaln (unpair p).1 (ofNat Code (unpair p).2)) (List.range (unpair p).1)