ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (h₂.toFun.comp h₂.invFun)
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<GOAL>Epi f ↔ Function.Surjective ⇑f
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<GOAL>Epi f → Function.Surjective ⇑f
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<GOAL>∃ a, f a = y
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<VAR>hy : ∀ (a : (forget Stonean).obj X), f a ≠ y<GOAL>False
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<VAR>hy : ∀ (a : (forget Stonean).obj X), f a ≠ y<VAR>C : Set ((forget Stonean).obj Y) := Set.range ⇑f<GOAL>False
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<VAR>hy : ∀ (a : (forget Stonean).obj X), f a ≠ y<VAR>C : Set ((forget Stonean).obj Y) := Set.range ⇑f<VAR>hC : IsClosed C<GOAL>False
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<VAR>hy : ∀ (a : (forget Stonean).obj X), f a ≠ y<VAR>C : Set ((forget Stonean).obj Y) := Set.range ⇑f<VAR>hC : IsClosed C<VAR>U : Set ((forget Stonean).obj Y) := Cᶜ<GOAL>False
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<VAR>hy : ∀ (a : (forget Stonean).obj X), f a ≠ y<VAR>C : Set ((forget Stonean).obj Y) := Set.range ⇑f<VAR>hC : IsClosed C<VAR>U : Set ((forget Stonean).obj Y) := Cᶜ<VAR>hUy : U ∈ 𝓝 y<GOAL>False
<VAR>X Y : Stonean<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>y : (forget Stonean).obj Y<VAR>hy : ∀ (a : (forget Stonean).obj X), f a ≠ y<VAR>C : Set ((forget Stonean).obj Y) := Set.range ⇑f<VAR>hC : IsClosed C<VAR>U : Set ((forget Stonean).obj Y) := Cᶜ<VAR>hUy : U ∈ 𝓝 y<VAR>V : Set ((forget Stonean).obj Y)<VAR>hV : V ∈ {s | IsClopen s}<VAR>hyV : y ∈ V<VAR>hVU : V ⊆ U<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>μ κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝² : IsSFiniteKernel μ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ : α<VAR>s✝ : Set (β × γ)<VAR>hs : MeasurableSet s✝<GOAL>(((μ + κ) ⊗ₖ η) a✝) s✝ = ((μ ⊗ₖ η + κ ⊗ₖ η) a✝) s✝
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a b : E<VAR>r r' : k<VAR>h : 0 < r<GOAL>a ≤ (lineMap a b) r ↔ (lineMap a b) 0 ≤ (lineMap a b) r
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>s : Set E<GOAL>μ (⇑(AffineMap.homothety x r) '' s) = μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s))
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>s : Set E<GOAL>μ (⇑(AffineMap.homothety x r) '' s) = μ ((fun x_1 => r • (x_1 - x) + x) '' s)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>s : Set E<GOAL>μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s)) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s
<VAR>α : Sort u_1<VAR>s : α → Prop<VAR>h : ∃ a, (fun b => a = b) = s<GOAL>(fun b => out ⟨s, h⟩ = b) = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ↥(Lp E p μ)<VAR>g : ↥(Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖<GOAL>‖f‖ ≤ ‖g‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ↥(Lp E p μ)<VAR>g : ↥(Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖<GOAL>eLpNorm (↑↑f) p μ ≤ eLpNorm (↑↑g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : AEMeasurable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>interior (closedBall x r) = ball x r
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<GOAL>interior (closedBall x 0) = ball x 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>interior (closedBall x r) = ball x r
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Set G<VAR>x✝ : G<GOAL>x✝ ∈ ↑(stabilizer G s) * s ↔ x✝ ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Set G<VAR>x✝ : G<GOAL>x✝ ∈ ↑(stabilizer G s) * s → x✝ ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>s : Set G<VAR>a : G<VAR>ha : a ∈ ↑(stabilizer G s)<VAR>b : G<VAR>hb : b ∈ s<GOAL>(fun x x_1 => x * x_1) a b ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>s : Set G<VAR>a : G<VAR>ha : a ∈ ↑(stabilizer G s)<VAR>b : G<VAR>hb : b ∈ s<GOAL>(fun x x_1 => x * x_1) a b ∈ a • s
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c u : αˣ<GOAL>Commute ↑a ↑a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : β × γ → α<VAR>c : α<GOAL>⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f (i, j) ≤ c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>x✝ : ℕ<GOAL>Disjoint (closure ((fun x => ∅) x✝)) s
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<VAR>h : a • S ≤ a • T<GOAL>S ≤ T
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → ↑Y.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → ↑Y.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → ↑Y.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>targetAffineLocally Q f
<VAR>F : Type u_1<VAR>inst✝ : NormedAddCommGroup F<VAR>g : ℝ → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Integrable (fun x => g (R * x)) volume ↔ Integrable g volume
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>h : ∅.Infinite<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖<VAR>x : α<GOAL>‖f x‖ ≤ 1 * ‖g x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖<VAR>x : α<GOAL>‖f x‖ ≤ ‖g x‖
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>⇑(coeff R 0) = ⇑(constantCoeff R)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>⇑(MvPowerSeries.coeff R 0) = ⇑(constantCoeff R)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → G<GOAL>↑‖∫ (a : α), f a ∂μ‖₊ ≤ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → G<GOAL>ENNReal.ofReal ‖∫ (a : α), f a ∂μ‖ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → G<GOAL>‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>iso'.hom.app X = iso'.hom.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫ R.symm.inverse.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.symm.inverse.obj X))) ≫ R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.symm.inverse.obj X))) ≫ R.inverse.map (B.map (L.counitIso.hom.app (L.symm.inverse.obj X)))) ≫ R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) = iso'.hom.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>R.functor.map (T.map (L.unitIso.hom.app X)) ≫ R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫ R.counitIso.hom.app (B.obj (L.functor.obj X)) = iso'.hom.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>(R.functor.map (T.map (L.unitIso.hom.app X)) ≫ R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫ R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) = iso'.hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>(R.functor.map (T.map (L.unitIso.hom.app X)) ≫ R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫ R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) = (T ⋙ R.functor).map (L.unitIso.hom.app X) ≫ (iso T L.functor R.functor B).hom.app ((L.functor ⋙ L.inverse).obj X)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>(R.functor.map (T.map (L.unitIso.hom.app X)) ≫ R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫ R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫ R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) = R.functor.map (T.map (L.unitIso.hom.app X)) ≫ (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.29733, u_5} C₅<VAR>inst✝ : Category.{?u.29737, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ≌ C₃<VAR>R : C₂ ≌ C₄<VAR>B : C₃ ⥤ C₄<VAR>h : CatCommSq T L.functor R.functor B<VAR>X : C₁<GOAL>R.functor.map (T.map (L.unitIso.hom.app X)) ≫ R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫ R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫ (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫ B.map (L.counitIso.hom.app (L.functor.obj X)) ≫ B.map (L.functor.map (L.unitIso.hom.app X)) = R.functor.map (T.map (L.unitIso.hom.app X)) ≫ (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))
<VAR>x : PartENat<VAR>n : ℕ<GOAL>(∃ (h : True → x.Dom), ∀ (hy : (↑n).Dom), x.get ⋯ ≤ (↑n).get hy) ↔ ∃ (h : x.Dom), x.get h ≤ n
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M<GOAL>(e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f
<VAR>X : Type u_1<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : BorelSpace X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>μ : Measure X<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ<VAR>inst✝² : μ.InnerRegularCompactLTTop<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<GOAL>μ k = ⨅ f, ⨅ (_ : Continuous f), ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : BorelSpace X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>μ : Measure X<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ<VAR>inst✝² : μ.InnerRegularCompactLTTop<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<GOAL>μ k ≤ ⨅ f, ⨅ (_ : Continuous f), ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : BorelSpace X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>μ : Measure X<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ<VAR>inst✝² : μ.InnerRegularCompactLTTop<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : RegularSpace X<GOAL>⨅ f, ⨅ (_ : Continuous f), ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ k
<VAR>V : Type u_1<VAR>V₁✝ : Type u_2<VAR>V₂✝ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : SeminormedAddCommGroup V₁✝<VAR>inst✝³ : SeminormedAddCommGroup V₂✝<VAR>inst✝² : SeminormedAddCommGroup V₃<VAR>f✝ g : NormedAddGroupHom V₁✝ V₂✝<VAR>V₁ : Type u_5<VAR>V₂ : Type u_6<VAR>inst✝¹ : NormedAddCommGroup V₁<VAR>inst✝ : NormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>hn : ‖f‖ = 0<VAR>x : V₁<GOAL>‖f‖ * ‖x‖ = 0
<VAR>V : Type u_1<VAR>V₁✝ : Type u_2<VAR>V₂✝ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : SeminormedAddCommGroup V₁✝<VAR>inst✝³ : SeminormedAddCommGroup V₂✝<VAR>inst✝² : SeminormedAddCommGroup V₃<VAR>f✝ g : NormedAddGroupHom V₁✝ V₂✝<VAR>V₁ : Type u_5<VAR>V₂ : Type u_6<VAR>inst✝¹ : NormedAddCommGroup V₁<VAR>inst✝ : NormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>hf : f = 0<GOAL>‖f‖ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : AddGroup α<VAR>a b : α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(Equiv.addRight a ^ n) x✝ = (Equiv.addRight (n • a)) x✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a * d + b * c ≤ a * c + b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hcd : c ≤ d<VAR>b : α<VAR>hab : a ≤ a + b<GOAL>a * d + (a + b) * c ≤ a * c + (a + b) * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a c : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>b : α<VAR>hab : a ≤ a + b<VAR>d : α<VAR>hcd : c ≤ c + d<GOAL>a * (c + d) + (a + b) * c ≤ a * c + (a + b) * (c + d)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a c : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>b : α<VAR>hab : a ≤ a + b<VAR>d : α<VAR>hcd : c ≤ c + d<GOAL>a * c + (a + b) * c + a * d ≤ a * c + (a + b) * c + (a + b) * d
<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✝ : μ.IsMulRightInvariant<VAR>g : G<GOAL>QuasiMeasurePreserving (fun h => g * h) μ μ
<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✝ : μ.IsMulRightInvariant<VAR>g : G<VAR>this : QuasiMeasurePreserving (fun h => h * g⁻¹) μ.inv.inv μ.inv.inv<GOAL>QuasiMeasurePreserving (fun h => g * h) μ μ
<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✝ : μ.IsMulRightInvariant<VAR>g : G<VAR>this : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ<GOAL>QuasiMeasurePreserving (fun h => g * h) μ μ