ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }<VAR>hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)<VAR>x : α<GOAL>(f.extendSubtype * σ) x = (τ * f.extendSubtype) x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ τ : Perm α<VAR>f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }<VAR>hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)<VAR>x : α<GOAL>f.extendSubtype (σ x) = τ (f.extendSubtype x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h✝ : x✝ ∈ closure s<VAR>x : R<VAR>hx : x ∈ ↑(Submonoid.closure s)<VAR>l : List R<VAR>hl : ∀ y ∈ l, y ∈ s<VAR>h : l.prod = x<GOAL>∀ y ∈ l, y ∈ s ∨ y = -1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝¹ : R<VAR>h : x✝¹ ∈ closure s<VAR>x : R<VAR>x✝ : (fun x => ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x) x<VAR>L : List (List R)<VAR>hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x<GOAL>∀ (head : List R) (tail : List (List R)), (List.map List.prod (List.map (List.cons (-1)) tail)).sum = -(List.map List.prod tail).sum → (List.map List.prod (List.map (List.cons (-1)) (head :: tail))).sum = -(List.map List.prod (head :: tail)).sum
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ : ℕ<VAR>χ : DirichletCharacter R n✝<VAR>n : ℕ<GOAL>conductor 1 ∣ n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ : ℕ<VAR>χ : DirichletCharacter R n✝<VAR>n : ℕ<GOAL>1 ∣ n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<GOAL>(map (fun t => X - C t) s).prod = ∑ j ∈ Finset.range (card s + 1), (-1) ^ j * (C (s.esymm j) * X ^ (card s - j))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<GOAL>(map (fun x => X + C (-x)) s).prod = ∑ j ∈ Finset.range (card s + 1), (-1) ^ j * (C (s.esymm j) * X ^ (card s - j))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<GOAL>(map (fun x => X + C (-x)) s).prod = (map (fun r => X + C r) (map (fun t => -t) s)).prod
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>s : Multiset R<GOAL>∑ j ∈ Finset.range (card s + 1), (-1) ^ j * (C (s.esymm j) * X ^ (card s - j)) = ∑ j ∈ Finset.range (card (map (fun t => -t) s) + 1), C ((map (fun t => -t) s).esymm j) * X ^ (card (map (fun t => -t) s) - j)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : ∃ f', HasFDerivAt f f' x<GOAL>HasFDerivAt f (fderiv 𝕜 f x) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : ∃ f', HasFDerivAt f f' x<GOAL>HasFDerivAt f (Classical.choose h) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>s t : Set E<GOAL>span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → ⟪u, v⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module S M<VAR>inst✝ : Module R M<VAR>n : ℤ<VAR>b : M<GOAL>((smulAddHom R M).flip b).comp (castAddHom R) = (smulAddHom ℤ M).flip b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module S M<VAR>inst✝ : Module R M<VAR>n : ℤ<VAR>b : M<GOAL>(((smulAddHom R M).flip b).comp (castAddHom R)) 1 = ((smulAddHom ℤ M).flip b) 1
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>n : ℕ<VAR>ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n + 1] t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>n : ℕ<VAR>ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set (α × α)<VAR>htU : t ∈ 𝓤 α<VAR>hts : t ○ t ⊆ s<GOAL>∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n + 1] t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>n : ℕ<VAR>ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set (α × α)<VAR>htU : t ∈ 𝓤 α<VAR>hts : t ○ t ⊆ s<VAR>U : Set (α × α)<VAR>hU : U ⊆ t ∧ (fun x => U ○ x)^[n] U ⊆ t<GOAL>U ⊆ s ∧ (fun x => U ○ x)^[n + 1] U ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>n : ℕ<VAR>ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set (α × α)<VAR>htU : t ∈ 𝓤 α<VAR>hts : t ○ t ⊆ s<VAR>U : Set (α × α)<VAR>hU : U ⊆ t ∧ (fun x => U ○ x)^[n] U ⊆ t<GOAL>U ⊆ s ∧ U ○ (fun x => U ○ x)^[n] U ⊆ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ s.direction ↔ ∃ p2 ∈ s, v = p -ᵥ p2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ (fun x => p -ᵥ x) '' ↑s ↔ ∃ p2 ∈ s, v = p -ᵥ p2
<VAR>x y : ℂ<GOAL>sinh x + cosh x = cexp x
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>m : Multiset M<VAR>comm : {x | x ∈ m}.Pairwise Commute<VAR>h : ∀ x ∈ m, x ∈ S<GOAL>m.noncommProd comm ∈ S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>l : List M<VAR>comm : {x | x ∈ ⟦l⟧}.Pairwise Commute<VAR>h : ∀ x ∈ ⟦l⟧, x ∈ S<GOAL>Multiset.noncommProd ⟦l⟧ comm ∈ S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>l : List M<VAR>comm : {x | x ∈ ⟦l⟧}.Pairwise Commute<VAR>h : ∀ x ∈ ⟦l⟧, x ∈ S<GOAL>l.prod ∈ S
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>f : H →* G<VAR>hf : IsPGroup p ↥f.ker<VAR>inst✝ : Finite (Sylow p G)<VAR>h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P => exists_comap_eq_of_ker_isPGroup P hf<VAR>g : Sylow p H → Sylow p G := fun P => Classical.choose ⋯<VAR>hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P<VAR>P Q : Sylow p H<VAR>h : g P = g Q<GOAL>comap f ↑(g Q) = ↑Q
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x y : L<VAR>h : x ∈ I<GOAL>⁅x, y⁆ ∈ I
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x y : L<VAR>h : x ∈ I<GOAL>⁅-y, x⁆ ∈ I
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x y : L<VAR>h : x ∈ I<GOAL>x ∈ I
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H₁ H₂ : Subgroup G<VAR>h : Disjoint H₁ H₂<VAR>x y : ↥H₁ × ↥H₂<VAR>hxy : (fun g => ↑g.1 * ↑g.2) x = (fun g => ↑g.1 * ↑g.2) y<GOAL>x = y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H₁ H₂ : Subgroup G<VAR>h : Disjoint H₁ H₂<VAR>x y : ↥H₁ × ↥H₂<VAR>hxy : (↑y.1)⁻¹ * ↑x.1 * (↑x.2 * (↑y.2)⁻¹) = 1<GOAL>x = y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H₁ H₂ : Subgroup G<VAR>h : Disjoint H₁ H₂<VAR>x y : ↥H₁ × ↥H₂<VAR>hxy : ↑(y.1⁻¹ * x.1) = 1 ∧ ↑(x.2 * y.2⁻¹) = 1<GOAL>x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis b<VAR>x y : X<VAR>h : ∀ s ∈ b, x ∈ s ↔ y ∈ s<GOAL>(𝓝 y).HasBasis (fun t => t ∈ b ∧ x ∈ t) fun t => t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis b<VAR>x y : X<VAR>h : ∀ s ∈ b, x ∈ s ↔ y ∈ s<VAR>x✝ : Set X<GOAL>x✝ ∈ b ∧ x ∈ x✝ ↔ x✝ ∈ b ∧ y ∈ x✝
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hd : p.degree = q.degree<VAR>hp0 : p ≠ 0<VAR>hlc : p.leadingCoeff = q.leadingCoeff<VAR>hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p<VAR>hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q<VAR>hd' : p.natDegree = q.natDegree<VAR>hq0 : q ≠ 0<GOAL>(p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<GOAL>x ≤ y ↔ ReflTransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>x : A<VAR>φ : ↑(characterSpace ℂ ↥(elementalStarAlgebra ℂ x))<GOAL>φ ⟨x, ⋯⟩ ∈ spectrum ℂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>x y z : Ordinal.{u_4}<GOAL>(x * y + z) % x = z % x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>y z : Ordinal.{u_4}<GOAL>(0 * y + z) % 0 = z % 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>x y z : Ordinal.{u_4}<VAR>hx : x ≠ 0<GOAL>(x * y + z) % x = z % x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x y z : M<GOAL>z ∈ span R {x, y} ↔ ∃ a b, a • x + b • y = z
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ∆ a = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : ∀ t ∈ 𝒜, a ∉ t<VAR>ht : 𝒜.Shatters t<GOAL>a ∉ t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : ∀ t ∈ 𝒜, a ∉ t<VAR>ht : 𝒜.Shatters t<VAR>u : Finset α<VAR>hu : u ∈ 𝒜<VAR>htu : t ⊆ u<GOAL>a ∉ t
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : (fun x x_1 => x + x_1) (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a)) (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - c)) = (fun x x_1 => x + x_1) p p<GOAL>toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - a) + toIocMod hp 0 (b - c)) = p + p<GOAL>toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) = 2 • p<GOAL>toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : min (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c)) (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) ≤ p<GOAL>toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p<GOAL>toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p<GOAL>toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p<GOAL>toIcoMod hp 0 (b - c) ≤ toIocMod hp 0 (b - c)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<VAR>this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p<GOAL>toIcoMod hp 0 (b - a) ≤ toIocMod hp 0 (b - a)
<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 α<GOAL>f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝⁴ : Mul α✝<VAR>inst✝³ : Mul β✝<VAR>γ : Type u_1<VAR>inst✝² : Mul γ<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Semigroup α<VAR>inst✝ : CommSemigroup β<VAR>f g : α → β<VAR>hf : IsMulHom f<VAR>hg : IsMulHom g<VAR>a b : α<GOAL>f (a * b) * g (a * b) = f a * g a * (f b * g b)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl L<GOAL>ConnectedComponent.map (induceHom Hom.id ⋯) C = C
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u_2}<GOAL>c.ord.cof ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<GOAL>eLpNorm ({x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊}.indicator (f i)) p μ = eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}<GOAL>eLpNorm ({x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊}.indicator (f i)) p μ = eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}<GOAL>eLpNorm (fun x => ‖{x | C ≤ ‖f i x‖}.indicator (f i) x‖) p μ = eLpNorm (fun x => ‖{x | C ≤ ↑‖f j x‖₊}.indicator (f j) x‖) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hι : Nonempty ι<VAR>C : ℝ<VAR>hC₁ : 0 < C<VAR>hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}<GOAL>eLpNorm (fun x => {x | C ≤ ‖f i x‖}.indicator (fun a => ‖f i a‖) x) p μ = eLpNorm (fun x => {x | C ≤ ‖f j x‖}.indicator (fun a => ‖f j a‖) x) p μ