ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>inst✝ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : A ⟶ F.obj X<VAR>v : B ⟶ F.obj Y<VAR>sq : CommSq u i (F.map p) v<VAR>adj : G ⊣ F<GOAL>Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t✝ s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>v : ℕ → Set α<VAR>hv : t ⊆ ⋃ n, v n<VAR>h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤<VAR>A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)<GOAL>μ (toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t✝ s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>v : ℕ → Set α<VAR>hv : t ⊆ ⋃ n, v n<VAR>h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤<VAR>A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)<GOAL>μ ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then h.choose else if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose else ⋯.choose) ∩ s) = μ (t ∩ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>S : E →L[𝕜] F<GOAL>IsSelfAdjoint (S.comp (T.comp (adjoint S)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : adjoint T = T<VAR>S : E →L[𝕜] F<GOAL>adjoint (S.comp (T.comp (adjoint S))) = S.comp (T.comp (adjoint S))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : adjoint T = T<VAR>S : E →L[𝕜] F<GOAL>(S.comp T).comp (adjoint S) = S.comp (T.comp (adjoint S))
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<GOAL>ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => Φ x i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : f ≤ᶠ[ae (μ.restrict (Icc a b))] g<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : f ≤ᶠ[ae (μ.restrict (Icc a b))] g<VAR>H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), f x ≤ g x := Eventually.filter_mono (ae_mono (Measure.restrict_mono Ioc_subset_Icc_self (le_refl μ))) h<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>QuasiMeasurePreserving Inv.inv μ μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hsm : MeasurableSet s<VAR>hμs : μ s = 0<GOAL>(map Inv.inv μ) s = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hsm : MeasurableSet s<VAR>hμs : μ s = 0<GOAL>μ s⁻¹ = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hsm : MeasurableSet s<VAR>hμs : μ s = 0<VAR>hf : Measurable fun z => (z.2 * z.1, z.1⁻¹)<GOAL>μ s⁻¹ = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hsm : MeasurableSet s<VAR>hμs : μ s = 0<VAR>hf : Measurable fun z => (z.2 * z.1, z.1⁻¹)<GOAL>(map (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod μ)) (s⁻¹ ×ˢ s⁻¹) = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hsm : MeasurableSet s<VAR>hμs : μ s = 0<VAR>hf : Measurable fun z => (z.2 * z.1, z.1⁻¹)<VAR>hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)<GOAL>(map (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod μ)) (s⁻¹ ×ˢ s⁻¹) = 0
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>W : C<VAR>f f' : t.pt ⟶ W<VAR>w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'<GOAL>f = f'
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>W : C<VAR>f f' : t.pt ⟶ W<VAR>w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'<GOAL>h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ f, naturality := ⋯ } } = h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ f', naturality := ⋯ } }
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>W : C<VAR>f f' : t.pt ⟶ W<VAR>w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'<GOAL>(fun b => t.ι.app b ≫ f) = fun b => t.ι.app b ≫ f'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm R₁ M₁<VAR>b : B.IsRefl<VAR>W : Submodule R₁ M₁<VAR>hW : Disjoint W (B.orthogonal W)<VAR>x : M₁<VAR>hx : x ∈ W<VAR>b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0<GOAL>⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm R₁ M₁<VAR>b : B.IsRefl<VAR>W : Submodule R₁ M₁<VAR>hW : Disjoint W (B.orthogonal W)<VAR>x : M₁<VAR>hx : x ∈ W<VAR>b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0<GOAL>x ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm R₁ M₁<VAR>b : B.IsRefl<VAR>W : Submodule R₁ M₁<VAR>hW : Disjoint W (B.orthogonal W)<VAR>x : M₁<VAR>hx : x ∈ W<VAR>b₁ : ∀ (n : ↥W), ((B.restrict W) ⟨x, hx⟩) n = 0<VAR>y : M₁<VAR>hy : y ∈ W<GOAL>B.IsOrtho y x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm R₁ M₁<VAR>b : B.IsRefl<VAR>W : Submodule R₁ M₁<VAR>hW : Disjoint W (B.orthogonal W)<VAR>x : M₁<VAR>hx : x ∈ W<VAR>y : M₁<VAR>hy : y ∈ W<VAR>b₁ : ((B.restrict W) ⟨x, hx⟩) ⟨y, hy⟩ = 0<GOAL>B.IsOrtho y x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm R₁ M₁<VAR>b : B.IsRefl<VAR>W : Submodule R₁ M₁<VAR>hW : Disjoint W (B.orthogonal W)<VAR>x : M₁<VAR>hx : x ∈ W<VAR>y : M₁<VAR>hy : y ∈ W<VAR>b₁ : (B x) y = 0<GOAL>B.IsOrtho y x
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>a : A<GOAL>‖↑a‖ = ‖a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hs : MeasurableSet s<GOAL>essSup (s.indicator f) μ = essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (s₁ ∪ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>h₂ : MeasurableSet s₂<GOAL>MeasurableSet (⋃ b, bif b then s₁ else s₂)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ : R[X]<VAR>N i : ℕ<VAR>f : AddMonoidAlgebra R ℕ<GOAL>(embDomain (revAt N) f) i = f ((revAt N) i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>inv (pullback.snd f g) ≫ pullback.fst f g = g ≫ inv f
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>x < y ↔ x' < y'
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abs' (↑f j - ↑f i) < ε<VAR>j : ℕ<VAR>hj : j ≥ i<GOAL>abs' ((fun n => (starRingEnd ℂ) (↑f n)) j - (fun n => (starRingEnd ℂ) (↑f n)) i) < ε
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abs' (↑f j - ↑f i) < ε<VAR>j : ℕ<VAR>hj : j ≥ i<GOAL>abs' (↑f j - ↑f i) < ε
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a x : α<VAR>hx : fract x ≠ 0<GOAL>fract (-x) = 1 - fract x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a x : α<VAR>hx : fract x ≠ 0<GOAL>0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a x : α<VAR>hx : fract x ≠ 0<GOAL>1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a x : α<VAR>hx : fract x ≠ 0<GOAL>-x - (1 - fract x) = ↑(-⌊x⌋ - 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a x : α<VAR>hx : fract x ≠ 0<GOAL>-x + fract x = -↑⌊x⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a x : α<VAR>hx : fract x ≠ 0<GOAL>-(↑⌊x⌋ + fract x) + fract x = -↑⌊x⌋
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ x y : E<GOAL>openSegment 𝕜 x y = (fun p => p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>X✝ Y✝ : (Mon_ Cᵒᵖ)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>f.unop.hom.unop ≫ ((fun A => Mon_OpOpToComon_obj' C (unop A)) Y✝).counit = ((fun A => Mon_OpOpToComon_obj' C (unop A)) X✝).counit
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>X✝ Y✝ : (Mon_ Cᵒᵖ)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(f.unop.hom.unop ≫ ((fun A => Mon_OpOpToComon_obj' C (unop A)) Y✝).counit).op = ((fun A => Mon_OpOpToComon_obj' C (unop A)) X✝).counit.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>X✝ Y✝ : (Mon_ Cᵒᵖ)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>f.unop.hom.unop ≫ ((fun A => Mon_OpOpToComon_obj' C (unop A)) Y✝).comul = ((fun A => Mon_OpOpToComon_obj' C (unop A)) X✝).comul ≫ (f.unop.hom.unop ⊗ f.unop.hom.unop)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>X✝ Y✝ : (Mon_ Cᵒᵖ)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(f.unop.hom.unop ≫ ((fun A => Mon_OpOpToComon_obj' C (unop A)) Y✝).comul).op = (((fun A => Mon_OpOpToComon_obj' C (unop A)) X✝).comul ≫ (f.unop.hom.unop ⊗ f.unop.hom.unop)).op
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>inst✝ : OrderBot α<GOAL>⊥ < a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>inst✝ : OrderBot α<VAR>h : ⊥ = a<GOAL>⊥ < a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>inst✝ : OrderBot α<VAR>h : ⊥ < a<GOAL>⊥ < a
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : μH[↑d] s = ⊤<GOAL>↑d ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : μH[↑d] s = ⊤<GOAL>↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d
<VAR>u : PrimeMultiset<VAR>n : ℕ+<GOAL>u.prod ∣ n ↔ u ≤ n.factorMultiset
<VAR>u : PrimeMultiset<VAR>n : ℕ+<VAR>h : u.prod ∣ n.factorMultiset.prod ↔ u ≤ n.factorMultiset := prod_dvd_iff<GOAL>u.prod ∣ n ↔ u ≤ n.factorMultiset
<VAR>u : PrimeMultiset<VAR>n : ℕ+<VAR>h : u.prod ∣ n ↔ u ≤ n.factorMultiset<GOAL>u.prod ∣ n ↔ u ≤ n.factorMultiset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>f : α → β<VAR>hf : ∀ (i : ι), InjOn f (s i)<VAR>x : α<VAR>hx : x ∈ ⋃ i, s i<VAR>y : α<VAR>hy : y ∈ ⋃ i, s i<VAR>hxy : f x = f y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>f : α → β<VAR>hf : ∀ (i : ι), InjOn f (s i)<VAR>x : α<VAR>hx✝ : x ∈ ⋃ i, s i<VAR>y : α<VAR>hy : y ∈ ⋃ i, s i<VAR>hxy : f x = f y<VAR>i : ι<VAR>hx : x ∈ s i<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>f : α → β<VAR>hf : ∀ (i : ι), InjOn f (s i)<VAR>x : α<VAR>hx✝ : x ∈ ⋃ i, s i<VAR>y : α<VAR>hy✝ : y ∈ ⋃ i, s i<VAR>hxy : f x = f y<VAR>i : ι<VAR>hx : x ∈ s i<VAR>j : ι<VAR>hy : y ∈ s j<GOAL>x = y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>h : 1 < |n|<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<GOAL>Ergodic f volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>h : 1 < |n|<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<VAR>he : MeasurePreserving (⇑e) volume volume<GOAL>Ergodic f volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>h : 1 < |n|<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<VAR>he : MeasurePreserving (⇑e) volume volume<GOAL>⇑e ∘ f ∘ ⇑e.symm = fun y => n • y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<VAR>he : MeasurePreserving (⇑e) volume volume<VAR>h : n - 1 ≠ 0<GOAL>⇑e ∘ f ∘ ⇑e.symm = fun y => n • y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<VAR>he : MeasurePreserving (⇑e) volume volume<VAR>h : n - 1 ≠ 0<VAR>hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)<GOAL>⇑e ∘ f ∘ ⇑e.symm = fun y => n • y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<VAR>he : MeasurePreserving (⇑e) volume volume<VAR>h : n - 1 ≠ 0<VAR>hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)<VAR>y : AddCircle T<GOAL>(⇑e ∘ f ∘ ⇑e.symm) y = n • y
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>n : ℤ<VAR>f : AddCircle T → AddCircle T := fun y => n • y + x<VAR>e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))<VAR>he : MeasurePreserving (⇑e) volume volume<VAR>h : n - 1 ≠ 0<VAR>hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)<VAR>y : AddCircle T<GOAL>DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n✝ : ℕ<VAR>h : a * b ∈ I ^ (n✝ + 1)<VAR>hI0 : ¬I = ⊥<GOAL>a ∈ I ∨ b ∈ I ^ (n✝ + 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n✝ : ℕ<VAR>hI0 : ¬I = ⊥<VAR>h : I ^ (n✝ + 1) ∣ span {a} * span {b}<GOAL>I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n✝ : ℕ<VAR>hI0 : ¬I = ⊥<VAR>h : I ^ (n✝ + 1) ∣ span {a} * span {b}<VAR>ha : ¬I ∣ span {a}<GOAL>I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n✝ : ℕ<VAR>hI0 : ¬I = ⊥<VAR>h : I ^ (n✝ + 1) ∣ span {b} * span {a}<VAR>ha : ¬I ∣ span {a}<GOAL>I ∣ span {a} ∨ I ^ (n✝ + 1) ∣ span {b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.formPerm x ∈ l<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∉ l<GOAL>l.formPerm x ∉ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivInvOneMonoid G<VAR>a : G<GOAL>a / 1 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>l l' : Filter α<VAR>f : α → E<VAR>s : Set α<VAR>sl : s ∈ l<VAR>hs : IntegrableOn f s μ<GOAL>IntegrableAtFilter (-f) l μ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.20185, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>c : CokernelCofork S.f<VAR>hc : IsColimit c<GOAL>𝟙 S.X₂ ≫ S.g = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ✝ : Type u_4<VAR>inst✝¹⁸ : CommRing Rₘ<VAR>inst✝¹⁷ : Algebra R Rₘ<VAR>inst✝¹⁶ : CommRing Sₘ✝<VAR>inst✝¹⁵ : Algebra S Sₘ✝<VAR>M : Submonoid R<VAR>inst✝¹⁴ : IsLocalization M Rₘ<VAR>inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝<VAR>inst✝¹² : Algebra Rₘ Sₘ✝<VAR>inst✝¹¹ : Algebra R Sₘ✝<VAR>inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝<VAR>inst✝⁹ : IsScalarTower R S Sₘ✝<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : Algebra R Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<GOAL>traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)