ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this : Nonempty { x // x ∈ s }<GOAL>s.card < t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<GOAL>s.card < t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>dir_lt : (affineSpan k ↑s).direction < (affineSpan k ↑t).direction<GOAL>s.card < t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)<GOAL>s.card < t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)<VAR>finrank_lt : finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 < finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1<GOAL>s.card < t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)<VAR>finrank_lt : Fintype.card { x // x ∈ s } < finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1<GOAL>s.card < t.card
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>b₁ b₂ : β<VAR>a : α<VAR>ha : a ∈ s<VAR>h : f a * b₁ = f a * b₂<GOAL>(∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>h : G.IsClique s<VAR>f : α ↪ β<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : f a ≠ f b<GOAL>(SimpleGraph.map f G).Adj (f a) (f b)
<VAR>R : Type u<VAR>inst✝⁴ : NonUnitalSemiring R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : Nontrivial R<VAR>x : R<VAR>hx : IsRegular x<GOAL>0 < x * star x
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝¹⁰ : Ring 𝕜<VAR>n : ℕ<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousConstSMul 𝕜 E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜 F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousConstSMul 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hp : p ≠ 0<GOAL>p.order = 0 ↔ p 0 ≠ 0
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : Scheme<VAR>f₁ f₂ : X ⟶ Y<VAR>h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂<GOAL>f₁ = f₂
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : Scheme<VAR>f₁ f₂ : X ⟶ Y<VAR>h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂<GOAL>𝒰.fromGlued ≫ f₁ = 𝒰.fromGlued ≫ f₂
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : Scheme<VAR>f₁ f₂ : X ⟶ Y<VAR>h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂<GOAL>∀ (b : 𝒰.gluedCover.diagram.R), Multicoequalizer.π 𝒰.gluedCover.diagram b ≫ 𝒰.fromGlued ≫ f₁ = Multicoequalizer.π 𝒰.gluedCover.diagram b ≫ 𝒰.fromGlued ≫ f₂
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α✝<VAR>α : Type u_3<VAR>d : α → α → ℝ≥0<GOAL>⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε} = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α✝<VAR>α : Type u_3<VAR>d : α → α → ℝ≥0<GOAL>(∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}) ∧ ∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteSemilatticeSup α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : ι → α<GOAL>a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>l : List α<GOAL>l ∈ s.lists ↔ s = ⟦l⟧
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l a✝ : List α<GOAL>l ∈ lists ⟦a✝⟧ ↔ ⟦a✝⟧ = ⟦l⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>inst✝² : (j : α) → Decidable (j ∈ s)<VAR>inst✝¹ : DecidableEq α<VAR>j : α<VAR>inst✝ : (i : α) → Decidable (i ∈ insert j s)<GOAL>(insert j s).piecewise f g = update (s.piecewise f g) j (f j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f g : (i : α) → δ i<VAR>inst✝² : (j : α) → Decidable (j ∈ s)<VAR>inst✝¹ : DecidableEq α<VAR>j : α<VAR>inst✝ : (i : α) → Decidable (i ∈ insert j s)<GOAL>(fun i => if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j)
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>s : Set α<GOAL>∀ (x : α), x ∈ op 1 • s ↔ x ∈ s
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>hB : B.Nondegenerate<VAR>hB' : B.IsSymm<VAR>b : Basis ι S M<GOAL>B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>∂ ⊤ = ⊥
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>h : e ∉ I<GOAL>M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set α)<VAR>h : SeparatesPoints α<VAR>this : MeasurableSpace α := generateFrom S<VAR>x y : α<VAR>hxy : ∀ s ∈ S, x ∈ s ↔ y ∈ s<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set α)<VAR>h : SeparatesPoints α<VAR>this : MeasurableSpace α := generateFrom S<VAR>x y : α<VAR>hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)<GOAL>x = y
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t<GOAL>f.toPOUFun i x = (f i) x * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - (f j) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t<VAR>j : ι<VAR>hj : 1 - (f j) x ≠ 1<GOAL>WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t<VAR>j : ι<VAR>hj : ¬(f j) x = 0<GOAL>WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>i : ι<VAR>x : X<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t<VAR>j : ι<VAR>hj : ¬(f j) x = 0<GOAL>WellOrderingRel j i → j ∈ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>hm₁ : m₁ ≤ mΩ<VAR>hm₂ : m₂ ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>CondIndep m' m₁ m₂ hm' μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>hm₁ : m₁ ≤ mΩ<VAR>hm₂ : m₂ ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>(∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {s | MeasurableSet s} → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']) ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>hm₁ : m₁ ≤ mΩ<VAR>hm₂ : m₂ ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>∀ s ∈ {s | MeasurableSet s}, MeasurableSet s
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : (X ^ n - C x).degree ≠ 0<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : (X ^ n - C x).degree ≠ 0<VAR>z : k<VAR>hz : (X ^ n - C x).IsRoot z<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : (X ^ n - C x).degree ≠ 0<VAR>z : k<VAR>hz : (X ^ n - C x).IsRoot z<GOAL>z ^ n = x
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : 0 < n<VAR>this : (X ^ n - C x).degree ≠ 0<VAR>z : k<VAR>hz : z ^ n - x = 0<GOAL>z ^ n = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>hs : autoParam s.Finite _auto✝<VAR>hsc : autoParam sᶜ.Finite _auto✝<GOAL>s.ncard + sᶜ.ncard = Nat.card α
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<GOAL>coeffs 1 = {1}
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<GOAL>{1} ⊆ coeffs 1
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<GOAL>∃ a ∈ support 1, coeff a 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>c : Chain α<GOAL>⊤ (ωSup c) = ωSup (c.map ⊤)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>c : Chain α<GOAL>∀ (c_1 : β), ⊤ (ωSup c) ≤ c_1 ↔ ωSup (c.map ⊤) ≤ c_1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>c : Chain α<VAR>z : β<GOAL>⊤ (ωSup c) ≤ z ↔ ωSup (c.map ⊤) ≤ z
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<GOAL>(μ.prod ν).map ⋯ = ν.prod μ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<GOAL>↑((μ.prod ν).map ⋯) = ↑(ν.prod μ)
<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>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Memℒp f p μ<GOAL>Memℒp (fun x => RCLike.re (f x)) p μ
<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>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Memℒp f p μ<VAR>this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖<GOAL>Memℒp (fun x => RCLike.re (f x)) p μ
<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>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Memℒp f p μ<VAR>this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖<GOAL>AEStronglyMeasurable (fun x => RCLike.re (f x)) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<GOAL>Ico a b \ Ico c b = Ico a (min b c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<GOAL>MeasurableSet (range Sum.inr)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<GOAL>MeasurableSet (Sum.inr '' univ)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<GOAL>LinearIndependent R v
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<GOAL>∀ (l : ι →₀ R), (Finsupp.total ι N R v) l = 0 → l = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι N R v) l = 0<VAR>a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp<GOAL>l = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι N R v) l = 0<VAR>a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp<VAR>ha : a = 0<GOAL>l = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι N R v) l = 0<VAR>a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp<VAR>ha : a = 0<VAR>i : ι<GOAL>l i = 0 i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι N R v) l = 0<VAR>a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp<VAR>ha : a = 0<VAR>i : ι<GOAL>(fun c => c • v i) (l i) = (fun c => c • v i) (0 i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι N R v) l = 0<VAR>a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp<VAR>ha : a = 0<VAR>i : ι<VAR>this : l i • v i = ↑(a i)<GOAL>(fun c => c • v i) (l i) = (fun c => c • v i) (0 i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<VAR>x✝¹ : DecidableEq ι := Classical.decEq ι<VAR>x✝ : DecidableEq R := Classical.decEq R<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι N R v) l = 0<VAR>a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp<VAR>ha : a = 0<VAR>i : ι<VAR>this : l i = 0 ∨ v i = 0<GOAL>(fun c => c • v i) (l i) = (fun c => c • v i) (0 i)
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>h : abv.IsAdmissible<VAR>A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R<VAR>e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>h✝ : abv.IsAdmissible<VAR>A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R<VAR>e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι<VAR>i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ<VAR>ne : i₀ ≠ i₁<VAR>h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : R<VAR>hb : b ≠ 0<VAR>h✝ : abv.IsAdmissible<VAR>A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R<VAR>e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι<VAR>i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ<VAR>ne : i₀ ≠ i₁<VAR>h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε<VAR>k : ι<GOAL>↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t t' : Set (ProjectiveSpectrum 𝒜)<GOAL>(vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n : ℕ<GOAL>‖x‖ ≤ ↑p ^ (-↑n) ↔ ↑n ≤ x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n : ℕ<GOAL>↑p ^ (-x.valuation) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n k : ℕ<GOAL>↑p ^ (-↑k) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ ↑k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n k : ℕ<GOAL>(↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n k : ℕ<VAR>aux : ∀ (m : ℕ), 0 < ↑p ^ m<GOAL>(↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n k : ℕ<VAR>aux : ∀ (m : ℕ), 0 < ↑p ^ m<GOAL>↑p ^ n ≤ ↑p ^ k ↔ n ≤ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n k : ℕ<VAR>aux : ∀ (m : ℕ), 0 < ↑p ^ m<VAR>this : p ^ n ≤ p ^ k ↔ n ≤ k<GOAL>↑p ^ n ≤ ↑p ^ k ↔ n ≤ k
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>n k : ℕ<VAR>aux : ∀ (m : ℕ), 0 < ↑p ^ m<VAR>this : p ^ n ≤ p ^ k ↔ n ≤ k<GOAL>↑p ^ n ≤ ↑p ^ k ↔ p ^ n ≤ p ^ k
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>s : Finset ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>s : Finset ℕ<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>s : Finset ℕ<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>H₁ : ∏ p ∈ filter Nat.Prime s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1<VAR>s : Finset ℕ<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>H₁ : ∏ p ∈ filter Nat.Prime s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹<VAR>H₂ : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹)
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>i j : ι<VAR>h : i ≠ j<VAR>x : E i<VAR>y : E j<GOAL>1 ≤ dist ⟨i, x⟩ ⟨j, y⟩