ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>df : p.natDegree < n<GOAL>(p - q).coeff n = -q.coeff n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_directed : Directed LE.le (aeSeq hf p)<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_directed : Directed LE.le (aeSeq hf p)<GOAL>∫⁻ (a : α), (⨆ i, f i) a ∂μ = ∫⁻ (a : α), ⨆ b, aeSeq hf p b a ∂?m.329415
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_directed : Directed LE.le (aeSeq hf p)<GOAL>⨆ b, ∫⁻ (a : α), f b a ∂μ = ⨆ b, ∫⁻ (a : α), aeSeq hf p b a ∂?m.329415
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>p : α → (β → ℝ≥0∞) → Prop := fun x f' => Directed LE.le f'<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x<VAR>h_ae_seq_directed : Directed LE.le (aeSeq hf p)<GOAL>Measure α
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p p' : R[X]<VAR>q : PolynomialModule R M<GOAL>(comp p) (p' • q) = p'.comp p • (comp p) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>p p' : R[X]<VAR>q : PolynomialModule R M<GOAL>eval₂ (algebraMap R R[X]) p p' • (eval p) ((map R[X] (lsingle R 0)) q) = eval₂ C p p' • (eval p) ((map R[X] (lsingle R 0)) q)
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : SimpleFunc α ℝ<VAR>g : α → ℝ<VAR>hg : Integrable g μ<VAR>this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)<GOAL>μ[↑f * g|m] =ᶠ[ae μ] ↑f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : SimpleFunc α ℝ<VAR>g : α → ℝ<VAR>hg : Integrable g μ<VAR>this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)<VAR>c : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ[↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * g|m] =ᶠ[ae μ] ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : SimpleFunc α ℝ<VAR>g : α → ℝ<VAR>hg : Integrable g μ<VAR>this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), s.indicator (Function.const α c) * f = s.indicator (c • f)<VAR>g₁ g₂ : SimpleFunc α ℝ<VAR>x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)<VAR>h_eq₁ : (fun f => μ[↑f * g|m] =ᶠ[ae μ] ↑f * μ[g|m]) g₁<VAR>h_eq₂ : (fun f => μ[↑f * g|m] =ᶠ[ae μ] ↑f * μ[g|m]) g₂<GOAL>μ[↑(g₁ + g₂) * g|m] =ᶠ[ae μ] ↑(g₁ + g₂) * μ[g|m]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<GOAL>(-s).totalVariation = s.totalVariation
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : AddCommMonoid L<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : TopologicalSpace N<VAR>n : MeasurableSpace α<VAR>v : VectorMeasure α M<VAR>hle : m ≤ n<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(trim 0 hle) i = ↑0 i
<VAR>ι : Type u<VAR>X : ι → Type<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J K : ι → Prop<VAR>x : ↑(obj C J)<GOAL>∃ a, (π_app C J) a = x
<VAR>ι : Type u<VAR>X : ι → Type<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J K : ι → Prop<VAR>x : ↑(obj C J)<VAR>y : (i : ι) → X i<VAR>hy : y ∈ C ∧ (precomp Subtype.val) y = ↑x<GOAL>∃ a, (π_app C J) a = x
<VAR>d x y z w : ℕ<VAR>xy : { re := ↑x, im := -↑y }.Nonneg<VAR>zw : { re := -↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg
<VAR>d x y z w : ℕ<VAR>xy : { re := ↑x, im := -↑y }.Nonneg<VAR>zw : { re := -↑z, im := ↑w }.Nonneg<VAR>this : { re := subNatNat x z, im := subNatNat w y }.Nonneg<GOAL>({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg
<VAR>d x y z w : ℕ<VAR>xy : { re := ↑x, im := -↑y }.Nonneg<VAR>zw : { re := -↑z, im := ↑w }.Nonneg<VAR>this : { re := subNatNat x z, im := subNatNat w y }.Nonneg<GOAL>{ re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : ∀ i ∈ ↑l, ord I i < o₁<VAR>f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ<GOAL>f ∈ eval (π C fun x => ord I x < o₂) '' {m | m < l} ↔ f ∈ ⇑(πs' C h) '' (eval (π C fun x => ord I x < o₁) '' {m | m < l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : ∀ i ∈ ↑l, ord I i < o₁<VAR>f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ<GOAL>(∃ x < l, eval (π C fun x => ord I x < o₂) x = f) ↔ ∃ a < l, (πs' C h) (eval (π C fun x => ord I x < o₁) a) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : ∀ i ∈ ↑l, ord I i < o₁<VAR>f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ<GOAL>∀ (a : Products I), a < l ∧ eval (π C fun x => ord I x < o₂) a = f ↔ a < l ∧ (πs' C h) (eval (π C fun x => ord I x < o₁) a) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : ∀ i ∈ ↑l, ord I i < o₁<VAR>f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ<VAR>m : Products I<GOAL>m < l ∧ eval (π C fun x => ord I x < o₂) m = f ↔ m < l ∧ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : ∀ i ∈ ↑l, ord I i < o₁<VAR>f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ<VAR>m : Products I<GOAL>m < l → (eval (π C fun x => ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : ∀ i ∈ ↑l, ord I i < o₁<VAR>f : LocallyConstant ↑(π C fun x => ord I x < o₂) ℤ<VAR>m : Products I<VAR>hm : m < l<GOAL>eval (π C fun x => ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x => ord I x < o₁) m) = f
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁸ : Ring R✝<VAR>inst✝¹⁷ : Ring R'✝<VAR>inst✝¹⁶ : AddCommGroup M<VAR>inst✝¹⁵ : AddCommGroup M'<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R✝ M<VAR>inst✝¹² : Module R✝ M'<VAR>inst✝¹¹ : Module R✝ M₁<VAR>inst✝¹⁰ : Module R'✝ M'<VAR>inst✝⁹ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>R' : Type w'<VAR>S'✝ : Type v'<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : Ring S'✝<VAR>inst✝³ : Algebra R' S'✝<VAR>S' : Type v<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<GOAL>Module.rank R S ≤ Module.rank R' S'
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalCommSemiring α<VAR>inst✝ : Fintype m<VAR>A : Matrix m n α<VAR>x : m → α<VAR>x✝ : n<GOAL>(Aᵀ *ᵥ x) x✝ = (x ᵥ* A) x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : IntegrableOn f s μ<VAR>hg : IntegrableOn g sᶜ μ<GOAL>∫ (x : X), s.piecewise f g x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, g x ∂μ
<VAR>n✝ : ℕ<VAR>c✝ : Composition n✝<VAR>n : ℕ<VAR>hn : 0 < n<VAR>c : Composition n<GOAL>c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n
<VAR>n✝ : ℕ<VAR>c✝ : Composition n✝<VAR>n : ℕ<VAR>hn : 0 < n<VAR>c : Composition n<GOAL>¬c ≠ single n hn ↔ ¬∀ (i : Fin c.length), c.blocksFun i < n
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>Λ : Module.Dual ℝ ℝ<VAR>Λ₀ : ℝ<VAR>hΛ : (Λ, Λ₀) ≠ 0<VAR>hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0<GOAL>∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>T2Space X ↔ ∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y
<VAR>R : CommRingCat<VAR>f : ↑R<VAR>x : ↑↑(Spec R).toPresheafedSpace<GOAL>x ∈ ↑((Spec R).basicOpen ((Scheme.ΓSpecIso R).inv f)) ↔ x ∈ ↑(PrimeSpectrum.basicOpen f)
<VAR>R : CommRingCat<VAR>f : ↑R<VAR>x : ↑↑(Spec R).toPresheafedSpace<GOAL>IsUnit (((Spec R).presheaf.germ ⟨x, _root_.trivial⟩) ((Scheme.ΓSpecIso R).inv f)) ↔ x ∈ PrimeSpectrum.basicOpen f
<VAR>R : CommRingCat<VAR>f : ↑R<VAR>x : ↑↑(Spec R).toPresheafedSpace<GOAL>IsUnit ((StructureSheaf.toStalk (↑R) x) f) ↔ f ∉ x.asIdeal
<VAR>R : CommRingCat<VAR>f : ↑R<VAR>x : ↑↑(Spec R).toPresheafedSpace<GOAL>IsUnit ((algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ f ∉ x.asIdeal
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<GOAL>Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<GOAL>s.ordT5Nhd t ⊓ t.ordT5Nhd s ≤ ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x : α<VAR>hx₁ : x ∈ s.ordT5Nhd t<VAR>hx₂ : x ∈ t.ordT5Nhd s<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x : α<VAR>hx₁ : x ∈ s.ordT5Nhd t<VAR>hx₂ : x ∈ t.ordT5Nhd s<VAR>a : α<VAR>has : a ∈ s<VAR>ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x : α<VAR>hx₂ : x ∈ t.ordT5Nhd s<VAR>a : α<VAR>has : a ∈ s<VAR>ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x : α<VAR>hx₂ : x ∈ t.ordT5Nhd s<VAR>a : α<VAR>has : a ∈ s<VAR>ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a<VAR>b : α<VAR>hbt : b ∈ t<VAR>hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a<VAR>b : α<VAR>hbt : b ∈ t<VAR>hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>b : α<VAR>hbt : b ∈ t<VAR>hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hb' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hb' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hxa : x ≤ a<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hax : a ≤ x<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hax : a ≤ x<VAR>hbx : b ≤ x<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hax : a ≤ x<VAR>hxb : x ≤ b<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>ha : [[a, x]] ⊆ tᶜ<VAR>hb : [[b, x]] ⊆ sᶜ<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>hax : a ≤ x<VAR>hxb : x ≤ b<VAR>h' : x ∈ s.ordSeparatingSet t<GOAL>x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>x : { x // x ∈ s.ordSeparatingSet t }<VAR>ha : [[a, ↑x]] ⊆ tᶜ<VAR>hb : [[b, ↑x]] ⊆ sᶜ<VAR>hax : a ≤ ↑x<VAR>hxb : ↑x ≤ b<GOAL>↑x ∈ ⊥
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>x : { x // x ∈ s.ordSeparatingSet t }<VAR>ha : [[a, ↑x]] ⊆ tᶜ<VAR>hb : [[b, ↑x]] ⊆ sᶜ<VAR>hax : a ≤ ↑x<VAR>hxb : ↑x ≤ b<GOAL>(s.ordSeparatingSet t).ordConnectedComponent ↑x ⊆ [[a, b]]
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>x : { x // x ∈ s.ordSeparatingSet t }<VAR>ha : [[a, ↑x]] ⊆ tᶜ<VAR>hb : [[b, ↑x]] ⊆ sᶜ<VAR>hax : a ≤ ↑x<VAR>hxb : ↑x ≤ b<VAR>y : α<VAR>hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x<GOAL>y ∈ [[a, b]]
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>x : { x // x ∈ s.ordSeparatingSet t }<VAR>ha : [[a, ↑x]] ⊆ tᶜ<VAR>hb : [[b, ↑x]] ⊆ sᶜ<VAR>hax : a ≤ ↑x<VAR>hxb : ↑x ≤ b<VAR>y : α<VAR>hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x<GOAL>¬y < a ∧ ¬b < y
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>x : { x // x ∈ s.ordSeparatingSet t }<VAR>ha : [[a, ↑x]] ⊆ tᶜ<VAR>hb : [[b, ↑x]] ⊆ sᶜ<VAR>hax : a ≤ ↑x<VAR>hxb : ↑x ≤ b<VAR>y : α<VAR>hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x<VAR>sol1 : y < a → False<GOAL>¬y < a ∧ ¬b < y
<VAR>α✝ : Type u_1<VAR>inst✝¹ : LinearOrder α✝<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>has : a ∈ s<VAR>b : α<VAR>hbt : b ∈ t<VAR>hab : a ≤ b<VAR>hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ<VAR>x : { x // x ∈ s.ordSeparatingSet t }<VAR>ha : [[a, ↑x]] ⊆ tᶜ<VAR>hb : [[b, ↑x]] ⊆ sᶜ<VAR>hax : a ≤ ↑x<VAR>hxb : ↑x ≤ b<VAR>y : α<VAR>hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x<VAR>sol1 : y < a → False<VAR>sol2 : b < y → False<GOAL>¬y < a ∧ ¬b < y
<VAR>p q : ℚ<GOAL>q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : MeasurableSpace α✝<VAR>inst✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Ioc l u = S}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>⟪x, y⟫_𝕜 = 1 ↔ x = y
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
<VAR>R : Type u_1<VAR>inst✝¹ : AddGroupWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a✝ b a : ℤ<GOAL>↑a = 0 ↔ ↑p ∣ a
<VAR>R : Type u_1<VAR>inst✝¹ : AddGroupWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a✝ b a : ℤ<VAR>h : a < 0<GOAL>↑a = 0 ↔ ↑p ∣ a
<VAR>R : Type u_1<VAR>inst✝¹ : AddGroupWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a b : ℤ<GOAL>↑0 = 0 ↔ ↑p ∣ 0
<VAR>R : Type u_1<VAR>inst✝¹ : AddGroupWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a✝ b a : ℤ<VAR>h : 0 < a<GOAL>↑a = 0 ↔ ↑p ∣ a
<VAR>E : ℕ → Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Encodable ι<VAR>F : ι → Type u_3<VAR>inst✝ : (i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<VAR>i : ι<VAR>h : dist x y < (1 / 2) ^ encode i<GOAL>dist (x i) (y i) ≤ dist x y
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁶ : NormedAddCommGroup E✝<VAR>inst✝⁵ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝² : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>k l : ℕ<VAR>h : k + l ≠ Fintype.card ι<VAR>x✝¹ : { s // s.card = l }<VAR>x✝ : x✝¹ ∈ Finset.univ<GOAL>f.toFormalMultilinearSeries.changeOriginSeriesTerm k l ↑x✝¹ ⋯ = 0
<VAR>l : List Prop<GOAL>(map Not l).TFAE ↔ l.TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>↑(lowerClosure s) ⊆ closure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>↑(lowerClosure s) = closure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>inst✝¹ = scott α