ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L₁<VAR>inst✝⁴ : LieRing L₂<VAR>inst✝³ : LieRing L₃<VAR>inst✝² : LieAlgebra R L₁<VAR>inst✝¹ : LieAlgebra R L₂<VAR>inst✝ : LieAlgebra R L₃<VAR>f_inv : L₂ → L₁<VAR>f : L₁ → L₂<VAR>map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x y : L₁}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, y⁆ = ⁅{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun y⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : L₂ → L₁<VAR>g : L₁ → L₂<VAR>map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : L₁), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x y : L₁}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, y⁆ = ⁅{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun y⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : f = g ∧ f_inv = g_inv<GOAL>{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } = { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv, left_inv := left_inv✝, right_inv := right_inv✝ }
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L₁<VAR>inst✝⁴ : LieRing L₂<VAR>inst✝³ : LieRing L₃<VAR>inst✝² : LieAlgebra R L₁<VAR>inst✝¹ : LieAlgebra R L₂<VAR>inst✝ : LieAlgebra R L₃<VAR>f_inv : L₂ → L₁<VAR>f : L₁ → L₂<VAR>map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x y : L₁}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, y⁆ = ⁅{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun y⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : L₂ → L₁<VAR>g : L₁ → L₂<VAR>map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : L₁), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x y : L₁}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, y⁆ = ⁅{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun y⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : f = g ∧ f_inv = g_inv<GOAL>f = g
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L₁<VAR>inst✝⁴ : LieRing L₂<VAR>inst✝³ : LieRing L₃<VAR>inst✝² : LieAlgebra R L₁<VAR>inst✝¹ : LieAlgebra R L₂<VAR>inst✝ : LieAlgebra R L₃<VAR>f_inv : L₂ → L₁<VAR>f : L₁ → L₂<VAR>map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x y : L₁}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, y⁆ = ⁅{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun y⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : L₂ → L₁<VAR>g : L₁ → L₂<VAR>map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : L₁), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x y : L₁}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, y⁆ = ⁅{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun y⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : f = g ∧ f_inv = g_inv<GOAL>f_inv = g_inv
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>(∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = √(∑ i : ι, ‖x i‖ ^ 2)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>(∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / 2)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁵ : Semiring R₁<VAR>inst✝¹⁴ : Semiring R₂<VAR>inst✝¹³ : Semiring R₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : AddCommGroup N₁<VAR>inst✝⁸ : AddCommGroup N₂<VAR>inst✝⁷ : AddCommGroup N₃<VAR>inst✝⁶ : Module R₁ M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>inst✝³ : Module R₁ N₁<VAR>inst✝² : Module R₂ N₂<VAR>inst✝¹ : Module R₃ N₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>c : M<GOAL>(g.comp 0) c = 0 c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : AEMeasurable f μ<GOAL>essSup (g ∘ f) μ ≤ essSup g (Measure.map f μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : AEMeasurable f μ<GOAL>map (g ∘ f) (ae μ) ≤ map g (ae (Measure.map f μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : AEMeasurable f μ<GOAL>map g (map f (ae μ)) ≤ map g (ae (Measure.map f μ))
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<GOAL>coeSubmodule S ⊤ = 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>I : Ideal R<VAR>hI₂ : I.IsPrime<VAR>hI : I ≠ ⊥<GOAL>∃ x ∈ I, Prime x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>n : ℤ<VAR>a : α<GOAL>IsSquare ((a * a) ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>(∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>(f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>x✝ : C<GOAL>e.functor.map (e.unit.app x✝) ≫ 𝟙 (e.functor.obj (e.inverse.obj (e.functor.obj x✝))) ≫ e.counit.app (e.functor.obj x✝) = 𝟙 (e.functor.obj x✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>x✝ : C<GOAL>e.functor.map (e.unit.app x✝) ≫ e.counit.app (e.functor.obj x✝) = 𝟙 (e.functor.obj x✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>x✝ : D<GOAL>e.unit.app (e.inverse.obj x✝) ≫ 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj x✝))) ≫ e.inverse.map (e.counit.app x✝) = 𝟙 (e.inverse.obj x✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>x✝ : D<GOAL>e.unit.app (e.inverse.obj x✝) ≫ e.inverse.map (e.counit.app x✝) = 𝟙 (e.inverse.obj x✝)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<GOAL>(changeForm h) 1 = 1
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖<GOAL>Integrable (⇑f) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>n : ℤ<GOAL>‖ContinuousMap.restrict (↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }) f‖ * (volume ↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }).toReal ≤ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖<GOAL>⋃ i, ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := ⋯ } = univ
<VAR>y : ℝ<VAR>h : y < 0<GOAL>0 ^ y = ⊤
<VAR>y : ℝ<VAR>h : y < 0<GOAL>some 0 ^ y = ⊤
<VAR>y : ℝ<VAR>h : y < 0<GOAL>(if 0 = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow 0 y)) = ⊤
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{u_3, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>G : V ⥤ W<VAR>inst✝ : G.Additive<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<GOAL>G.map (C.d i (c.next i) ≫ hom (c.next i) i + hom i (c.prev i) ≫ D.d (c.prev i) i) = G.map (C.d i (c.next i)) ≫ G.map (hom (c.next i) i) + G.map (hom i (c.prev i)) ≫ G.map (D.d (c.prev i) i)
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<GOAL>I.boundary M = (I.interior M)ᶜ
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<GOAL>I.interior M ⊓ I.boundary M = ⊥
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<GOAL>diracProba ∘ ⇑diracProbaEquiv.symm = fun μ => ↑μ
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<VAR>μ : ↑(range diracProba)<GOAL>(diracProba ∘ ⇑diracProbaEquiv.symm) μ = ↑μ
<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>inst✝ : SFinite μ<VAR>s t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set (β × β)<VAR>f : α → α → β<VAR>hf : UniformContinuous fun p => f p.1 p.2<VAR>hs : s ∈ 𝓤 β<GOAL>∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set (β × β)<VAR>f : α → α → β<VAR>hf : Tendsto ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)<VAR>hs : s ∈ 𝓤 β<GOAL>∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set (β × β)<VAR>f : α → α → β<VAR>hf : Tendsto ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)<VAR>hs : s ∈ 𝓤 β<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>v : Set (α × α)<VAR>hv : v ∈ 𝓤 α<VAR>huvt : u ×ˢ v ⊆ ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' s<GOAL>∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>s : Unit →₀ ℕ<VAR>n : ℕ<VAR>h : s () = n<GOAL>coeff R n = MvPowerSeries.coeff R s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
<VAR>F : Type w<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S✝<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>g : S✝ →ₙ+* T<VAR>f : R →ₙ+* S✝<VAR>S : Set (NonUnitalSubring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α × β → E<VAR>hf : AEStronglyMeasurable f (μ.prod ν)<GOAL>(fun x => ∫ (y : β), f (x, y) ∂ν) =ᶠ[ae μ] fun x => ∫ (y : β), AEStronglyMeasurable.mk f hf (x, y) ∂ν
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>h : Inducing (↑(a.pretrivializationAt b) ∘ TotalSpace.mk b)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<GOAL>Inducing (TotalSpace.mk b)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>h : Inducing ((a.pretrivializationAt b).source.restrict ↑(a.pretrivializationAt b) ∘ codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<GOAL>Inducing (TotalSpace.mk b)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>h : Inducing ((a.pretrivializationAt b).source.restrict ↑(a.pretrivializationAt b) ∘ codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<GOAL>Inducing (codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>h : Inducing ((a.pretrivializationAt b).source.restrict ↑(a.pretrivializationAt b) ∘ codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<GOAL>Continuous (codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>TensorBimod.actLeft (P.tensorBimod Q) L ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = R.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ ≫ TensorBimod.actLeft P (Q.tensorBimod L)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(tensorLeft R.X).map (coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X) ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)) ≫ TensorBimod.actLeft (P.tensorBimod Q) L ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = (tensorLeft R.X).map (coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X) ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)) ≫ R.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ ≫ TensorBimod.actLeft P (Q.tensorBimod L)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>R.X ◁ coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X) ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫ TensorBimod.actLeft (P.tensorBimod Q) L ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = R.X ◁ coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X) ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫ R.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ ≫ TensorBimod.actLeft P (Q.tensorBimod L)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>((α_ R.X (P.tensorBimod Q).X L.X).inv ≫ (P.tensorBimod Q).actLeft ▷ L.X ≫ coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X) ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = R.X ◁ coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X) ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫ R.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ ≫ TensorBimod.actLeft P (Q.tensorBimod L)