ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i<VAR>m : (i : ι) → E i<GOAL>‖(g.compContinuousLinearMap fun i => (f i).toContinuousLinearMap) m‖ ≤ ‖g‖ * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i<VAR>m : (i : ι) → E i<GOAL>‖g‖ * ∏ i : ι, ‖((fun i => ↑((fun i => (f i).toContinuousLinearMap) i)) i) (m i)‖ ≤ ‖g‖ * ∏ i : ι, ‖m i‖
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<GOAL>Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<VAR>h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1<VAR>f g : R[X]<VAR>hfg : p = f * g<GOAL>(g * C f.leadingCoeff).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<VAR>h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1<VAR>f g : R[X]<VAR>hfg : p = f * g<GOAL>(f * C g.leadingCoeff).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<VAR>h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1<VAR>f g : R[X]<VAR>hfg : p = f * g<GOAL>g * C f.leadingCoeff * (f * C g.leadingCoeff) = p
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hxy : x + y ∈ s<VAR>hy : y ≠ 0<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>x + t • y ∈ interior s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hxy : x + y ∈ s<VAR>hy : y ≠ 0<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<VAR>h : x + t • y = (1 - t) • x + t • (x + y)<GOAL>x + t • y ∈ interior s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>hs : StrictConvex 𝕜 s<VAR>hx : x ∈ s<VAR>hxy : x + y ∈ s<VAR>hy : y ≠ 0<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<VAR>h : x + t • y = (1 - t) • x + t • (x + y)<GOAL>(1 - t) • x + t • (x + y) ∈ interior s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : MeasurableMul₂ G<VAR>inst✝ : MeasurableInv G<VAR>μ : Measure α<VAR>f g : α → G<VAR>hf : AEMeasurable f μ<VAR>h : AEMeasurable (f * g) μ<GOAL>g = f * g * f⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>c : Chain α<VAR>f : α → β<VAR>hf : ScottContinuous f<GOAL>IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (ωSup c))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>c : Chain α<VAR>f : α → β<VAR>hf : ScottContinuous f<GOAL>IsLUB (Set.range (f ∘ ⇑c)) (f (ωSup c))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>c : Chain α<VAR>f : α → β<VAR>hf : ScottContinuous f<GOAL>IsLUB (f '' Set.range ⇑c) (f (ωSup c))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g)ᘁ = gᘁ ≫ fᘁ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g)ᘁ = (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ ≫ Zᘁ ◁ (g ⊗ fᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ ε_ Z Zᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ ε_ Z Zᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom = (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ ≫ Zᘁ ◁ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ (α_ Zᘁ Z Xᘁ).inv ≫ ε_ Z Zᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(((((ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ) ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ)) ≫ (α_ Zᘁ Z Xᘁ).inv) ≫ ε_ Z Zᘁ ▷ Xᘁ) ≫ (λ_ Xᘁ).hom = (((((ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ) ≫ Zᘁ ◁ (g ⊗ (((((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ) ≫ Yᘁ ◁ f ▷ Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv) ≫ ε_ Y Yᘁ ▷ Xᘁ) ≫ (λ_ Xᘁ).hom)) ≫ (α_ Zᘁ Z Xᘁ).inv) ≫ ε_ Z Zᘁ ▷ Xᘁ) ≫ (λ_ Xᘁ).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>((ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ) ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) = ((ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ) ≫ Zᘁ ◁ (g ⊗ (((((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ) ≫ Yᘁ ◁ f ▷ Xᘁ) ≫ (α_ Yᘁ Y Xᘁ).inv) ≫ ε_ Y Yᘁ ▷ Xᘁ) ≫ (λ_ Xᘁ).hom)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) = (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ Y Yᘁ ≫ Zᘁ ◁ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(ρ_ Zᘁ).inv ≫ Zᘁ ◁ (η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ) = (ρ_ Zᘁ).inv ≫ Zᘁ ◁ (η_ Y Yᘁ ≫ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasRightDual X<VAR>inst✝¹ : HasRightDual Y<VAR>inst✝ : HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>η_ Y Yᘁ ≫ (g ⊗ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ
<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>inst✝ : IsMarkovKernel κ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
<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>inst✝ : IsMarkovKernel κ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)) ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblZ P = 0
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>v : Vector ℕ n.succ<GOAL>f (ofFn fun i => v.get i.succ) = f v.tail
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>v : Vector ℕ n.succ<GOAL>f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>v : Vector ℕ n.succ<GOAL>(fun i => v.get i.succ) = v.tail.get
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>v : Vector ℕ n.succ<VAR>i : Fin n<GOAL>v.get i.succ = v.tail.get i
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<GOAL>T.η.app c.pt ≫ lambda c t = 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<GOAL>∀ (j : J), c.ι.app j ≫ T.η.app c.pt ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>c.ι.app j ≫ T.η.app c.pt ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>c.ι.app j = c.ι.app j ≫ 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<GOAL>T.μ.app c.pt ≫ lambda c t = T.map (lambda c t) ≫ lambda c t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>(T.mapCocone (T.mapCocone c)).ι.app j ≫ T.μ.app c.pt ≫ lambda c t = (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.map (lambda c t) ≫ lambda c t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ (D.obj j).a ≫ c.ι.app j
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : Nontrivial ι<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : Nontrivial ι<VAR>h0 : 1 < ↑#ι<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : Nontrivial ι<VAR>h0 : 1 < ↑#ι<VAR>h1 : 0 < ↑#ι - 1<VAR>h2 : 0 ≤ 1 / (↑#ι - 1)<VAR>h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : Nontrivial ι<VAR>h0 : 1 < ↑#ι<VAR>h1 : 0 < ↑#ι - 1<VAR>h2 : 0 ≤ 1 / (↑#ι - 1)<VAR>h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1<VAR>h4 : p = 1 + 1 / (↑#ι - 1)<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : Nontrivial ι<VAR>h0 : 1 < ↑#ι<VAR>h1 : 0 < ↑#ι - 1<VAR>h2 : 0 ≤ 1 / (↑#ι - 1)<VAR>h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1<VAR>h4 : p = 1 + 1 / (↑#ι - 1)<GOAL>∫⁻ (x : (i : ι) → A i), ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + 1 / (↑#ι - 1))
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp : (↑#ι).IsConjExponent p<VAR>f : ((a : ι) → A a) → ℝ≥0∞<VAR>hf : Measurable f<VAR>this : Nontrivial ι<VAR>h0 : 1 < ↑#ι<VAR>h1 : 0 < ↑#ι - 1<VAR>h2 : 0 ≤ 1 / (↑#ι - 1)<VAR>h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1<VAR>h4 : p = 1 + 1 / (↑#ι - 1)<GOAL>(fun x => ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1))) = fun x => f x ^ (1 - (↑#ι - 1) * (1 / (↑#ι - 1))) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1))
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => c ≤ x<VAR>hac : a ≤ c<GOAL>filter (fun x => c ≤ x) (Ico a b) = Ico c b
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => c ≤ x<VAR>hac : a ≤ c<GOAL>(Finset.Ico c b).val = Ico c b
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<GOAL>fibRec.IsSolution fun x => ψ ^ x
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<GOAL>(X ^ 2 - (X + 1)).IsRoot ψ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>b : Set (Set α)<VAR>bct : b.Countable<VAR>hbm : ∀ s ∈ b, MeasurableSet s<VAR>hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y<GOAL>∃ m', CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>b : Set (Set α)<VAR>bct : b.Countable<VAR>hbm : ∀ s ∈ b, MeasurableSet s<VAR>hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y<GOAL>CountablyGenerated α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>b : Set (Set α)<VAR>bct : b.Countable<VAR>hbm : ∀ s ∈ b, MeasurableSet s<VAR>hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y<GOAL>SeparatesPoints α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>b : Set (Set α)<VAR>bct : b.Countable<VAR>hbm : ∀ s ∈ b, MeasurableSet s<VAR>hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y<GOAL>∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<GOAL>(NatTrans.leftDerivedToHomotopyCategory α).app X = (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<GOAL>(NatTrans.leftDerivedToHomotopyCategory α).app X ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom = (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<GOAL>(HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) = ((F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex))) ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<GOAL>(HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) = (F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<GOAL>(HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom = (F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>β : (projectiveResolution X).complex ⟶ P.complex<VAR>hβ : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β = P.iso.hom<GOAL>(HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom = (F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)