ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<VAR>c : Cardinal.{u}<VAR>e : Cardinal.lift.{v, u} c = b.card<VAR>α : Type u<VAR>β : Type (max u v)<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<VAR>f : α ≃ β<VAR>g : ⇑f ⁻¹'o s ≃r s<VAR>this : IsWellOrder α (⇑f ⁻¹'o s)<GOAL>∃ a', lift.{v, u} a' = type s
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<VAR>c : Cardinal.{u}<VAR>e : Cardinal.lift.{v, u} c = b.card<VAR>α : Type u<VAR>β : Type (max u v)<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<VAR>f : α ≃ β<VAR>g : ⇑f ⁻¹'o s ≃r s<VAR>this✝ : IsWellOrder α (⇑f ⁻¹'o s)<VAR>this : lift.{max u v, u} (type (⇑f ⁻¹'o s)) = lift.{max u v, max u v} (type s)<GOAL>∃ a', lift.{v, u} a' = type s
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<VAR>c : Cardinal.{u}<VAR>e : Cardinal.lift.{v, u} c = b.card<VAR>α : Type u<VAR>β : Type (max u v)<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<VAR>f : α ≃ β<VAR>g : ⇑f ⁻¹'o s ≃r s<VAR>this✝ : IsWellOrder α (⇑f ⁻¹'o s)<VAR>this : lift.{v, u} (type (⇑f ⁻¹'o s)) = type s<GOAL>∃ a', lift.{v, u} a' = type s
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_2<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : IsLocalization S A<VAR>M : Type u_3<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : IsScalarTower R A M<VAR>M' : Type u_4<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module A M'<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>Q : Type (max u_3 u_4 u_2)<VAR>x✝³ : AddCommMonoid Q<VAR>x✝² : Module R Q<VAR>x✝¹ : Module A Q<VAR>x✝ : IsScalarTower R A Q<VAR>g : M →ₗ[R] Q<GOAL>∃! g', ↑R g' ∘ₗ f = g
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_2<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : IsLocalization S A<VAR>M : Type u_3<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : IsScalarTower R A M<VAR>M' : Type u_4<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module A M'<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>Q : Type (max u_3 u_4 u_2)<VAR>x✝³ : AddCommMonoid Q<VAR>x✝² : Module R Q<VAR>x✝¹ : Module A Q<VAR>x✝ : IsScalarTower R A Q<VAR>ℓ : M' →ₗ[R] Q<VAR>h₂ : ∀ (y : M' →ₗ[R] Q), (fun l => l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ<GOAL>∃! g', ↑R g' ∘ₗ f = ℓ ∘ₗ f
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.102334, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ✝ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>hk : k ≫ K.d i j = 0<VAR>φ : K ⟶ L<GOAL>(k ≫ φ.f i) ≫ L.d i j = 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ✝ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>hk : k ≫ K.d i j = 0<VAR>φ : K ⟶ L<GOAL>K.liftCycles k j hj hk ≫ cyclesMap φ i = L.liftCycles (k ≫ φ.f i) j hj ⋯
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f✝ g✝ : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → A<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : ContinuousOn g [[a, b]]<GOAL>IntervalIntegrable (fun x => g x * f x) μ a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f✝ g✝ : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → A<VAR>hf : IntegrableOn f (Ι a b) μ<VAR>hg : ContinuousOn g [[a, b]]<GOAL>IntegrableOn (fun x => g x * f x) (Ι a b) μ
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x : α<VAR>n : ℕ<VAR>ih : normalizedFactors (x ^ n) = n • normalizedFactors x<VAR>h0 : ¬x = 0<GOAL>normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<GOAL>UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ swap F) ↔ ∀ (k : κ), UniformContinuous (⇑UniformFun.ofFun ∘ swap F)
<VAR>θ : Angle<GOAL>|θ.toReal| = π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : (↥A)ˣ<GOAL>A.valuation ↑↑a = 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : (↥A)ˣ<GOAL>∃ a_1, ↑↑a_1 * 1 = ↑↑a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>a : (↥A)ˣ<GOAL>↑↑a * 1 = ↑↑a
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<GOAL>sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g κ μ<VAR>hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'<VAR>hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g κ μ<VAR>hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'<VAR>hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<VAR>a : α<VAR>hf' : f =ᶠ[ae (κ a)] f'<VAR>hg' : g =ᶠ[ae (κ a)] g'<VAR>hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)<GOAL>(κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g κ μ<VAR>hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'<VAR>hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<VAR>a : α<VAR>hf' : f =ᶠ[ae (κ a)] f'<VAR>hg' : g =ᶠ[ae (κ a)] g'<VAR>hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)<VAR>h1 : f ⁻¹' A =ᶠ[ae (κ a)] f' ⁻¹' A<GOAL>(κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g κ μ<VAR>hf : ∀ᵐ (a : α) ∂μ, f =ᶠ[ae (κ a)] f'<VAR>hg : ∀ᵐ (a : α) ∂μ, g =ᶠ[ae (κ a)] g'<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<VAR>a : α<VAR>hf' : f =ᶠ[ae (κ a)] f'<VAR>hg' : g =ᶠ[ae (κ a)] g'<VAR>hfg' : (κ a) (f ⁻¹' A ∩ g ⁻¹' B) = (κ a) (f ⁻¹' A) * (κ a) (g ⁻¹' B)<VAR>h1 : f ⁻¹' A =ᶠ[ae (κ a)] f' ⁻¹' A<VAR>h2 : g ⁻¹' B =ᶠ[ae (κ a)] g' ⁻¹' B<GOAL>(κ a) (f' ⁻¹' A ∩ g' ⁻¹' B) = (κ a) (f' ⁻¹' A) * (κ a) (g' ⁻¹' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Finite<VAR>hfin : ∀ i ∈ s, μ (f i) ≠ ⊤<GOAL>μ (⋃ i ∈ s, f i) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Finite<VAR>hfin : ∀ i ∈ s, μ (f i) ≠ ⊤<GOAL>(fun i => ⋃ (_ : i ∈ s), f i) = fun i => ⋃ (_ : i ∈ hs.toFinset), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Set β<VAR>f : β → Set α<VAR>hs : s.Finite<VAR>hfin : ∀ i ∈ s, μ (f i) ≠ ⊤<GOAL>∑ i ∈ hs.toFinset, μ (f 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>f✝ f : G →* N<VAR>H : Subgroup N<VAR>h : H ≤ f.range<GOAL>map f (comap f H) = H
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>a : Rˣ<GOAL>1 ↑a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Group α<VAR>a : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : a < 1<GOAL>1 < a⁻ᵐ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<GOAL>integral f = ‖posPart f‖ - ‖negPart f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>ae_eq₁ : ↑(toSimpleFunc f).posPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))<GOAL>integral f = ‖posPart f‖ - ‖negPart f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>ae_eq₁ : ↑(toSimpleFunc f).posPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))<VAR>ae_eq₂ : ↑(toSimpleFunc f).negPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))<GOAL>integral f = ‖posPart f‖ - ‖negPart f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>ae_eq₁ : ↑(toSimpleFunc f).posPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))<VAR>ae_eq₂ : ↑(toSimpleFunc f).negPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))<GOAL>MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) = MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>ae_eq₁ : ↑(toSimpleFunc f).posPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))<VAR>ae_eq₂ : ↑(toSimpleFunc f).negPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))<GOAL>Integrable (↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>ae_eq₁ : ↑(toSimpleFunc f).posPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (posPart f)))<VAR>ae_eq₂ : ↑(toSimpleFunc f).negPart =ᶠ[ae μ] ↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))<GOAL>Integrable (↑(SimpleFunc.map norm (toSimpleFunc (negPart f)))) μ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ Sum.inl)<VAR>c₂ : Cofan (X ∘ Sum.inr)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>hc₂ : IsColimit c₂<VAR>inst✝ : MonoCoprod C<VAR>inr : c₂.pt ⟶ c.pt<VAR>hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)<GOAL>Mono inr
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ Sum.inl)<VAR>c₂ : Cofan (X ∘ Sum.inr)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>hc₂ : IsColimit c₂<VAR>inst✝ : MonoCoprod C<VAR>inr : c₂.pt ⟶ c.pt<VAR>hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)<GOAL>inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : β → α → β<VAR>b : β<VAR>a : α<VAR>l : List α<VAR>h : 0 < (scanl f b l).length<GOAL>(scanl f b l).get ⟨0, h⟩ = b
<VAR>n m : ℕ<VAR>a : Fin (n + 1)<GOAL>a < last n ↔ a ≠ last n
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<GOAL>(mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom ≫ mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom = mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (𝟙 X₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<GOAL>mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).inv (𝟙 X₃) ≫ (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom ≫ mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom = mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).inv (𝟙 X₃) ≫ mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (𝟙 X₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D : Type u_4<VAR>I₁ : Type u_5<VAR>I₂ : Type u_6<VAR>I₃ : Type u_7<VAR>J : Type u_8<VAR>inst✝¹⁵ : Category.{u_10, u_1} C₁<VAR>inst✝¹⁴ : Category.{u_12, u_2} C₂<VAR>inst✝¹³ : Category.{u_11, u_3} C₃<VAR>inst✝¹² : Category.{u_9, u_4} D<VAR>inst✝¹¹ : Zero I₂<VAR>inst✝¹⁰ : DecidableEq I₂<VAR>inst✝⁹ : HasInitial C₂<VAR>F₁ : C₁ ⥤ C₂ ⥤ C₁<VAR>F₂ : C₂ ⥤ C₃ ⥤ C₃<VAR>G : C₁ ⥤ C₃ ⥤ D<VAR>associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂<VAR>X₂ : C₂<VAR>e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁<VAR>e₂ : F₂.obj X₂ ≅ 𝟭 C₃<VAR>inst✝⁸ : (X₁ : C₁) → PreservesColimit (Functor.empty C₂) (F₁.obj X₁)<VAR>inst✝⁷ : (X₃ : C₃) → PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)<VAR>r : I₁ × I₂ × I₃ → J<VAR>π : I₁ × I₃ → J<VAR>τ : TriangleIndexData r π<VAR>X₁ : GradedObject I₁ C₁<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂<VAR>inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π<VAR>inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃<VAR>inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π<VAR>inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃<VAR>inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π<VAR>triangle : ∀ (X₁ : C₁) (X₃ : C₃), ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃<VAR>j : J<VAR>i₁ : I₁<VAR>i₃ : I₃<VAR>hj : π (i₁, i₃) = j<GOAL>ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj ≫ (mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).inv (𝟙 X₃) ≫ (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom ≫ mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom) j = ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj ≫ (mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).inv (𝟙 X₃) ≫ mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom (𝟙 X₃)) j