ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>∀ (j : K), t.ι.app j ≫ Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s) ≫ P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t) = t.ι.app j ≫ 𝟙 t.pt
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>g : Y → Z<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>f : PartialHomeomorph X Y<VAR>hx : x ∈ f.source<VAR>hf : IsLocalHomeomorph ↑f<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn (↑f) U
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<GOAL>Disjoint I (orthogonal Φ hΦ_inv I)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<GOAL>I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<GOAL>I = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<VAR>x : ↥I<VAR>y : ↥I<GOAL>⁅↑x, ↑y⁆ ∈ ↑⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<VAR>x : ↥I<VAR>y : ↥I<GOAL>⁅↑x, ↑y⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<VAR>x : ↥I<VAR>y : ↥I<VAR>z : L<GOAL>(Φ ⁅↑x, ↑y⁆) z = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<VAR>x : ↥I<VAR>y : ↥I<VAR>z : L<GOAL>(Φ ↑y) ⁅↑x, z⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ✝ : LinearMap.BilinForm R M<VAR>hΦ_nondeg✝ : Φ✝.Nondegenerate<VAR>hΦ_inv✝ : LinearMap.BilinForm.lieInvariant L Φ✝<VAR>Φ : LinearMap.BilinForm R L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>contra : I ≤ orthogonal Φ hΦ_inv I<VAR>x : ↥I<VAR>y : ↥I<VAR>z : L<VAR>hyz : ⁅↑x, z⁆ ∈ I<GOAL>(Φ ↑y) ⁅↑x, z⁆ = 0
<VAR>b x : Bool<VAR>l : List Bool<VAR>h : Chain (fun x x_1 => x ≠ x_1) b (x :: l)<GOAL>count (!b) (x :: l) = count b (x :: l) + (x :: l).length % 2
<VAR>x : Bool<VAR>l : List Bool<VAR>h : Chain (fun x x_1 => x ≠ x_1) (!x) (x :: l)<GOAL>count (!!x) (x :: l) = count (!x) (x :: l) + (x :: l).length % 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<GOAL>μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<VAR>hs_univ : ⋃ i, s i = univ<GOAL>μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<VAR>hs_univ : ⋃ i, s i = univ<VAR>hs_meas : ∀ (i : ℕ), MeasurableSet (s i)<GOAL>μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<VAR>hs_univ : ⋃ i, s i = univ<VAR>hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ<GOAL>μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<VAR>hs_univ : ⋃ i, s i = univ<VAR>hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ<VAR>h_univ_empty : ¬univ = ∅<GOAL>μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<VAR>hs_univ : ⋃ i, s i = univ<VAR>hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ<VAR>h_univ_empty : ¬univ = ∅<VAR>i : ℕ<VAR>hsi : s i = univ<GOAL>μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>μ : Measure α<VAR>h this : SigmaFinite μ<VAR>s : ℕ → Set α := spanningSets μ<VAR>hs_univ : ⋃ i, s i = univ<VAR>hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ<VAR>h_univ_empty : ¬univ = ∅<VAR>i : ℕ<VAR>hsi : s i = univ<GOAL>μ (s i) < ⊤
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J✝ : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I J : FractionalIdeal S P<VAR>x : P<VAR>hx : x ∈ I * J<GOAL>x ∈ ↑I * ↑J
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure (X ∩ M.E) = M.closure X
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>S : ι → Submonoid M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>H✝ H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<GOAL>H.toLieSubmodule.normalizer = H.toLieSubmodule
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S✝ : IntermediateField K L<VAR>S : Subalgebra K L<VAR>hS : IsField ↥S<VAR>x✝ : L<GOAL>x✝ ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x✝ ∈ S
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>hx : ¬‖x‖ = 0<GOAL>Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : σ →₀ ℕ<VAR>c : R<GOAL>((monomial s) c).totalDegree ≤ s.sum fun x => id
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : DecidableEq R<VAR>hp : p ≠ 0<GOAL>↑(normUnit p) = C p.leadingCoeff⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : DecidableEq R<VAR>hp : p ≠ 0<VAR>this : p.leadingCoeff ≠ 0<GOAL>↑(normUnit p) = C p.leadingCoeff⁻¹
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : Mul G<VAR>inst✝ : IsLeftCancelMul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>hr : ∀ (y : k), r * y = 0 ↔ y = 0<VAR>x : G<GOAL>(single x r * f).support = map (mulLeftEmbedding x) f.support
<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>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : CompleteSpace 𝕜<VAR>E : Type u_6<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<GOAL>Integrable (fun x => f x • c) μ ↔ Integrable f μ
<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>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : CompleteSpace 𝕜<VAR>E : Type u_6<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<GOAL>AEStronglyMeasurable f μ → (∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ < ⊤ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤)
<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>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : CompleteSpace 𝕜<VAR>E : Type u_6<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<VAR>a✝ : AEStronglyMeasurable f μ<GOAL>∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ < ⊤ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
<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>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : CompleteSpace 𝕜<VAR>E : Type u_6<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<VAR>a✝ : AEStronglyMeasurable f μ<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = 0 ∨ ↑‖c‖₊ = 0 ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
<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>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : CompleteSpace 𝕜<VAR>E : Type u_6<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<VAR>a✝ : AEStronglyMeasurable f μ<VAR>this : ∀ (x : ℝ≥0∞), x = 0 → x < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = 0 ∨ ↑‖c‖₊ = 0 ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>g : α → γ<VAR>g' : β → γ<GOAL>(range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃<VAR>β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄<VAR>γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅<VAR>δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆<VAR>c : C<GOAL>({ app := fun X_1 => G₂.map (({ app := fun X => α.app (R₂.obj X), naturality := ⋯ } ≫ { app := fun X => R₃.map (β.app X), naturality := ⋯ }).app X_1), naturality := ⋯ } ≫ { app := fun X_1 => ({ app := fun X_2 => γ.app (R₄.obj X_2), naturality := ⋯ } ≫ { app := fun X_2 => R₅.map (δ.app X_2), naturality := ⋯ }).app (K₁.obj X_1), naturality := ⋯ }).app c = ({ app := fun X_1 => ({ app := fun X_2 => G₂.map (α.app X_2), naturality := ⋯ } ≫ { app := fun X_2 => γ.app (H₁.obj X_2), naturality := ⋯ }).app (R₂.obj X_1), naturality := ⋯ } ≫ { app := fun X_1 => R₅.map (({ app := fun X => H₂.map (β.app X), naturality := ⋯ } ≫ { app := fun X => δ.app (K₁.obj X), naturality := ⋯ }).app X_1), naturality := ⋯ }).app c
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃<VAR>β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄<VAR>γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅<VAR>δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆<VAR>c : C<GOAL>G₂.map (α.app (R₂.obj c)) ≫ G₂.map (R₃.map (β.app c)) ≫ γ.app (R₄.obj (K₁.obj c)) ≫ R₅.map (δ.app (K₁.obj c)) = G₂.map (α.app (R₂.obj c)) ≫ γ.app (H₁.obj (R₂.obj c)) ≫ R₅.map (H₂.map (β.app c)) ≫ R₅.map (δ.app (K₁.obj c))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>X : Type u₇<VAR>Y : Type u₈<VAR>Z : Type u₉<VAR>inst✝⁸ : Category.{v₁, u₁} A<VAR>inst✝⁷ : Category.{v₂, u₂} B<VAR>inst✝⁶ : Category.{v₃, u₃} C<VAR>inst✝⁵ : Category.{v₄, u₄} D<VAR>inst✝⁴ : Category.{v₅, u₅} E<VAR>inst✝³ : Category.{v₆, u₆} F<VAR>inst✝² : Category.{v₇, u₇} X<VAR>inst✝¹ : Category.{v₈, u₈} Y<VAR>inst✝ : Category.{v₉, u₉} Z<VAR>G₁ : A ⥤ D<VAR>H₁ : B ⥤ E<VAR>K₁ : C ⥤ F<VAR>G₂ : D ⥤ X<VAR>H₂ : E ⥤ Y<VAR>K₂ : F ⥤ Z<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : B ⥤ C<VAR>R₂ : C ⥤ B<VAR>L₃ : D ⥤ E<VAR>R₃ : E ⥤ D<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>L₅ : X ⥤ Y<VAR>R₅ : Y ⥤ X<VAR>L₆ : Y ⥤ Z<VAR>R₆ : Z ⥤ Y<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>adj₅ : L₅ ⊣ R₅<VAR>adj₆ : L₆ ⊣ R₆<VAR>α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃<VAR>β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄<VAR>γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅<VAR>δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆<VAR>c : C<GOAL>G₂.map (α.app (R₂.obj c)) ≫ G₂.map (R₃.map (β.app c)) ≫ γ.app (R₄.obj (K₁.obj c)) ≫ R₅.map (δ.app (K₁.obj c)) = G₂.map (α.app (R₂.obj c)) ≫ ((R₃ ⋙ G₂).map (β.app c) ≫ γ.app (R₄.obj (K₁.obj c))) ≫ R₅.map (δ.app (K₁.obj c))
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(μ.toFun s)) K' ≤ (fun s => ↑(μ.toFun s)) K + ↑ε
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>hc : ¬∃ K', K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(μ.toFun s)) K' ≤ (fun s => ↑(μ.toFun s)) K + ↑ε<GOAL>False
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(μ.toFun K) + ↑ε < ↑(μ.toFun x)<GOAL>False
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(μ.toFun K) + ↑ε < ↑(μ.toFun x)<VAR>lower_bound_iInf : (fun s => ↑(μ.toFun s)) K + ↑ε ≤ ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), (fun s => ↑(μ.toFun s)) K'<GOAL>False
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>H : μ.ContentRegular<VAR>K : Compacts G<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>hc : ∀ (x : Compacts G), K.carrier ⊆ interior x.carrier → ↑(μ.toFun K) + ↑ε < ↑(μ.toFun x)<VAR>lower_bound_iInf : (fun s => ↑(μ.toFun s)) K + ↑ε ≤ (fun s => ↑(μ.toFun s)) K<GOAL>False
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>h : ∀ p ∈ e.source, ∃ s, IsOpen s ∧ p ∈ s ∧ ∃ φ u, ∃ (hu : IsOpen u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr s).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)<GOAL>∃ U, e.source = U ×ˢ univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>h : ∀ (x : ↑e.source), ∃ s, IsOpen s ∧ ↑x ∈ s ∧ ∃ φ u, ∃ (hu : IsOpen u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr s).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)<GOAL>∃ U, e.source = U ×ˢ univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>s : ↑e.source → Set (B × F)<VAR>hs : ∀ (x : ↑e.source), IsOpen (s x)<VAR>hsp : ∀ (x : ↑e.source), ↑x ∈ s x<VAR>φ : ↑e.source → B → F ≃L[𝕜] F<VAR>u : ↑e.source → Set B<VAR>hu : ∀ (x : ↑e.source), IsOpen (u x)<VAR>hφ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1)) (u x)<VAR>h2φ : ∀ (x : ↑e.source), SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x_1 => ↑(φ x x_1).symm) (u x)<VAR>heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.partialHomeomorph (φ x) ⋯ ⋯ ⋯)<GOAL>∃ U, e.source = U ×ˢ univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)