ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p j : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>F : ℕ → ℚ<VAR>S : Finset ℕ<VAR>hn1 : ∀ (i : ℕ), 0 < F i<VAR>s : ℕ<VAR>S' : Finset ℕ<VAR>Hnot : s ∉ S'<VAR>Hne : S'.Nonempty<VAR>Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)<VAR>hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)<GOAL>padicValRat p (F j) < padicValRat p (∑ i ∈ Finset.cons s S' Hnot, F i)
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (map (fun p => p a) l).TFAE<GOAL>(map (fun p => ∃ a, p a) l).TFAE
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (map (fun p => p a) l).TFAE<GOAL>∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)
<VAR>α : Type u_1<VAR>l : List (α → Prop)<VAR>H : ∀ (a : α), (map (fun p => p a) l).TFAE<VAR>p₁ : α → Prop<VAR>hp₁ : p₁ ∈ l<VAR>p₂ : α → Prop<VAR>hp₂ : p₂ ∈ l<GOAL>(∃ a, p₁ a) ↔ ∃ a, p₂ a
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<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>π : ι → Sort u_2<VAR>s : Finset ι<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 = (insert j ↑s).piecewise f g
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<GOAL>MeasurePreserving (⇑(toLin' t.toMatrix)) volume volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<GOAL>MeasurePreserving (⇑(toLin' t.toMatrix)) volume volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<GOAL>Measure.map (⇑(toLin' t.toMatrix)) volume = volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>(Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i : ι, volume (s i)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h2s : MeasurableSet (univ.pi s)<GOAL>(Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i : ι, volume (s i)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h2s : MeasurableSet (univ.pi s)<GOAL>∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.map (⇑(toLin' t.toMatrix)) volume = ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i => volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h2s : MeasurableSet (univ.pi s)<GOAL>(∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂Measure.pi fun x => volume) = ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i => volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h2s : MeasurableSet (univ.pi s)<GOAL>(∫⋯∫⁻_{t.i}, fun a => (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂fun x => volume) = ∫⋯∫⁻_{t.i}, (univ.pi s).indicator 1 ∂fun x => volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h2s : MeasurableSet (univ.pi s)<GOAL>(fun x => ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) (Function.update x t.i xᵢ))) = fun x => ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x t.i xᵢ)
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>t : TransvectionStruct ι ℝ<VAR>ht : Measurable ⇑(toLin' t.toMatrix)<VAR>s : ι → Set ℝ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>h2s : MeasurableSet (univ.pi s)<VAR>x : ι → ℝ<GOAL>∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) (Function.update x t.i xᵢ)) = ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x t.i xᵢ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<GOAL>∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<GOAL>(κ.fst a) {a_1 | ¬κ.densityProcess κ.fst n a a_1 univ = 1} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<GOAL>(κ.fst a) {a_1 | ¬κ.densityProcess κ.fst n a a_1 univ = 1} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<GOAL>(κ.fst a) {x | (κ.fst a) (countablePartitionSet n x) = 0} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<VAR>this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u<GOAL>(κ.fst a) {x | (κ.fst a) (countablePartitionSet n x) = 0} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<VAR>this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u<GOAL>(κ.fst a) (⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<VAR>this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u<GOAL>∑' (p : ↑(countablePartition γ n)), (κ.fst a) (⋃ (_ : (κ.fst a) ↑p = 0), ↑p) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<VAR>this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u<GOAL>(countablePartition γ n).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<VAR>this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u<GOAL>(countablePartition γ n).PairwiseDisjoint fun u => ⋃ (_ : (κ.fst a) u = 0), u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}<VAR>this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u<GOAL>∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A<VAR>Apos : 0 ≤ A<GOAL>‖NumberField.house.asiegel K a‖ ≤ NumberField.house.c₂ K * A
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A<VAR>Apos : 0 ≤ A<GOAL>∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖NumberField.house.asiegel K a i j‖ ≤ NumberField.house.c₂ K * A
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A<VAR>Apos : 0 ≤ A<GOAL>0 ≤ NumberField.house.c₂ K * A
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsLindelof s ↔ IsLindelof (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hs : IsLindelof (f '' s)<VAR>F : Filter X<VAR>F_ne_bot : F.NeBot<VAR>x✝ : CountableInterFilter F<VAR>F_le : F ≤ 𝓟 s<GOAL>∃ x ∈ s, ClusterPt x F
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hs : IsLindelof (f '' s)<VAR>F : Filter X<VAR>F_ne_bot : F.NeBot<VAR>x✝ : CountableInterFilter F<VAR>F_le : F ≤ 𝓟 s<VAR>x : X<VAR>x_in : x ∈ s<VAR>hx : ClusterPt (f x) (map f F)<GOAL>∃ x ∈ s, ClusterPt x F
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : x ∉ closure s<GOAL>ContinuousAt (fun x => (infDist x s)⁻¹) x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : x ∉ closure ∅<GOAL>ContinuousAt (fun x => (infDist x ∅)⁻¹) x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : x ∉ closure s<VAR>hs : s.Nonempty<GOAL>ContinuousAt (fun x => (infDist x s)⁻¹) x
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<GOAL>p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p q✝ : ℝ≥0<VAR>q : ℝ≥0∞<VAR>hpq : 0 ≤ q<GOAL>0 = 0 ∧ q = 0 ∨ 0 = 0 ∧ q = ⊤ ∨ 0 = 0 ∧ 0 < q.toReal ∨ 0 = ⊤ ∧ q = ⊤ ∨ 0 < ENNReal.toReal 0 ∧ q = ⊤ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hp : 0 < p<GOAL>p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : 0 < p<VAR>hpq : p ≤ ⊤<GOAL>p = 0 ∧ ⊤ = 0 ∨ p = 0 ∧ ⊤ = ⊤ ∨ p = 0 ∧ 0 < ⊤.toReal ∨ p = ⊤ ∧ ⊤ = ⊤ ∨ 0 < p.toReal ∧ ⊤ = ⊤ ∨ 0 < p.toReal ∧ 0 < ⊤.toReal ∧ p.toReal ≤ ⊤.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hp : 0 < p<VAR>hq : q < ⊤<GOAL>p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < q.toReal ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < p.toReal ∧ q = ⊤ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hp : 0 < p<VAR>hq : q < ⊤<GOAL>0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hp : 0 < p<VAR>hq : q < ⊤<VAR>hq' : 0 < q<GOAL>0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hp : 0 < p<VAR>hq : q < ⊤<VAR>hq' : 0 < q<VAR>hp' : p < ⊤<GOAL>0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (1 + 1) (-z)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommSemiring S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommSemiring P<VAR>inst✝⁷ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝⁶ : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝⁵ : Algebra P Q<VAR>inst✝⁴ : IsLocalization T Q<VAR>A : Type u_5<VAR>inst✝³ : CommSemiring A<VAR>U : Submonoid A<VAR>W : Type u_6<VAR>inst✝² : CommSemiring W<VAR>inst✝¹ : Algebra A W<VAR>inst✝ : IsLocalization U W<VAR>l : P →+* A<VAR>hl : T ≤ Submonoid.comap l U<VAR>x : S<GOAL>(map W l hl) ((map Q g hy) x) = (map W (l.comp g) ⋯) x
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommSemiring S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommSemiring P<VAR>inst✝⁷ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝⁶ : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝⁵ : Algebra P Q<VAR>inst✝⁴ : IsLocalization T Q<VAR>A : Type u_5<VAR>inst✝³ : CommSemiring A<VAR>U : Submonoid A<VAR>W : Type u_6<VAR>inst✝² : CommSemiring W<VAR>inst✝¹ : Algebra A W<VAR>inst✝ : IsLocalization U W<VAR>l : P →+* A<VAR>hl : T ≤ Submonoid.comap l U<VAR>x : S<GOAL>(map W l hl) ((map Q g hy) x) = ((map W l hl).comp (map Q g hy)) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<VAR>t : Set α<GOAL>t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (r.comp s) l).sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<VAR>t : Set α<GOAL>(∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t) ↔ ∃ x ∈ l, r.core (s.core x) ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter γ<VAR>t✝ : Set α<VAR>t : Set γ<VAR>tsets : t ∈ l<VAR>ht : r.core (s.core t) ⊆ t✝<GOAL>∃ x, (∃ x_1 ∈ l, s.core x_1 ⊆ x) ∧ r.core x ⊆ t✝
<VAR>R : Type u<VAR>inst₁ inst₂ : AddCommGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddCommGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>this : toAddCommGroup = toAddCommGroup<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : AddCommGroupWithOne R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_one : One.one = One.one<VAR>this✝ : toAddCommGroup = toAddCommGroup<VAR>this : toAddGroupWithOne = toAddGroupWithOne<GOAL>inst₁ = inst₂
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>f : Ordinal.{u} → Ordinal.{u}<GOAL>IsNormal f ↔ StrictMono f ∧ Continuous f
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>h : IsNormal f<GOAL>Continuous f
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>f : Ordinal.{u} → Ordinal.{u}<GOAL>StrictMono f ∧ Continuous f → IsNormal f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] ∅<GOAL>s ∩ t =ᶠ[ae μ] ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] ∅<GOAL>∅ = ∅ ∩ t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>c : k<GOAL>affineCombinationLineMapWeights i j c j = c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F U V : Set X<VAR>hU : IsPathConnected U<VAR>hV : IsPathConnected V<VAR>x : X<VAR>xU : x ∈ U<VAR>xV : x ∈ V<GOAL>IsPathConnected (U ∪ V)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F U V : Set X<VAR>hU : IsPathConnected U<VAR>hV : IsPathConnected V<VAR>x : X<VAR>xU : x ∈ U<VAR>xV : x ∈ V<GOAL>∀ {y : X}, y ∈ U ∪ V → JoinedIn (U ∪ V) x y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>p p'✝ : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Ring R₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>p' : Submodule R (M ⧸ p)<GOAL>p ≤ comap p.mkQ p'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>UnifTight f p μ ↔ ∀ ⦃ε : ℝ≥0∞⦄, 0 < ε → ∃ 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>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>UnifTight f p μ ↔ (∀ (r : ℝ≥0), 0 < r → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑r) ∧ (0 < ⊤ → ∃ 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>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>0 < ⊤ → ∃ 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>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>∃ s, μ s ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>μ ∅ ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>x : E<GOAL>IsVonNBounded 𝕜 (x +ᵥ s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>x : E<GOAL>IsVonNBounded 𝕜 ({x} +ᵥ s)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Integrable (fun x => rexp (f x)) μ<VAR>g : α → ℝ<VAR>hg : Integrable (fun x => rexp (g x)) μ<GOAL>(μ.tilted f).tilted g = (μ.tilted g).tilted f
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<GOAL>#{ s // Bounded r s } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>ha : #α = 0<GOAL>#{ s // Bounded r s } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>ha : #α ≠ 0<GOAL>#{ s // Bounded r s } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>ha : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<GOAL>#{ s // Bounded r s } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>ha✝ : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>ha : ℵ₀ ≤ #α<GOAL>#{ s // Bounded r s } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>ha✝ : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>ha : ℵ₀ ≤ #α<GOAL>#{ s // Bounded r s } ≤ #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>ha✝ : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>ha : ℵ₀ ≤ #α<GOAL>#α ≤ #{ s // Bounded r s }