ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : TopologicalSpace γ<VAR>inst✝¹¹ : TopologicalSpace δ<VAR>inst✝¹⁰ : MeasurableSpace β<VAR>inst✝⁹ : PseudoMetrizableSpace β<VAR>inst✝⁸ : BorelSpace β<VAR>inst✝⁷ : MeasurableSpace γ<VAR>inst✝⁶ : PseudoMetrizableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : SecondCountableTopologyEither β γ<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : PseudoMetrizableSpace δ<VAR>inst✝¹ : OpensMeasurableSpace δ<VAR>inst✝ : SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>hms : MeasurableSet s<VAR>hcs' : μ s ≠ ⊤<VAR>t : Set Ω<GOAL>μ[|s] t * μ s = μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>hms : MeasurableSet s<VAR>hcs' : μ s ≠ ⊤<VAR>t : Set Ω<VAR>hcs : μ s = 0<GOAL>μ[|s] t * μ s = μ (s ∩ t)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>hms : MeasurableSet s<VAR>hcs' : μ s ≠ ⊤<VAR>t : Set Ω<VAR>hcs : μ s ≠ 0<GOAL>μ[|s] t * μ s = μ (s ∩ t)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Lattice (α i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>update f i '' uIcc a (f i) = uIcc (update f i a) f
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Ring R<VAR>inst✝¹ : Module R M<VAR>S : Submodule R M<VAR>inst✝ : S.IsPrincipal<GOAL>S = ⊥ ↔ generator S = 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : S.P T.obj₁<GOAL>S.W T.mor₂
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : S.P T.obj₁<GOAL>∃ X f h, ∃ (_ : Triangle.mk f T.mor₂ h ∈ distinguishedTriangles), S.P X
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y z x✝ : R<GOAL>x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y z x✝ : R<GOAL>(∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>α : Type v<VAR>s : α → Set X<VAR>ho : ∀ (a : α), IsOpen (s a)<VAR>hu : ⋃ a, s a = univ<GOAL>∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>α : Type v<VAR>s : α → Set X<VAR>ho : ∀ (a : α), IsOpen (s a)<VAR>hu : ⋃ a, s a = univ<VAR>U : α → Set Y<VAR>hUo : ∀ (a : α), IsOpen (U a)<VAR>hU : ∀ (a : α), e ⁻¹' U a = s a<GOAL>∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>α : Type v<VAR>s : α → Set X<VAR>ho : ∀ (a : α), IsOpen (s a)<VAR>U : α → Set Y<VAR>hUo : ∀ (a : α), IsOpen (U a)<VAR>hU : ∀ (a : α), e ⁻¹' U a = s a<VAR>hu : ⋃ a, e ⁻¹' U a = univ<GOAL>∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>α : Type v<VAR>s : α → Set X<VAR>ho : ∀ (a : α), IsOpen (s a)<VAR>U : α → Set Y<VAR>hUo : ∀ (a : α), IsOpen (U a)<VAR>hU : ∀ (a : α), e ⁻¹' U a = s a<VAR>hu : ⋃ a, e ⁻¹' U a = univ<VAR>heU : range e ⊆ ⋃ i, U i<GOAL>∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>α : Type v<VAR>s : α → Set X<VAR>ho : ∀ (a : α), IsOpen (s a)<VAR>U : α → Set Y<VAR>hUo : ∀ (a : α), IsOpen (U a)<VAR>hU : ∀ (a : α), e ⁻¹' U a = s a<VAR>hu : ⋃ a, e ⁻¹' U a = univ<VAR>heU : range e ⊆ ⋃ i, U i<VAR>V : α → Set Y<VAR>hVo : ∀ (i : α), IsOpen (V i)<VAR>heV : range e ⊆ ⋃ i, V i<VAR>hVf : LocallyFinite V<VAR>hVU : ∀ (i : α), V i ⊆ U i<GOAL>∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace Y<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>α : Type v<VAR>s : α → Set X<VAR>ho : ∀ (a : α), IsOpen (s a)<VAR>U : α → Set Y<VAR>hUo : ∀ (a : α), IsOpen (U a)<VAR>hU : ∀ (a : α), e ⁻¹' U a = s a<VAR>hu : ⋃ a, e ⁻¹' U a = univ<VAR>heU : range e ⊆ ⋃ i, U i<VAR>V : α → Set Y<VAR>hVo : ∀ (i : α), IsOpen (V i)<VAR>heV : range e ⊆ ⋃ i, V i<VAR>hVf : LocallyFinite V<VAR>hVU : ∀ (i : α), V i ⊆ U i<GOAL>⋃ b, (fun a => e ⁻¹' V a) b = univ
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>β : ι✝ → Type u_4<VAR>inst✝⁵ : Fact (1 ≤ p)<VAR>inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)<VAR>inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)<VAR>inst✝² : Fintype ι✝<VAR>ι : Type u_5<VAR>inst✝¹ : Finite ι<VAR>α : ι → Type u_6<VAR>inst✝ : (i : ι) → PseudoMetricSpace (α i)<VAR>f g : PiLp ⊤ α<GOAL>⨆ i, edist (f i) (g i) ≠ ⊤
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>β : ι✝ → Type u_4<VAR>inst✝⁵ : Fact (1 ≤ p)<VAR>inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)<VAR>inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)<VAR>inst✝² : Fintype ι✝<VAR>ι : Type u_5<VAR>inst✝¹ : Finite ι<VAR>α : ι → Type u_6<VAR>inst✝ : (i : ι) → PseudoMetricSpace (α i)<VAR>f g : PiLp ⊤ α<VAR>val✝ : Fintype ι<GOAL>⨆ i, edist (f i) (g i) ≠ ⊤
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>β : ι✝ → Type u_4<VAR>inst✝⁵ : Fact (1 ≤ p)<VAR>inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)<VAR>inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)<VAR>inst✝² : Fintype ι✝<VAR>ι : Type u_5<VAR>inst✝¹ : Finite ι<VAR>α : ι → Type u_6<VAR>inst✝ : (i : ι) → PseudoMetricSpace (α i)<VAR>f g : PiLp ⊤ α<VAR>val✝ : Fintype ι<VAR>M : { r // 0 ≤ r }<VAR>hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M<GOAL>⨆ i, edist (f i) (g i) ≠ ⊤
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>β : ι✝ → Type u_4<VAR>inst✝⁵ : Fact (1 ≤ p)<VAR>inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)<VAR>inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)<VAR>inst✝² : Fintype ι✝<VAR>ι : Type u_5<VAR>inst✝¹ : Finite ι<VAR>α : ι → Type u_6<VAR>inst✝ : (i : ι) → PseudoMetricSpace (α i)<VAR>f g : PiLp ⊤ α<VAR>val✝ : Fintype ι<VAR>M : { r // 0 ≤ r }<VAR>hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M<VAR>i : ι<GOAL>edist (f i) (g i) ≤ ↑M
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι✝ : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>β : ι✝ → Type u_4<VAR>inst✝⁵ : Fact (1 ≤ p)<VAR>inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)<VAR>inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)<VAR>inst✝² : Fintype ι✝<VAR>ι : Type u_5<VAR>inst✝¹ : Finite ι<VAR>α : ι → Type u_6<VAR>inst✝ : (i : ι) → PseudoMetricSpace (α i)<VAR>f g : PiLp ⊤ α<VAR>val✝ : Fintype ι<VAR>M : { r // 0 ≤ r }<VAR>hM : ∀ (i : ι), ⟨dist (f i) (g i), ⋯⟩ ≤ M<VAR>i : ι<GOAL>↑⟨dist (f i) (g i), ⋯⟩ ≤ ↑M
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hy : y ∈ I<GOAL>x * y ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ t : Set α<VAR>s : Finset α<VAR>inst✝ : Fintype ↑t<GOAL>s ⊆ t.toFinset ↔ ↑s ⊆ t
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝¹ : TotalComplexShape c₂ c₁ c₁₂<VAR>inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)
<VAR>x : ℝ≥0∞<GOAL>x⁻¹.log = -x.log
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>V : ι → Type u_4<VAR>hc : Fintype.card ι < n<GOAL>(completeMultipartiteGraph V).CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>V : ι → Type u_4<VAR>hc : Fintype.card ι < n<GOAL>⊤ ↪g completeMultipartiteGraph V → False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>V : ι → Type u_4<VAR>hc : Fintype.card ι < n<VAR>f : ⊤ ↪g completeMultipartiteGraph V<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>V : ι → Type u_4<VAR>hc : Fintype.card ι < n<VAR>f : ⊤ ↪g completeMultipartiteGraph V<VAR>v w : Fin n<VAR>hn : v ≠ w<VAR>he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>V : ι → Type u_4<VAR>hc : Fintype.card ι < n<VAR>f : ⊤ ↪g completeMultipartiteGraph V<VAR>v w : Fin n<VAR>hn : (f v).fst ≠ (f w).fst<VAR>he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w<GOAL>False
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : IsProbabilityMeasure μ<VAR>f : X →ᵇ E<GOAL>‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : IsProbabilityMeasure μ<VAR>f : X →ᵇ E<GOAL>‖f‖ = (μ Set.univ).toReal * ‖f‖
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝¹ : CardinalInterFilter l c<VAR>g : Set (Set α)<VAR>f : Filter α<VAR>inst✝ : CardinalInterFilter f c<VAR>hc : 2 < c<VAR>h : g ⊆ f.sets<VAR>s : Set α<VAR>hs : s ∈ cardinalGenerate g hc<GOAL>s ∈ f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y z : (i : ι) → β i<GOAL>hammingDist x z ≤ hammingDist x y + hammingDist y z
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<GOAL>Measure.trim 0 hm = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : ↥(Lp E 1 μ)<VAR>hC : 0 ≤ C<GOAL>‖setToFun μ T hT ↑↑f‖ ≤ C * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : ↥(Lp E 1 μ)<VAR>hC : 0 ≤ C<GOAL>‖(L1.setToL1 hT) f‖ ≤ C * ‖f‖
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<GOAL>μ (limsup s atTop) = 0
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<VAR>ht : ∑' (i : ℕ), μ (t i) ≠ ⊤<GOAL>μ (limsup s atTop) = 0
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<VAR>ht : ∑' (i : ℕ), μ (t i) ≠ ⊤<GOAL>μ (limsup t atTop) = 0
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<VAR>ht : ∑' (i : ℕ), μ (t i) ≠ ⊤<GOAL>μ (⋂ n, ⋃ i, t (i + n)) ≤ 0
<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>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<VAR>ht : ∑' (i : ℕ), μ (t i) ≠ ⊤<GOAL>Antitone fun n => ⋃ i, t (i + n)
<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>m✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<VAR>ht : ∑' (i : ℕ), μ (t i) ≠ ⊤<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>x : α<GOAL>x ∈ (fun n => ⋃ i, t (i + n)) m → x ∈ (fun n => ⋃ i, t (i + n)) n
<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>m✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : ℕ → Set α<VAR>hs : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>t : ℕ → Set α := fun n => toMeasurable μ (s n)<VAR>ht : ∑' (i : ℕ), μ (t i) ≠ ⊤<VAR>n m : ℕ<VAR>hnm : n ≤ m<VAR>x : α<GOAL>(∃ i, x ∈ t (i + m)) → ∃ i, x ∈ t (i + n)
<VAR>m n : ℕ<VAR>x y : ZMod n<GOAL>(x * y).cast = x.cast * y.cast % ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>g : PseudoEpimorphism β γ<VAR>f₁ f₂ : PseudoEpimorphism α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<GOAL>iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>biproduct.ι f j ▷ X ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j
<VAR>c : Char<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor (c :: l) r it<GOAL>ValidFor l (c :: r) it.prev
<VAR>c : Char<VAR>l r : List Char<VAR>h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }<GOAL>ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev
<VAR>c : Char<VAR>l r : List Char<VAR>h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }<VAR>this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l.reverse + c.utf8Size } = { byteIdx := utf8Len l.reverse }<GOAL>ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev
<VAR>c : Char<VAR>l r : List Char<VAR>h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }<VAR>this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }<GOAL>ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev
<VAR>c : Char<VAR>l r : List Char<VAR>h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }<VAR>this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }<GOAL>ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l } }
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹² : Fintype m<VAR>inst✝¹¹ : Fintype m₁<VAR>inst✝¹⁰ : Fintype m₂<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype n₁<VAR>inst✝⁷ : Fintype n₂<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : DecidableEq m₁<VAR>inst✝⁴ : DecidableEq m₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq n₁<VAR>inst✝¹ : DecidableEq n₂<VAR>inst✝ : Semiring R<VAR>A₁ : Matrix m m₁ R<VAR>A₂ : Matrix m m₂ R<VAR>B₁₁ : Matrix m₁ n₁ R<VAR>B₁₂ : Matrix m₁ n₂ R<VAR>B₂₁ : Matrix m₂ n₁ R<VAR>B₂₂ : Matrix m₂ n₂ R<GOAL>A₁.fromColumns A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromColumns (A₁ * B₁₂ + A₂ * B₂₂)
<VAR>G✝ : PGame<VAR>inst✝¹ : G✝.Impartial<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>G ⧏ 0 ↔ 0 ⧏ G
<VAR>a b : ℕ<VAR>hb₀ : (b / 2).beq 0 = false<VAR>ha : a % 2 = 0<VAR>hb₁ : b % 2 = 0<GOAL>jacobiSymNat a b = 0
<VAR>a b : ℕ<VAR>hb₀ : (b / 2).beq 0 = false<VAR>ha : a % 2 = 0<VAR>hb₁ : b % 2 = 0<VAR>hf : (↑a).gcd ↑b = 1<GOAL>False
<VAR>a b : ℕ<VAR>hb₀ : (b / 2).beq 0 = false<VAR>ha : a % 2 = 0<VAR>hb₁ : b % 2 = 0<VAR>hf : (↑a).gcd ↑b = 1<VAR>h : 2 ∣ a.gcd b<GOAL>False
<VAR>a b : ℕ<VAR>hb₀ : (b / 2).beq 0 = false<VAR>ha : a % 2 = 0<VAR>hb₁ : b % 2 = 0<VAR>hf : (↑a).gcd ↑b = 1<VAR>h : 2 ∣ (↑a).gcd ↑b<GOAL>False
<VAR>a b : ℕ<VAR>hb₀ : (b / 2).beq 0 = false<VAR>ha : a % 2 = 0<VAR>hb₁ : b % 2 = 0<VAR>hf : (↑a).gcd ↑b = 1<VAR>h : Even 1<GOAL>False
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : NonUnitalNonAssocSemiring A<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : NonUnitalNonAssocSemiring C<VAR>inst✝² : Module R C<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>φ : F<VAR>x✝ : B<GOAL>x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : NonUnitalNonAssocSemiring A<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : NonUnitalNonAssocSemiring C<VAR>inst✝² : Module R C<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>φ : F<VAR>x✝ : B<GOAL>(∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<GOAL>Tendsto (fun x => f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x * cos x = (cos a ^ 2 - cos b ^ 2) / 2
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(shiftFunctorZero C A).hom.app X ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<GOAL>A = B
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<VAR>v : n → 𝕜<VAR>t : ℝ<VAR>ht : t ≠ 0<VAR>hv : v ≠ 0<VAR>hv' : (A - B) *ᵥ v = t • v<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<VAR>v : n → 𝕜<VAR>t : ℝ<VAR>ht : t ≠ 0<VAR>hv : v ≠ 0<VAR>hv' : (A - B) *ᵥ v = t • v<VAR>h_sum : 0 = ↑t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v)<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<VAR>v : n → 𝕜<VAR>t : ℝ<VAR>ht : t ≠ 0<VAR>hv : v ≠ 0<VAR>hv' : (A - B) *ᵥ v = t • v<VAR>h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<VAR>v : n → 𝕜<VAR>t : ℝ<VAR>ht : t ≠ 0<VAR>hv : v ≠ 0<VAR>hv' : (A - B) *ᵥ v = t • v<VAR>h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0<VAR>h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0<GOAL>False