ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G' : Type u_1<VAR>inst✝¹⁰ : AddGroup G'<VAR>inst✝⁹ : MeasurableSpace G'<VAR>inst✝⁸ : TopologicalSpace G'<VAR>inst✝⁷ : TopologicalAddGroup G'<VAR>inst✝⁶ : BorelSpace G'<VAR>μ' : Measure G'<VAR>Γ' : AddSubgroup G'<VAR>inst✝⁵ : Countable ↥Γ'<VAR>inst✝⁴ : MeasurableSpace (G' ⧸ Γ')<VAR>inst✝³ : BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))<VAR>h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<VAR>π : G' → G' ⧸ Γ' := mk<VAR>meas_π : Measurable π<GOAL>∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')
<VAR>G' : Type u_1<VAR>inst✝¹⁰ : AddGroup G'<VAR>inst✝⁹ : MeasurableSpace G'<VAR>inst✝⁸ : TopologicalSpace G'<VAR>inst✝⁷ : TopologicalAddGroup G'<VAR>inst✝⁶ : BorelSpace G'<VAR>μ' : Measure G'<VAR>Γ' : AddSubgroup G'<VAR>inst✝⁵ : Countable ↥Γ'<VAR>inst✝⁴ : MeasurableSpace (G' ⧸ Γ')<VAR>inst✝³ : BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))<VAR>h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<VAR>π : G' → G' ⧸ Γ' := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<GOAL>∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')
<VAR>G' : Type u_1<VAR>inst✝¹⁰ : AddGroup G'<VAR>inst✝⁹ : MeasurableSpace G'<VAR>inst✝⁸ : TopologicalSpace G'<VAR>inst✝⁷ : TopologicalAddGroup G'<VAR>inst✝⁶ : BorelSpace G'<VAR>μ' : Measure G'<VAR>Γ' : AddSubgroup G'<VAR>inst✝⁵ : Countable ↥Γ'<VAR>inst✝⁴ : MeasurableSpace (G' ⧸ Γ')<VAR>inst✝³ : BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))<VAR>h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<VAR>π : G' → G' ⧸ Γ' := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<GOAL>∫ (x : G'), g (π x) * f x ∂μ' = ∫ (x : G' ⧸ Γ'), automorphize (g ∘ π * f) x ∂Measure.map mk (μ'.restrict 𝓕')
<VAR>G' : Type u_1<VAR>inst✝¹⁰ : AddGroup G'<VAR>inst✝⁹ : MeasurableSpace G'<VAR>inst✝⁸ : TopologicalSpace G'<VAR>inst✝⁷ : TopologicalAddGroup G'<VAR>inst✝⁶ : BorelSpace G'<VAR>μ' : Measure G'<VAR>Γ' : AddSubgroup G'<VAR>inst✝⁵ : Countable ↥Γ'<VAR>inst✝⁴ : MeasurableSpace (G' ⧸ Γ')<VAR>inst✝³ : BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))<VAR>h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<VAR>π : G' → G' ⧸ Γ' := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<VAR>H₁ : Integrable (g ∘ π * f) μ'<GOAL>∫ (x : G'), g (π x) * f x ∂μ' = ∫ (x : G' ⧸ Γ'), automorphize (g ∘ π * f) x ∂Measure.map mk (μ'.restrict 𝓕')
<VAR>G' : Type u_1<VAR>inst✝¹⁰ : AddGroup G'<VAR>inst✝⁹ : MeasurableSpace G'<VAR>inst✝⁸ : TopologicalSpace G'<VAR>inst✝⁷ : TopologicalAddGroup G'<VAR>inst✝⁶ : BorelSpace G'<VAR>μ' : Measure G'<VAR>Γ' : AddSubgroup G'<VAR>inst✝⁵ : Countable ↥Γ'<VAR>inst✝⁴ : MeasurableSpace (G' ⧸ Γ')<VAR>inst✝³ : BorelSpace (G' ⧸ Γ')<VAR>𝓕' : Set G'<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ'.IsAddRightInvariant<VAR>f : G' → K<VAR>f_ℒ_1 : Integrable f μ'<VAR>g : G' ⧸ Γ' → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ'.restrict 𝓕')) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))<VAR>h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'<VAR>π : G' → G' ⧸ Γ' := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<VAR>H₁ : Integrable (g ∘ π * f) μ'<VAR>H₂ : AEStronglyMeasurable (automorphize (g ∘ π * f)) (Measure.map mk (μ'.restrict 𝓕'))<GOAL>∫ (x : G'), g (π x) * f x ∂μ' = ∫ (x : G' ⧸ Γ'), automorphize (g ∘ π * f) x ∂Measure.map mk (μ'.restrict 𝓕')
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>n₁ /. ↑d₁ + n₂ /. ↑d₂ + n₃ /. ↑d₃ = n₁ /. ↑d₁ + (n₂ /. ↑d₂ + n₃ /. ↑d₃)
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>((n₁ * ↑d₂ + n₂ * ↑d₁) * ↑d₃ + n₃ * (↑d₁ * ↑d₂)) /. (↑d₁ * ↑d₂ * ↑d₃) = (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ + n₃ * ↑d₂) * ↑d₁) /. (↑d₁ * (↑d₂ * ↑d₃))
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>(n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂))) /. (↑d₁ * (↑d₂ * ↑d₃)) = (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁)) /. (↑d₁ * (↑d₂ * ↑d₃))
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>h : Disjoint s t<GOAL>G.edgeDensity s t + Gᶜ.edgeDensity s t = 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>h : Disjoint s t<GOAL>↑(G.interedges s t).card + ↑(Gᶜ.interedges s t).card = ↑s.card * ↑t.card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>h : Disjoint s t<GOAL>↑s.card * ↑t.card ≠ 0
<VAR>R : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>α : Type u_4<VAR>γ : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : AddGroup α<VAR>inst✝⁵ : Monoid γ<VAR>inst✝⁴ : MulAction γ α<VAR>inst✝³ : SMul R γ<VAR>inst✝² : SMul R α<VAR>inst✝¹ : IsScalarTower R γ α<VAR>inst✝ : SlashAction β G α γ<VAR>k : β<VAR>g : G<VAR>a : α<VAR>r : R<GOAL>(r • a) ∣[k;γ] g = r • a ∣[k;γ] g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<GOAL>(p - q).natDegree = (q - p).natDegree
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X✝ Y✝ : W.FunctorsInverting D<VAR>τ : X✝ ⟶ Y✝<GOAL>W.Q ⋙ (fun G => lift G.obj ⋯) X✝ = X✝.obj
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X✝ Y✝ : W.FunctorsInverting D<VAR>τ : X✝ ⟶ Y✝<GOAL>Y✝.obj = W.Q ⋙ (fun G => lift G.obj ⋯) Y✝
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>G : W.FunctorsInverting D<GOAL>𝟙 W.Q ◫ { obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.map (𝟙 G) = 𝟙 W.Q ◫ 𝟙 ({ obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.obj G)
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>G : W.FunctorsInverting D<GOAL>eqToHom ⋯ ≫ 𝟙 G ≫ eqToHom ⋯ = 𝟙 W.Q ◫ 𝟙 ({ obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.obj G)
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>G : W.FunctorsInverting D<VAR>X : C<GOAL>(eqToHom ⋯ ≫ 𝟙 G ≫ eqToHom ⋯).app X = (𝟙 W.Q ◫ 𝟙 ({ obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.obj G)).app X
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>G : W.FunctorsInverting D<VAR>X : C<GOAL>(𝟙 G).app X = 𝟙 ((lift G.obj ⋯).obj (W.Q.obj X))
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X✝ Y✝ Z✝ : W.FunctorsInverting D<VAR>τ₁ : X✝ ⟶ Y✝<VAR>τ₂ : Y✝ ⟶ Z✝<VAR>X : C<GOAL>(𝟙 W.Q ◫ { obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.map (τ₁ ≫ τ₂)).app X = (𝟙 W.Q ◫ ({ obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.map τ₁ ≫ { obj := fun G => lift G.obj ⋯, map := fun {X Y} τ => natTransExtension (eqToHom ⋯ ≫ τ ≫ eqToHom ⋯) }.map τ₂)).app X
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>X✝ Y✝ Z✝ : W.FunctorsInverting D<VAR>τ₁ : X✝ ⟶ Y✝<VAR>τ₂ : Y✝ ⟶ Z✝<VAR>X : C<GOAL>(τ₁ ≫ τ₂).app X = τ₁.app X ≫ τ₂.app X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>hs : IsLowerSet s<GOAL>Disjoint s ↑(upperClosure t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x‖₊ ∂μ = (∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ * ↑‖x‖₊ ∂μ = (∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>Measurable fun a => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Monoid G<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : Module k V<VAR>ρ : Representation k G V<VAR>g : G<VAR>r : k<GOAL>ρ.asAlgebraHom (Finsupp.single g r) = r • ρ g
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : F →ₗ[𝕜] E<VAR>hf : Function.Surjective ⇑f<GOAL>IsOpenMap ⇑f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : F →ₗ[𝕜] E<VAR>hf : Function.Surjective ⇑f<VAR>g : E →ₗ[𝕜] F<VAR>hg : f ∘ₗ g = id<GOAL>IsOpenMap ⇑f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : F →ₗ[𝕜] E<VAR>hf : Function.Surjective ⇑f<VAR>g : E →ₗ[𝕜] F<VAR>hg : f ∘ₗ g = id<VAR>x : F<GOAL>ContinuousAt (fun y => g (y - f x) + x) (f x)
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : F →ₗ[𝕜] E<VAR>hf : Function.Surjective ⇑f<VAR>g : E →ₗ[𝕜] F<VAR>hg : f ∘ₗ g = id<VAR>x : F<GOAL>(fun y => g (y - f x) + x) (f x) = x
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁷ : AddCommGroup E<VAR>inst✝¹⁶ : Module 𝕜 E<VAR>inst✝¹⁵ : TopologicalSpace E<VAR>inst✝¹⁴ : TopologicalAddGroup E<VAR>inst✝¹³ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝¹² : AddCommGroup F<VAR>inst✝¹¹ : Module 𝕜 F<VAR>inst✝¹⁰ : TopologicalSpace F<VAR>inst✝⁹ : TopologicalAddGroup F<VAR>inst✝⁸ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : T2Space E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : F →ₗ[𝕜] E<VAR>hf : Function.Surjective ⇑f<VAR>g : E →ₗ[𝕜] F<VAR>hg : f ∘ₗ g = id<VAR>x : F<VAR>y : E<GOAL>f ((fun y => g (y - f x) + x) y) = y
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f : P.B a ⟹ α<VAR>i : Fin2 n<VAR>x : α i<GOAL>x ∈ supp ⟨a, f⟩ i ↔ x ∈ f i '' univ
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f : P.B a ⟹ α<VAR>i : Fin2 n<VAR>x : α i<GOAL>(∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x) ↔ ∃ y, f i y = x
<VAR>V : Type (u + 1)<VAR>inst✝³ : LargeCategory V<VAR>G✝ : MonCat<VAR>W : Type (u + 1)<VAR>inst✝² : LargeCategory W<VAR>inst✝¹ : MonoidalCategory V<VAR>inst✝ : MonoidalCategory W<VAR>F : LaxMonoidalFunctor V W<VAR>G : MonCat<VAR>g : ↑G<GOAL>𝟙 (𝟙_ W) ≫ F.ε = F.ε ≫ F.map (𝟙 (𝟙_ V))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>X₁ X₂ S : C<VAR>f₁ : X₁ ⟶ S<VAR>f₂ : X₂ ⟶ S<VAR>inst✝¹ : HasPullback f₁ f₂<VAR>inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)<VAR>x : (forget C).obj (pullback f₁ f₂)<GOAL>∃ x₁ x₂, ∃ (h : f₁ x₁ = f₂ x₂), x = pullbackMk f₁ f₂ x₁ x₂ h
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>X₁ X₂ S : C<VAR>f₁ : X₁ ⟶ S<VAR>f₂ : X₂ ⟶ S<VAR>inst✝¹ : HasPullback f₁ f₂<VAR>inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)<VAR>x₁ : (forget C).obj X₁<VAR>x₂ : (forget C).obj X₂<VAR>h : f₁ (x₁, x₂).1 = f₂ (x₁, x₂).2<GOAL>∃ x₁_1 x₂_1, ∃ (h_1 : f₁ x₁_1 = f₂ x₂_1), (pullbackEquiv f₁ f₂).symm ⟨(x₁, x₂), h⟩ = pullbackMk f₁ f₂ x₁_1 x₂_1 h_1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<VAR>h : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<VAR>h : ∃ a, ∀ b ≥ a, r * ‖f b‖ ≤ ‖f (b + 1)‖<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<VAR>N : ℕ<VAR>hNN₀ : N₀ ≤ N<VAR>hN : ‖f N‖ ≠ 0<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<VAR>N : ℕ<VAR>hNN₀ : N₀ ≤ N<VAR>hN : ‖f N‖ ≠ 0<GOAL>¬Summable fun n => f (n + N)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<VAR>N : ℕ<VAR>hNN₀ : N₀ ≤ N<VAR>hN : ‖f N‖ ≠ 0<VAR>h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)<GOAL>Tendsto ((fun a => ‖a‖) ∘ fun n => f (n + N)) atTop atTop
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<VAR>N : ℕ<VAR>hNN₀ : N₀ ≤ N<VAR>hN : ‖f N‖ ≠ 0<VAR>h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)<GOAL>0 < ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>r : ℝ<VAR>hr : 1 < r<VAR>hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖<VAR>N : ℕ<VAR>hNN₀ : N₀ ≤ N<VAR>hN : ‖f N‖ ≠ 0<VAR>h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)<GOAL>∀ (n : ℕ), r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) n ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (n + 1)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : Nonempty β<VAR>f : β → α<VAR>hf : Continuous f<VAR>hlim : Tendsto f (cocompact β) atTop<VAR>inhabited_h : Inhabited β<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.438256, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>X Y : HomologicalComplex C (ComplexShape.up ℤ)<VAR>f : { as := X } ⟶ { as := Y }<GOAL>∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.438256, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>X Y : HomologicalComplex C (ComplexShape.up ℤ)<VAR>f : X ⟶ Y<GOAL>∃ Z g h, Triangle.mk ((quotient C (ComplexShape.up ℤ)).map f) g h ∈ distinguishedTriangles C