ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s t : Set A<VAR>hst : s ⊆ t<VAR>hs : AlgebraicIndependent R Subtype.val<VAR>u : Set A<VAR>huai : AlgebraicIndependent R Subtype.val<VAR>left✝ : s ⊆ u<VAR>hut : u ⊆ t<VAR>hsu : s ⊆ u<VAR>hx : ∀ a ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}, u ⊆ a → a = u<GOAL>∃ u, AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s t : Set A<VAR>hst : s ⊆ t<VAR>hs : AlgebraicIndependent R Subtype.val<VAR>u : Set A<VAR>huai : AlgebraicIndependent R Subtype.val<VAR>left✝ : s ⊆ u<VAR>hut : u ⊆ t<VAR>hsu : s ⊆ u<VAR>hx : ∀ a ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}, u ⊆ a → a = u<GOAL>∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x✝ : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s t : Set A<VAR>hst : s ⊆ t<VAR>hs : AlgebraicIndependent R Subtype.val<VAR>u : Set A<VAR>huai : AlgebraicIndependent R Subtype.val<VAR>left✝ : s ⊆ u<VAR>hut : u ⊆ t<VAR>hsu : s ⊆ u<VAR>hx : ∀ a ∈ {u | AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t}, u ⊆ a → a = u<VAR>x : Set A<VAR>hxai : AlgebraicIndependent R Subtype.val<VAR>huv : u ⊆ x<VAR>hxt : x ⊆ t<GOAL>x = u
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : IsFiltered C<VAR>O : Finset C<VAR>H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))<VAR>J : Type w<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : FinCategory J<VAR>F : J ⥤ C<GOAL>Nonempty (Cocone F)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : C<VAR>h : ∀ (A : C) (f : I ⟶ A), IsIso f<VAR>I' A : C<VAR>f : I' ⟶ A<VAR>hI' : IsTerminal I'<VAR>this : IsIso (hI'.from I ≫ f)<GOAL>(inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<GOAL>HasConstantSpeedOnWith (naturalParameterization f s a) (variationOnFromTo f s a '' s) 1
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<GOAL>∀ ⦃x : ℝ⦄, x ∈ variationOnFromTo f s a '' s → ∀ ⦃y : ℝ⦄, y ∈ variationOnFromTo f s a '' s → x ≤ y → eVariationOn (naturalParameterization f s a) (variationOnFromTo f s a '' s ∩ Icc x y) = ENNReal.ofReal (↑1 * (y - x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c<GOAL>eVariationOn (naturalParameterization f s a) (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) = ENNReal.ofReal (↑1 * (variationOnFromTo f s a c - variationOnFromTo f s a b))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c<VAR>cb : c ≤ b<GOAL>eVariationOn (naturalParameterization f s a) (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) = ENNReal.ofReal (↑1 * (variationOnFromTo f s a c - variationOnFromTo f s a b))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c<VAR>bc : b ≤ c<GOAL>eVariationOn (naturalParameterization f s a) (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) = ENNReal.ofReal (↑1 * (variationOnFromTo f s a c - variationOnFromTo f s a b))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>IsSelfAdjoint (star x + x)
<VAR>a b k m n p : ℕ<GOAL>p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList
<VAR>R✝ : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : Semiring S<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>I : ι → Ideal R<VAR>hf : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>x : (i : ι) → R ⧸ I i<GOAL>∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = x i
<VAR>R✝ : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : Semiring S<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>I : ι → Ideal R<VAR>hf : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>y : R ⧸ ⨅ i, I i<GOAL>∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = (quotientInfToPiQuotient I) y i
<VAR>R✝ : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : Semiring S<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>I : ι → Ideal R<VAR>hf : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>r : R<GOAL>∃ r_1, ∀ (i : ι), (Quotient.mk (I i)) r_1 = (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) r) i
<VAR>μ ν : YoungDiagram<VAR>h_le : μ.transpose ≤ ν<VAR>c : ℕ × ℕ<VAR>hc : c ∈ μ.cells<GOAL>c ∈ ν.transpose.cells
<VAR>μ ν : YoungDiagram<VAR>h_le : μ.transpose ≤ ν<VAR>c : ℕ × ℕ<VAR>hc : c ∈ μ.cells<GOAL>c.swap ∈ ν
<VAR>α✝ : Type u_1<VAR>dflt : α✝<VAR>acc : Array α✝<VAR>n✝ : Nat<GOAL>takeDTR.go dflt (n✝ + 1) [] acc = acc.data ++ takeD (n✝ + 1) [] dflt
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>Integrable (f - g) μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>toDirectSum ((tprod R M n) x) = (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>(List.ofFn (⇑toDirectSum ∘ fun i => (ι R) (x i))).prod = (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>(List.ofFn fun x_1 => (DirectSum.of (fun n => ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_2 => x x_1)).prod = (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>(DirectSum.of (fun n => ⨂[R]^n M) ((List.finRange n).dProdIndex fun x => 1)) ((List.finRange n).dProd (fun x => 1) fun x_1 => (PiTensorProduct.tprod R) fun x_2 => x x_1) = (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>GradedMonoid.mk ((List.finRange n).dProdIndex fun x => 1) ((List.finRange n).dProd (fun x => 1) fun x_1 => (PiTensorProduct.tprod R) fun x_2 => x x_1) = GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>(List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod = GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
<VAR>p n k : ℕ<VAR>hp : Prime p<GOAL>p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<GOAL>span R ↑{1} = Subalgebra.toSubmodule ⊥
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.negMap ⟦P⟧ = ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hs : ∀ (i : ι), IsPreconnected (s i)<VAR>u v : Set ((i : ι) → π i)<VAR>uo : IsOpen u<VAR>vo : IsOpen v<VAR>hsuv : univ.pi s ⊆ u ∪ v<VAR>f : (i : ι) → π i<VAR>hfs : f ∈ univ.pi s<VAR>hfu : f ∈ u<VAR>g : (i : ι) → π i<VAR>hgs : g ∈ univ.pi s<VAR>hgv : g ∈ v<GOAL>(univ.pi s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hs : ∀ (i : ι), IsPreconnected (s i)<VAR>u v : Set ((i : ι) → π i)<VAR>uo : IsOpen u<VAR>vo : IsOpen v<VAR>hsuv : univ.pi s ⊆ u ∪ v<VAR>f : (i : ι) → π i<VAR>hfs : f ∈ univ.pi s<VAR>hfu : f ∈ u<VAR>g : (i : ι) → π i<VAR>hgs : g ∈ univ.pi s<VAR>hgv : g ∈ v<VAR>I : Finset ι<VAR>hI : I.piecewise f g ∈ u<GOAL>(univ.pi s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hs : ∀ (i : ι), IsPreconnected (s i)<VAR>u v : Set ((i : ι) → π i)<VAR>uo : IsOpen u<VAR>vo : IsOpen v<VAR>hsuv : univ.pi s ⊆ u ∪ v<VAR>f : (i : ι) → π i<VAR>hfs : f ∈ univ.pi s<VAR>hfu : f ∈ u<VAR>g : (i : ι) → π i<VAR>hgs : g ∈ univ.pi s<VAR>hgv : g ∈ v<VAR>hI : ∅.piecewise f g ∈ u<GOAL>(univ.pi s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hs : ∀ (i : ι), IsPreconnected (s i)<VAR>u v : Set ((i : ι) → π i)<VAR>uo : IsOpen u<VAR>vo : IsOpen v<VAR>hsuv : univ.pi s ⊆ u ∪ v<VAR>f : (i : ι) → π i<VAR>hfs : f ∈ univ.pi s<VAR>hfu : f ∈ u<VAR>g : (i : ι) → π i<VAR>hgs : g ∈ univ.pi s<VAR>hgv : g ∈ v<VAR>i : ι<VAR>I : Finset ι<VAR>a✝ : i ∉ I<VAR>ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty<VAR>hI : (insert i I).piecewise f g ∈ u<GOAL>(univ.pi s ∩ (u ∩ v)).Nonempty
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>easy : ¬↑P G < ε<VAR>ε_top : ¬ε = ⊤<GOAL>{Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>ε_top : ¬ε = ⊤<VAR>easy : ε ≤ ↑P G<GOAL>{Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>ε_top : ¬ε = ⊤<VAR>easy : ε ≤ ↑P G<VAR>aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)<GOAL>{Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>ε_top : ¬ε = ⊤<VAR>easy : ε ≤ ↑P G<VAR>aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : Q ∈ (fun Q => ↑Q G) ⁻¹' {x | ↑P G - ε < x}<GOAL>↑P G < ↑Q G + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>ε_top : ¬ε = ⊤<VAR>easy : ε ≤ ↑P G<VAR>aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ↑P G - ε < ↑Q G<GOAL>↑P G < ↑Q G + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>P : ProbabilityMeasure Ω<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>ε : ℝ≥0∞<VAR>ε_pos : 0 < ε<VAR>ε_top : ¬ε = ⊤<VAR>easy : ε ≤ ↑P G<VAR>aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)<VAR>Q : ProbabilityMeasure Ω<VAR>hQ : ↑P G - ε < ↑Q G<GOAL>↑P G = ↑P G - ε + ε
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>y : α<VAR>inst✝ : BEq α<GOAL>findIdx (fun x => x == y) (x :: xs) = bif x == y then 0 else findIdx (fun x => x == y) xs + 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>m : ι → OuterMeasure α<VAR>s : Set α<GOAL>(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>m : ι → OuterMeasure α<VAR>s : Set α<VAR>this : Nonempty ↑I<GOAL>(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n) → Ei i.castSucc<VAR>x : Ei (last n)<GOAL>‖f‖ * ∏ i : Fin (n + 1), ‖snoc m x i‖ = (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n) → Ei i.castSucc<VAR>x : Ei (last n)<GOAL>‖f‖ * ((∏ i : Fin n, ‖snoc m x i.castSucc‖) * ‖snoc m x (last n)‖) = (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>b₁ : Basis ι₁ 𝕜 E<VAR>b₂ : Basis ι₂ 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪b₁ i₁, B (b₂ i₂)⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>b₁ : Basis ι₁ 𝕜 E<VAR>b₂ : Basis ι₂ 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪b₁ i₁, B (b₂ i₂)⟫_𝕜<GOAL>A = adjoint B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>b₁ : Basis ι₁ 𝕜 E<VAR>b₂ : Basis ι₂ 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪b₁ i₁, B (b₂ i₂)⟫_𝕜<VAR>i₁ : ι₁<GOAL>A (b₁ i₁) = (adjoint B) (b₁ i₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : IsEmpty α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>h : (μ.prod ν) s = 0<GOAL>(fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>h : (μ.prod ν) s = 0<VAR>t : Set (α × β)<VAR>hst : s ⊆ t<VAR>mt : MeasurableSet t<VAR>ht : (μ.prod ν) t = 0<GOAL>(fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>h : (μ.prod ν) s = 0<VAR>t : Set (α × β)<VAR>hst : s ⊆ t<VAR>mt : MeasurableSet t<VAR>ht : (fun x => ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0<GOAL>(fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>h : (μ.prod ν) s = 0<VAR>t : Set (α × β)<VAR>hst : s ⊆ t<VAR>mt : MeasurableSet t<VAR>ht : (fun x => ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0<GOAL>(fun x => ν (Prod.mk x ⁻¹' s)) ≤ᶠ[ae μ] 0 ∧ 0 ≤ᶠ[ae μ] fun x => ν (Prod.mk x ⁻¹' s)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs₀ : s ⊆ Ioi 0<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<GOAL>closure E = ⋂ δ ∈ s, thickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs₀ : s ⊆ Ioi 0<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty<GOAL>cthickening 0 E = ⋂ δ ∈ s, thickening δ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<GOAL>Antiperiodic f (-c)
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<GOAL>Irreducible p ↔ Irreducible (map (algebraMap R K) p)
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑⟨c, c0⟩ • a<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑⟨c, c0⟩ • a<VAR>d : R<VAR>d0 : d ∈ R⁰<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑⟨d, d0⟩ • b<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ∈ R⁰<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ∈ R⁰<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<GOAL>IsUnit a ∨ IsUnit b