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>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : Nonempty ι<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedSpace ℝ 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : IsScalarTower ℝ 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>this : TopologicalAddGroup E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ p.basisSets) id
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : Nonempty ι<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : NormedSpace ℝ 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : IsScalarTower ℝ 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>this : TopologicalAddGroup E<GOAL>∀ i ∈ p.basisSets, Convex ℝ (id i)
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ S<VAR>I : Ideal S<VAR>bI : Basis ι ℤ ↥I<VAR>e : S ≃ₗ[ℤ] ↥I := b.equiv bI (Equiv.refl ι)<GOAL>(b.det (Subtype.val ∘ ⇑bI)).natAbs = absNorm I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>K K' : ℝ≥0<VAR>f : α → β<VAR>g : β → γ<VAR>hg : LipschitzWith K g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<GOAL>Integrable (g ∘ f) μ ↔ Integrable f μ
<VAR>α : Type ?u.2288<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>↑((fun s => ⟨(s.inf, s.sup), ⋯⟩) s(a, b)) = (a, b) ∨ ↑((fun s => ⟨(s.inf, s.sup), ⋯⟩) s(a, b)) = (a, b).swap
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>c n : ℤ<VAR>x a : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : c * n = n'<VAR>h₂ : smulg c a = a'<GOAL>smulg c (termg n x a) = termg n' x a'
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>S : Type u_1<VAR>inst✝ : CommSemiring S<VAR>x y : S<VAR>I : Ideal S<GOAL>x ∈ span {y} ⊔ I ↔ ∃ a, ∃ b ∈ I, a * y + b = x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>S : Type u_1<VAR>inst✝ : CommSemiring S<VAR>x y : S<VAR>I : Ideal S<GOAL>(∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) ↔ ∃ a, ∃ b ∈ I, a * y + b = x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → Preorder (α i)<VAR>x y✝ y : (i : ι) → α i<GOAL>(y ∈ univ.pi fun i => Iic (x i)) ↔ y ∈ Iic x
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>o.oangle x (-y) = o.oangle x y + ↑π
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(-(o.kahler x) y).arg = ↑((o.kahler x) y).arg + ↑π
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm f q μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm f q μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm f q μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<VAR>hq_top : ¬q = ⊤<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm f q μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<VAR>hq_top : ¬q = ⊤<VAR>hq0 : q ≠ 0<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm f q μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<VAR>hq_top : ¬q = ⊤<VAR>hq0 : q ≠ 0<VAR>hpq_real : p.toReal ≤ q.toReal<GOAL>eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm f q μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<VAR>hq_top : ¬q = ⊤<VAR>hq0 : q ≠ 0<VAR>hpq_real : p.toReal ≤ q.toReal<GOAL>eLpNorm' f p.toReal μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f✝ : α → E<VAR>p q : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hpq : p ≤ q<VAR>hfq_m : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm' f q.toReal μ < ⊤<VAR>hp0 : p ≠ 0<VAR>hp_top : ¬p = ⊤<VAR>hp_pos : 0 < p.toReal<VAR>hq_top : ¬q = ⊤<VAR>hq0 : q ≠ 0<VAR>hpq_real : p.toReal ≤ q.toReal<GOAL>eLpNorm' f p.toReal μ < ⊤
<VAR>ι : Type u_1<VAR>I : Box ι<VAR>inst✝ : Fintype ι<GOAL>↑I =ᶠ[ae volume] Box.Icc I
<VAR>ι : Type u_1<VAR>I : Box ι<VAR>inst✝ : Fintype ι<GOAL>(univ.pi fun i => Ioc (I.lower i) (I.upper i)) =ᶠ[ae volume] Box.Icc I
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : T<VAR>m : M<VAR>s : ↥S<VAR>n : M<VAR>t : ↥S<GOAL>x • (mk m s + mk n t) = x • mk m s + x • mk n t
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : T<VAR>m : M<VAR>s : ↥S<VAR>n : M<VAR>t : ↥S<GOAL>x • mk (t • m + s • n) (s * t) = mk (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m + ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n) ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : T<VAR>m : M<VAR>s : ↥S<VAR>n : M<VAR>t : ↥S<GOAL>IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • mk (t • m + s • n) (s * t) = mk (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m + ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n) ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : T<VAR>m : M<VAR>s : ↥S<VAR>n : M<VAR>t : ↥S<GOAL>mk (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n)) ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)) = mk (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m + ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n) ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>i✝ j✝ : n<VAR>t_hij : i✝ ≠ j✝<VAR>c✝ : R<GOAL>{ i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Setoid α)<GOAL>sSup S = EqvGen.Setoid fun x y => ∃ r ∈ S, r.Rel x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Setoid α)<GOAL>sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r.Rel x y) → s.Rel x y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Setoid α)<GOAL>upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r.Rel x y) → s.Rel x y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Setoid α)<GOAL>{x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a.Rel x_1 y → x.Rel x_1 y} = {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1.Rel x y → s.Rel x y}
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonAssocSemiring α<VAR>inst✝¹ : Fintype n<VAR>L : Matrix m n α<VAR>M : Matrix n o α<VAR>inst✝ : NonAssocSemiring β<VAR>f : α →+* β<VAR>i✝ : m<VAR>j✝ : o<GOAL>(L * M).map (⇑f) i✝ j✝ = (L.map ⇑f * M.map ⇑f) i✝ j✝
<VAR>n m : ℕ<GOAL>m ^^^ n ^^^ n = m
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>T0Space α ↔ ∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<VAR>hz : z ∈ U<GOAL>Tendsto (fun s => ∑ b ∈ s, deriv (F b) z) atTop (𝓝 (deriv (fun w => ∑' (i : ι), F i w) z))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<VAR>hz : z ∈ U<VAR>hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U<GOAL>Tendsto (fun s => ∑ b ∈ s, deriv (F b) z) atTop (𝓝 (deriv (fun w => ∑' (i : ι), F i w) z))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<VAR>hz : z ∈ U<VAR>hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U<GOAL>(fun s => ∑ b ∈ s, deriv (F b) z) = fun i => (deriv ∘ fun t x => ∑ n ∈ t, F n x) i z
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<VAR>hz : z ∈ U<VAR>hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U<VAR>s : Finset ι<GOAL>∑ b ∈ s, deriv (F b) z = (deriv ∘ fun t x => ∑ n ∈ t, F n x) s z
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<VAR>μ : Measure α<GOAL>AEMeasurable (g ∘ f) μ ↔ AEMeasurable 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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<VAR>μ : Measure α<VAR>H : AEMeasurable (g ∘ f) μ<GOAL>AEMeasurable 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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ✝ ν : Measure α<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<VAR>μ : Measure α<VAR>H : AEMeasurable (g ∘ f) μ<GOAL>AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : IsEmpty α<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : ε ≤ 0<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : Fintype.card α ≤ l<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P✝ : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<VAR>P : Finpartition univ<VAR>hP₁ : P.IsEquipartition<VAR>hP₂ : l ≤ P.parts.card<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) l<VAR>hP₄ : P.IsUniform G (ε / 8)<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P✝ : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<VAR>P : Finpartition univ<VAR>hP₁ : P.IsEquipartition<VAR>hP₂ : l ≤ P.parts.card<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) l<VAR>hP₄ : P.IsUniform G (ε / 8)<VAR>this : 4 / ε ≤ ↑P.parts.card<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P✝ : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<VAR>P : Finpartition univ<VAR>hP₁ : P.IsEquipartition<VAR>hP₂ : l ≤ P.parts.card<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) l<VAR>hP₄ : P.IsUniform G (ε / 8)<VAR>this : 4 / ε ≤ ↑P.parts.card<VAR>k : 2 * (↑G.edgeFinset.card - ↑(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card) < 2 * ε * ↑(Fintype.card α ^ 2)<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P✝ : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<VAR>P : Finpartition univ<VAR>hP₁ : P.IsEquipartition<VAR>hP₂ : l ≤ P.parts.card<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) l<VAR>hP₄ : P.IsUniform G (ε / 8)<VAR>this : 4 / ε ≤ ↑P.parts.card<VAR>k : 2 * (↑G.edgeFinset.card - ↑(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card) < 2 * (ε * ↑(Fintype.card α ^ 2))<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P✝ : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<VAR>P : Finpartition univ<VAR>hP₁ : P.IsEquipartition<VAR>hP₂ : l ≤ P.parts.card<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) l<VAR>hP₄ : P.IsUniform G (ε / 8)<VAR>this : 4 / ε ≤ ↑P.parts.card<VAR>k : ↑G.edgeFinset.card - ↑(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card < ε * ↑(Fintype.card α ^ 2)<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t✝ : Finset α<VAR>P✝ : Finpartition univ<VAR>ε : ℝ<VAR>hG : G.FarFromTriangleFree ε<VAR>h✝ : Nonempty α<VAR>hε : 0 < ε<VAR>l : ℕ := ⌈4 / ε⌉₊<VAR>hl : 4 / ε ≤ ↑l<VAR>hl' : l ≤ Fintype.card α<VAR>P : Finpartition univ<VAR>hP₁ : P.IsEquipartition<VAR>hP₂ : l ≤ P.parts.card<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) l<VAR>hP₄ : P.IsUniform G (ε / 8)<VAR>this : 4 / ε ≤ ↑P.parts.card<VAR>k : ↑G.edgeFinset.card - ↑(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card < ε * ↑(Fintype.card α ^ 2)<VAR>t : Finset α<VAR>ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Group α<VAR>inst✝³ : MulAction α β<VAR>inst✝² : ContinuousInv α<VAR>inst✝¹ : ContinuousSMul α β<VAR>s : Set α<VAR>t✝ : Set β<VAR>inst✝ : CompactSpace α<VAR>t : Set β<VAR>ht : IsClosed t<GOAL>IsClosed (Quotient.mk' '' t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Group α<VAR>inst✝³ : MulAction α β<VAR>inst✝² : ContinuousInv α<VAR>inst✝¹ : ContinuousSMul α β<VAR>s : Set α<VAR>t✝ : Set β<VAR>inst✝ : CompactSpace α<VAR>t : Set β<VAR>ht : IsClosed t<GOAL>IsClosed (⋃ g, (fun x => g • x) '' t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Group α<VAR>inst✝³ : MulAction α β<VAR>inst✝² : ContinuousInv α<VAR>inst✝¹ : ContinuousSMul α β<VAR>s : Set α<VAR>t✝ : Set β<VAR>inst✝ : CompactSpace α<VAR>t : Set β<VAR>ht : IsClosed t<GOAL>⋃ g, (fun x => g • x) '' t = univ • t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Group α<VAR>inst✝³ : MulAction α β<VAR>inst✝² : ContinuousInv α<VAR>inst✝¹ : ContinuousSMul α β<VAR>s : Set α<VAR>t✝ : Set β<VAR>inst✝ : CompactSpace α<VAR>t : Set β<VAR>ht : IsClosed t<GOAL>⋃ x ∈ univ, (fun x_1 => x • x_1) '' t = ⋃ a ∈ univ, a • t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<VAR>hi : i = 0<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) = X.map (SimplexCategory.σ (j.castLT ⋯)) ≫ X.map (SimplexCategory.δ (i.pred ⋯))
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<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 F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae (μ.trim hm)] ↑↑(-lpMeasSubgroupToLpTrim F p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<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 F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae (μ.trim hm)] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)