ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.19876, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>c : KernelFork S.g<VAR>hc : IsLimit c<GOAL>S.f ≫ 𝟙 S.X₂ = 0
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u v : U<VAR>x✝¹ : Γ'<VAR>x✝ : Γ<GOAL>((A.compHahnSeries B (u + v)).coeff x✝¹).coeff x✝ = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x✝¹).coeff x✝
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u v : U<VAR>x✝¹ : Γ'<VAR>x✝ : Γ<GOAL>(A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝ = (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ + (A (((of R).symm (B v)).coeff x✝¹)).coeff x✝
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>x y x✝ : α<GOAL>x✝ * y = x ↔ x = y * x✝
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>j : J<GOAL>((Pi.map fun j => (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j => (T j).obj₁)) ≫ (shiftFunctor C 1).map (Pi.π (fun j => (T j).obj₁) j) = Pi.π (fun j => (T j).obj₃) j ≫ (T j).mor₃
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>j : J<GOAL>(Pi.map fun j => (T j).mor₃) ≫ Pi.π (fun b => (shiftFunctor C 1).obj (T b).obj₁) j = Pi.π (fun j => (T j).obj₃) j ≫ (T j).mor₃
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(ofFn f).length = n
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>b ∈ sphere a r ↔ ‖b / a‖ = r
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(l.node' x r).dual = r.dual.node' x l.dual
<VAR>s : ℂ<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume<GOAL>False
<VAR>s : ℂ<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume<VAR>hs : s.re ≤ -1<GOAL>False
<VAR>s : ℂ<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume<VAR>hs : -1 < s.re<GOAL>False
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>(∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t y) ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝⁴ : HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>inst✝³ : HasPullback i i<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback (f ≫ i) (g ≫ i)<VAR>inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(pullbackDiagonalMapIdIso f g i).inv ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) = snd f g
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝⁴ : HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>inst✝³ : HasPullback i i<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback (f ≫ i) (g ≫ i)<VAR>inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i) = (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Iic b = Iic (b - a)
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d✝ : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>d : 𝔸<GOAL>HasStrictDerivAt (fun y => c y * d) (c' * d) x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d✝ : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>d : 𝔸<GOAL>c' * d = c' * d + c x * 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>Eu : Type u<VAR>inst✝⁵ : NormedAddCommGroup Eu<VAR>inst✝⁴ : NormedSpace 𝕜 Eu<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>s : Set Eu<VAR>t : Set Fu<VAR>g : Fu → Gu<VAR>f : Eu → Fu<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>Eu : Type u<VAR>inst✝⁵ : NormedAddCommGroup Eu<VAR>inst✝⁴ : NormedSpace 𝕜 Eu<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>s : Set Eu<VAR>t : Set Fu<VAR>g : Fu → Gu<VAR>f : Eu → Fu<VAR>hg : ContDiffOn 𝕜 0 g t<VAR>hf : ContDiffOn 𝕜 0 f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffOn 𝕜 0 (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>IH : ∀ {Eu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] {Fu : Type u} [inst_2 : NormedAddCommGroup Fu] [inst_3 : NormedSpace 𝕜 Fu] {Gu : Type u} [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] {s : Set Eu} {t : Set Fu} {g : Fu → Gu} {f : Eu → Fu}, ContDiffOn 𝕜 (↑n) g t → ContDiffOn 𝕜 (↑n) f s → s ⊆ f ⁻¹' t → ContDiffOn 𝕜 (↑n) (g ∘ f) s<VAR>Eu : Type u<VAR>inst✝⁵ : NormedAddCommGroup Eu<VAR>inst✝⁴ : NormedSpace 𝕜 Eu<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>s : Set Eu<VAR>t : Set Fu<VAR>g : Fu → Gu<VAR>f : Eu → Fu<VAR>hg : ContDiffOn 𝕜 (↑n.succ) g t<VAR>hf : ContDiffOn 𝕜 (↑n.succ) f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffOn 𝕜 (↑n.succ) (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>Itop : ∀ (n : ℕ) {Eu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] {Fu : Type u} [inst_2 : NormedAddCommGroup Fu] [inst_3 : NormedSpace 𝕜 Fu] {Gu : Type u} [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] {s : Set Eu} {t : Set Fu} {g : Fu → Gu} {f : Eu → Fu}, ContDiffOn 𝕜 (↑n) g t → ContDiffOn 𝕜 (↑n) f s → s ⊆ f ⁻¹' t → ContDiffOn 𝕜 (↑n) (g ∘ f) s<VAR>Eu : Type u<VAR>inst✝⁵ : NormedAddCommGroup Eu<VAR>inst✝⁴ : NormedSpace 𝕜 Eu<VAR>Fu : Type u<VAR>inst✝³ : NormedAddCommGroup Fu<VAR>inst✝² : NormedSpace 𝕜 Fu<VAR>Gu : Type u<VAR>inst✝¹ : NormedAddCommGroup Gu<VAR>inst✝ : NormedSpace 𝕜 Gu<VAR>s : Set Eu<VAR>t : Set Fu<VAR>g : Fu → Gu<VAR>f : Eu → Fu<VAR>hg : ContDiffOn 𝕜 ⊤ g t<VAR>hf : ContDiffOn 𝕜 ⊤ f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffOn 𝕜 ⊤ (g ∘ f) s
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : μ s ≠ 0<VAR>p : α → Prop<VAR>hp : ∀ᵐ (x : α) ∂μ.restrict s, p x<GOAL>∃ x ∈ s, p x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s<VAR>p : α → Prop<VAR>hp : ∀ᵐ (x : α) ∂μ.restrict s, p x<GOAL>∃ x ∈ s, p x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y : ↑Y<VAR>s1 s2 : S<GOAL>(fun s => g (s • y)) (s1 + s2) = (fun s => g (s • y)) s1 + (fun s => g (s • y)) s2
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y : ↑Y<VAR>s1 s2 : S<GOAL>g (s1 • y + s2 • y) = g (s1 • y) + g (s2 • y)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y : ↑Y<VAR>r : R<VAR>s : S<GOAL>g ((r • s) • y) = r • g (s • y)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y : ↑Y<VAR>r : R<VAR>s : S<GOAL>g ((r • s) • y) = g (r • s • y)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y : ↑Y<VAR>r : R<VAR>s : S<GOAL>g (↑f.toMonoidWithZeroHom r • s • y) = g (r • s • y)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y1 y2 : ↑Y<VAR>s : S<GOAL>((fun y => { toFun := fun s => g (s • y), map_add' := ⋯, map_smul' := ⋯ }) (y1 + y2)) s = ((fun y => { toFun := fun s => g (s • y), map_add' := ⋯, map_smul' := ⋯ }) y1 + (fun y => { toFun := fun s => g (s • y), map_add' := ⋯, map_smul' := ⋯ }) y2) s
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y1 y2 : ↑Y<VAR>s : S<GOAL>g (s • (y1 + y2)) = ({ toFun := fun s => g (s • y1), map_add' := ⋯, map_smul' := ⋯ } + { toFun := fun s => g (s • y2), map_add' := ⋯, map_smul' := ⋯ }) s
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y1 y2 : ↑Y<VAR>s : S<GOAL>g (s • (y1 + y2)) = { toFun := fun s => g (s • y1), map_add' := ⋯ } s + { toFun := fun s => g (s • y2), map_add' := ⋯ } s
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>y1 y2 : ↑Y<VAR>s : S<GOAL>g (s • (y1 + y2)) = g (s • y1) + g (s • y2)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>s : S<VAR>y : ↑Y<VAR>t : S<GOAL>({ toFun := fun y => { toFun := fun s => g (s • y), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (s • y)) t = ((RingHom.id S) s • { toFun := fun y => { toFun := fun s => g (s • y), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun y) t
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>s : S<VAR>y : ↑Y<VAR>t : S<GOAL>g (t • s • y) = (s • { toFun := fun s => g (s • y), map_add' := ⋯, map_smul' := ⋯ }) t
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>s : S<VAR>y : ↑Y<VAR>t : S<GOAL>g (t • s • y) = { toFun := fun s => g (s • y), map_add' := ⋯ } (t * s)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (restrictScalars f).obj Y ⟶ X<VAR>s : S<VAR>y : ↑Y<VAR>t : S<GOAL>g (t • s • y) = g ((t * s) • y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f' f g : α →ₘ[μ] β<VAR>hf : f' ≤ f<VAR>hg : f' ≤ g<GOAL>f' ≤ f ⊓ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f' f g : α →ₘ[μ] β<VAR>hf : ↑f' ≤ᶠ[ae μ] ↑f<VAR>hg : ↑f' ≤ᶠ[ae μ] ↑g<GOAL>↑f' ≤ᶠ[ae μ] ↑(f ⊓ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f' f g : α →ₘ[μ] β<VAR>hf : ↑f' ≤ᶠ[ae μ] ↑f<VAR>hg : ↑f' ≤ᶠ[ae μ] ↑g<VAR>a✝ : α<VAR>haf : ↑f' a✝ ≤ ↑f a✝<VAR>hag : ↑f' a✝ ≤ ↑g a✝<VAR>ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝<GOAL>↑f' a✝ ≤ ↑(f ⊓ g) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>f' f g : α →ₘ[μ] β<VAR>hf : ↑f' ≤ᶠ[ae μ] ↑f<VAR>hg : ↑f' ≤ᶠ[ae μ] ↑g<VAR>a✝ : α<VAR>haf : ↑f' a✝ ≤ ↑f a✝<VAR>hag : ↑f' a✝ ≤ ↑g a✝<VAR>ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝<GOAL>↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, image2 f s (t i j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
<VAR>θ : Angle<GOAL>θ - ↑π = θ + ↑π
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>pos : ℝ → ℝ := fun x => max x 0<VAR>neg : ℝ → ℝ := fun x => max (-x) 0<VAR>posm : Measurable pos<VAR>negm : Measurable neg<VAR>Xp : Ω → ℝ := pos ∘ X<VAR>Xm : Ω → ℝ := neg ∘ X<VAR>Yp : Ω → ℝ := pos ∘ Y<VAR>Ym : Ω → ℝ := neg ∘ Y<VAR>hXpm : X = Xp - Xm<VAR>hYpm : Y = Yp - Ym<VAR>hp1 : 0 ≤ Xm<VAR>hp2 : 0 ≤ Xp<VAR>hp3 : 0 ≤ Ym<GOAL>integral μ (X * Y) = integral μ X * integral μ Y