ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᶠ[ae μ] fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<VAR>hf_int' : Integrable (fun a => f (X a, Y a)) μ<GOAL>μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᶠ[ae μ] fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s✝ : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<VAR>hf_int' : Integrable (fun a => f (X a, Y a)) μ<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : μ s < ⊤<GOAL>IntegrableOn (fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) s μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<VAR>hf_int' : Integrable (fun a => f (X a, Y a)) μ<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ∫ (y : Ω), f (X x, y) ∂(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in s, f (X x, Y x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<VAR>hf_int' : Integrable (fun a => f (X a, Y a)) μ<GOAL>AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) μ
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0<GOAL>Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom = Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom * (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0<GOAL>Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) = Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0<GOAL>Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0<GOAL>(x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>√x < y ↔ x < y ^ 2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<GOAL>∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<VAR>i : ι<VAR>this : s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}<GOAL>MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<VAR>i : ι<VAR>this : s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}<GOAL>MeasurableSet {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<VAR>i : ι<VAR>this : s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}<GOAL>Measurable fun a => min (τ a) i
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSpace ι<VAR>inst✝ : BorelSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i})<VAR>i : ι<VAR>this : s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i}<GOAL>Measurable fun a => min (min (τ a) (π a)) i
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>c : G<GOAL>μ (c • s) = 0 ↔ μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝¹ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X✝ I✝ : Set α<VAR>M : Matroid α<VAR>I X : Set ↑M.E<GOAL>(M.restrictSubtype M.E).Basis I X ↔ M.Basis ↑I ↑X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s t : Multiset α<VAR>d : s.Nodup<VAR>h : a ∈ s - t<VAR>h' : a ∈ t<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s t : Multiset α<VAR>d : s.Nodup<VAR>h : a ∈ s - t<VAR>h' : a ∈ t<GOAL>count a (s - t) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s t : Multiset α<VAR>d : s.Nodup<VAR>h : a ∈ s - t<VAR>h' : a ∈ t<GOAL>count a s ≤ count a t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha✝ : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>h_spec : spectrum R a ⊆ {1}<VAR>ha : autoParam (p a) _auto✝<GOAL>a = 1
<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>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f<GOAL>sᶜ ∈ 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>hs : IsCompact s<VAR>f : Filter X<VAR>hf : sᶜ ∉ f<GOAL>∃ x ∈ s, sᶜ ∉ 𝓝 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>hs : IsCompact s<VAR>f : Filter X<VAR>hf : (f ⊓ 𝓟 s).NeBot<GOAL>∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ZNum<GOAL>↑n.succ = ↑n + 1
<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<GOAL>s ∈ coclosedCompact X ↔ IsCompact (closure 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<GOAL>(∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure 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>h : IsCompact (closure sᶜ)<GOAL>∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ s
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>p.rev.predAbove i = (p.predAbove i.rev).rev
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : p.succ ≤ i.rev<GOAL>p.rev.predAbove i = (p.predAbove i.rev).rev
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<VAR>h : i.rev ≤ p.castSucc<GOAL>p.rev.predAbove i = (p.predAbove i.rev).rev
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s t : Set X<VAR>h : s ⊆ t<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>dimH s ≤ dimH t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>S : Set (Set α)<VAR>f : Filter α<GOAL>f ≤ generate S ↔ f ≤ ⨅ s ∈ S, 𝓟 s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>v : V<VAR>p₁ p₂ : P<VAR>hv : v ≠ 0<VAR>r : ℝ<GOAL>dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ / ⟪v, v⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>v : V<VAR>p₁ p₂ : P<VAR>hv : v ≠ 0<VAR>r : ℝ<GOAL>⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ / ⟪v, v⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>v : V<VAR>p₁ p₂ : P<VAR>hv : v ≠ 0<VAR>r : ℝ<VAR>hvi : ⟪v, v⟫_ℝ ≠ 0<VAR>hd : discrim (⟪v, v⟫_ℝ) (2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * (2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ)<GOAL>⟪v, v⟫_ℝ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ / ⟪v, v⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>v : V<VAR>p₁ p₂ : P<VAR>hv : v ≠ 0<VAR>r : ℝ<VAR>hvi : ⟪v, v⟫_ℝ ≠ 0<VAR>hd : discrim (⟪v, v⟫_ℝ) (2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ * (2 * ⟪v, p₁ -ᵥ p₂⟫_ℝ)<GOAL>2 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>t : Set β<VAR>s : β → Set α<VAR>ht : t.Countable<VAR>hm : ∀ i ∈ t, NullMeasurableSet (s i) μ<VAR>hd : t.Pairwise (AEDisjoint μ on s)<VAR>f : α → ℝ≥0∞<VAR>this : Encodable ↑t<GOAL>∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<GOAL>xInTermsOfW p R 0 = X 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>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Tendsto (fun n => eLpNorm ((fun x => κ.densityProcess ν n a x s) - Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)) 1 (ν a)) atTop (𝓝 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>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Submartingale (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)
<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>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>UniformIntegrable (fun n x => κ.densityProcess ν n a x s) 1 (ν a)
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : Nontrivial R<VAR>h : ringChar R = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : Nontrivial R<VAR>h : ringChar R = 1<GOAL>0 = 1
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : Nontrivial R<VAR>h : ringChar R = 1<GOAL>1 = 0
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>n : ℕ<VAR>h : Squarefree (x ^ n)<VAR>h' : ¬IsUnit x<GOAL>n = 0 ∨ n = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>n : ℕ<VAR>h : Squarefree (x ^ n)<VAR>h' : n ≠ 0 ∧ n ≠ 1<GOAL>IsUnit x
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>n : ℕ<VAR>h : Squarefree (x ^ n)<VAR>h' : 2 ≤ n<GOAL>IsUnit x
<VAR>R : Type u_1<VAR>inst✝ : CommMonoid R<VAR>x : R<VAR>n : ℕ<VAR>h : Squarefree (x ^ n)<VAR>h' : 2 ≤ n<VAR>this : x * x ∣ x ^ n<GOAL>IsUnit x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a<GOAL>map id ⟨f, al⟩ = ⟨f, al⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a<GOAL>↑(map id ⟨f, al⟩) = ↑⟨f, al⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a<GOAL>Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a<VAR>e : Option.rec none some = id<GOAL>Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a<VAR>e : Option.rec none some = id<VAR>h : (fun x => x) = id<GOAL>Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x : α<VAR>k : ℤ<GOAL>(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x : α<VAR>k : ℤ<GOAL>f ((f ^ k) x) = (f ^ (k + 1)) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x : α<VAR>k : ℤ<GOAL>f.SameCycle x ((f ^ k) x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>⌊fract a⌋ = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>0 ≤ fract a ∧ fract a < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t✝ u v : Finset α<VAR>a b : α<VAR>ha : a ∈ s<VAR>t : Finset α<GOAL>s ∪ t.erase a = s ∪ t
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>l : List α<GOAL>card (Quot.mk Setoid.r l) = countP p (Quot.mk Setoid.r l) + countP (fun x => ¬p x) (Quot.mk Setoid.r l)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.66933, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<GOAL>Epi S.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.66933, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<VAR>this : S.HasHomology<GOAL>Epi S.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.66933, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<VAR>this✝ : S.HasHomology<VAR>this : Mono S.fromOpcycles<GOAL>Epi S.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.66933, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<VAR>this✝¹ : S.HasHomology<VAR>this✝ : Mono S.fromOpcycles<VAR>this : S.pOpcycles = 0<GOAL>Epi S.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.66933, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<VAR>this✝¹ : S.HasHomology<VAR>this✝ : Mono S.fromOpcycles<VAR>this : S.pOpcycles = 0<GOAL>∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.66933, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hg : S.g = 0<VAR>this✝¹ : S.HasHomology<VAR>this✝ : Mono S.fromOpcycles<VAR>this : S.pOpcycles = 0<VAR>A : C<VAR>x₂ : S.X₂ ⟶ A<VAR>hx₂ : S.f ≫ x₂ = 0<GOAL>x₂ = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Fintype V<VAR>inst✝⁴ : DecidableEq V<VAR>G✝ : SimpleGraph V<VAR>inst✝³ : DecidableRel G✝.Adj<VAR>inst✝² : DecidableEq G✝.ConnectedComponent<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>c : G.ConnectedComponent<GOAL>(fun i => if G.connectedComponentMk i = c then 1 else 0) ∈ LinearMap.ker (toLin' (lapMatrix ℝ G))
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Fintype V<VAR>inst✝⁴ : DecidableEq V<VAR>G✝ : SimpleGraph V<VAR>inst✝³ : DecidableRel G✝.Adj<VAR>inst✝² : DecidableEq G✝.ConnectedComponent<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>c : G.ConnectedComponent<GOAL>∀ (i j : V), G.Reachable i j → (if G.connectedComponentMk i = c then 1 else 0) = if G.connectedComponentMk j = c then 1 else 0
<VAR>s : ℝ<GOAL>Tendsto (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
<VAR>s : ℝ<VAR>this : (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹<GOAL>Tendsto (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) atTop (𝓝 0)
<VAR>s : ℝ<VAR>this : (fun x => rexp (-x) * x ^ s / rexp (-(1 / 2) * x)) = (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹<GOAL>Tendsto (fun x => rexp (1 / 2 * x) / x ^ s)⁻¹ atTop (𝓝 0)
<VAR>n i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < [n].len + 1<GOAL>↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 [n])) ⟨j, hj⟩)
<VAR>n i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < n + 1<GOAL>↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 [n])) ⟨j, hj⟩)
<VAR>n i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < n + 1<GOAL>↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯ else (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) = j
<VAR>n i : ℕ<VAR>hi : i < n + 1<VAR>j : ℕ<VAR>hj : j < n + 1<GOAL>(if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1 else ↑((if j < i then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯)) = j