ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>hs : s.IsWF<VAR>hsn : s.Nonempty<VAR>ht : t.IsWF<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = Min.min (hs.min hsn) (ht.min htn)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>hs : s.IsWF<VAR>hsn : s.Nonempty<VAR>ht : t.IsWF<VAR>htn : t.Nonempty<GOAL>Min.min (hs.min hsn) (ht.min htn) ≤ ⋯.min ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>a : α<VAR>hs : s.IsWF<VAR>hsn : s.Nonempty<VAR>ht : t.IsWF<VAR>htn : t.Nonempty<GOAL>hs.min hsn ≤ ⋯.min ⋯ ∨ ht.min htn ≤ ⋯.min ⋯
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S x<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S x<GOAL>S ∈ 𝓝[>] x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S x<GOAL>∃ u ∈ Ioi x, Ioc x u ⊆ S
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁸ : Ring K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module K V'<VAR>inst✝¹ : AddCommGroup V''<VAR>inst✝ : Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>lift.{v', v''} (f ∘ₗ g).rank ≤ lift.{v'', v'} g.rank
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁸ : Ring K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module K V'<VAR>inst✝¹ : AddCommGroup V''<VAR>inst✝ : Module K V''<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V''<GOAL>lift.{v', v''} (Module.rank K ↥(Submodule.map f (range g))) ≤ lift.{v'', v'} (Module.rank K ↥(range g))
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>-clog b r⁻¹ = log b r
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>f : unit R ⟶ M<VAR>X✝ Y✝ : Cᵒᵖ<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(M.map f✝) ((fun X => (Hom.app f X) 1) X✝) = (fun X => (Hom.app f X) 1) Y✝
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s : M.sections<VAR>X Y : Cᵒᵖ<VAR>p : X ⟶ Y<VAR>x : ↑(R.obj X)<GOAL>1 (((unit R).map p) x) • ↑s Y = (M.map p) (1 x • ↑s X)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s : M.sections<VAR>X Y : Cᵒᵖ<VAR>p : X ⟶ Y<VAR>x : ↑(R.obj X)<GOAL>1 (((unit R).map p) x) • (M.presheaf ⋙ forget AddCommGrp).map p (↑s X) = (R.map p) (1 x) • (M.presheaf.map p) (↑s X)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>f : unit R ⟶ M<VAR>X : Cᵒᵖ<GOAL>Hom.app ((fun s => Hom.mk' (fun X => (ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)) ⋯) ((fun f => sectionsMk (fun X => (Hom.app f X) 1) ⋯) f)) X = Hom.app f X
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s : M.sections<VAR>X : Cᵒᵖ<GOAL>↑((fun f => sectionsMk (fun X => (Hom.app f X) 1) ⋯) ((fun s => Hom.mk' (fun X => (ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)) ⋯) s)) X = ↑s X
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>z : α × β<VAR>i : ℕ<GOAL>(l₁.zip l₂).get? i = some z ↔ l₁.get? i = some z.1 ∧ l₂.get? i = some z.2
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>t : ↑I<GOAL>(if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>((toPadicInt p).comp (fromPadicInt p)) x = (RingHom.id ℤ_[p]) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<VAR>f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s<GOAL>s ∈ ofComapInfPrincipal h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<VAR>f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s<VAR>this : f.NeBot<GOAL>s ∈ ofComapInfPrincipal h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<VAR>f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s<VAR>this✝ : f.NeBot<VAR>this : s ∈ f<GOAL>s ∈ ofComapInfPrincipal h
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(starRingEnd ℂ) (cos ↑x) = cos ↑x
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>s : Finset β<VAR>f : β → L.BoundedFormula α n<VAR>v : α → M<VAR>v' : Fin n → M<GOAL>(iSup s f).Realize v v' ↔ ∃ b ∈ s, (f b).Realize v v'
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s✝ t : Set α<VAR>a : α<VAR>s : UpperSet α<GOAL>Set.Ici 1 * ↑s ⊆ ↑s
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s✝ t : Set α<VAR>a : α<VAR>s : UpperSet α<GOAL>⋃ a ∈ Set.Ici 1, a • ↑s ⊆ ↑s
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimit G<VAR>inst✝ : HasColimit (curry.obj G ⋙ colim)<VAR>j : J<VAR>k : K<GOAL>colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom = colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimit G<VAR>inst✝ : HasColimit (curry.obj G ⋙ colim)<VAR>j : J<VAR>k : K<GOAL>(colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom) ≫ (colimitIsoColimitCurryCompColim G).inv = (colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j) ≫ (colimitIsoColimitCurryCompColim G).inv
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h₀ h₀' : x ≠ 0<GOAL>⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h₀ : x ≠ 0<VAR>h₀' : ¬↑‖x‖ = 0<GOAL>⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
<VAR>a b : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1
<VAR>a b : UnitAddCircle<VAR>this : ∀ (s : ℂ), completedHurwitzZetaEven a s - completedHurwitzZetaEven b s = completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s - ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s<GOAL>DifferentiableAt ℂ (fun s => completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1
<VAR>a b : UnitAddCircle<VAR>this : ∀ (s : ℂ), completedHurwitzZetaEven a s - completedHurwitzZetaEven b s = completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s - ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s<GOAL>DifferentiableAt ℂ (fun x => completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x - ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / x) 1
<VAR>a b : UnitAddCircle<VAR>this : ∀ (s : ℂ), completedHurwitzZetaEven a s - completedHurwitzZetaEven b s = completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s - ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s<GOAL>DifferentiableAt ℂ (fun x => completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<GOAL>Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : Infinite (α × β)<GOAL>Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : Infinite (α × β)<GOAL>Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)<GOAL>¬Infinite (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)<VAR>H' : Infinite (α × β)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)<VAR>H' : Infinite (α × β)<VAR>a : α<VAR>b : β<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)<VAR>H' : Infinite (α × β)<VAR>a : α<VAR>b : β<VAR>this : Fintype α<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)<VAR>H' : Infinite (α × β)<VAR>a : α<VAR>b : β<VAR>this✝ : Fintype α<VAR>this : Fintype β<GOAL>False
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>f : M →ₗ[R] M₂<VAR>g : M₃ →ₗ[R] M₄<VAR>x : M × M₂<GOAL>x ∈ f.graph ↔ x ∈ range (id.prod f)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n) = X n ^ p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>X n ^ p + C ((Int.castRingHom (ZMod p)) ↑p) * (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) = X n ^ p
<VAR>α : Type u_1<VAR>β : List α → Sort u_2<VAR>f : (a : α) → (l : List α) → β l → β (a :: l)<VAR>b : β []<VAR>l l' : List α<VAR>hl : l ~ l'<VAR>f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')<VAR>f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))<GOAL>HEq (List.rec b f l) (List.rec b f l')
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>x y : M<VAR>h : b.toDual x = b.toDual y<VAR>i : ι<GOAL>(b.repr x) i = (b.repr y) i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>x y : M<VAR>h : b.toDual x = b.toDual y<VAR>i : ι<GOAL>(b.toDual x) (b i) = (b.toDual y) (b i)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.27008, 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>A' 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>α : A' ⟶ A<GOAL>(α ≫ k) ≫ K.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>A' 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>α : A' ⟶ A<GOAL>α ≫ K.liftCycles k j hj hk = K.liftCycles (α ≫ k) j hj ⋯
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>h : ∀ (c : CharacterModule A), c a = 0<GOAL>a = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>a : A<VAR>h : a ≠ 0<GOAL>∃ c, c a ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<VAR>h : ¬↑(padicNormE q) = ↑(padicNormE r)<VAR>this : padicNormE q ≠ padicNormE r<GOAL>↑(padicNormE (q + r)) = max ↑(padicNormE q) ↑(padicNormE r)
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>2 * count b l ≤ l.length + 1
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>(if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1) ≤ l.length + 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x y : G<GOAL>(compLpL 2 μ (toSpanSingleton ℝ (x + y))) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) = (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) + (compLpL 2 μ (toSpanSingleton ℝ y)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))
<VAR>x y : ℂ<GOAL>cosh (x + y) = cosh x * cosh y + sinh x * sinh y
<VAR>x y : ℂ<GOAL>(cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) = 2 * (cexp x * cexp y + cexp (-x) * cexp (-y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<VAR>r : 𝕜<VAR>hx : x ≠ 0<VAR>hr : r ≠ 0<VAR>hx' : ‖x‖ ≠ 0<VAR>hr' : ‖r‖ ≠ 0<GOAL>‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<VAR>r : 𝕜<VAR>hx : x ≠ 0<VAR>hr : r ≠ 0<VAR>hx' : ‖x‖ ≠ 0<VAR>hr' : ‖r‖ ≠ 0<GOAL>‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁷ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>E : Type u_9<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module R E<VAR>F : Type u_10<VAR>inst✝² : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝ : (i : ι) → Module R (t i)<VAR>a : ι → M<VAR>b : ι₂ → M<GOAL>PiTensorProduct.tmul (((tprod R) fun i => a i) ⊗ₜ[R] (tprod R) fun i => b i) = (tprod R) fun i => Sum.elim a b i
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁷ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>E : Type u_9<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module R E<VAR>F : Type u_10<VAR>inst✝² : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝ : (i : ι) → Module R (t i)<VAR>a : ι → M<VAR>b : ι₂ → M<GOAL>((((currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R)) fun i => a i) fun i => b i) = (tprod R) fun i => Sum.elim a b i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝ : Unique α<VAR>f : α → E<VAR>x : α<GOAL>x = default
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝ : Unique α<VAR>f : α → E<GOAL>∫ (x : α), f default ∂μ = (μ univ).toReal • f default
<VAR>α : Type u_1<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : NormalSpace α<VAR>inst✝⁷ : R1Space α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>inst✝ : μ.WeaklyRegular<VAR>f : ↥(Lp E p μ)<GOAL>f ∈ closure ↑(boundedContinuousFunction E p μ)
<VAR>α : Type u_1<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : NormalSpace α<VAR>inst✝⁷ : R1Space α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>inst✝ : μ.WeaklyRegular<VAR>f : ↥(Lp E p μ)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<GOAL>∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ EMetric.closedBall f ε
<VAR>α : Type u_1<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : NormalSpace α<VAR>inst✝⁷ : R1Space α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>inst✝ : μ.WeaklyRegular<VAR>f : ↥(Lp E p μ)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>g : α →ᵇ E<VAR>hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε<VAR>g_mem : Memℒp (⇑g) p μ<GOAL>∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ EMetric.closedBall f ε
<VAR>α : Type u_1<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : NormalSpace α<VAR>inst✝⁷ : R1Space α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>inst✝ : μ.WeaklyRegular<VAR>f : ↥(Lp E p μ)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>g : α →ᵇ E<VAR>hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε<VAR>g_mem : Memℒp (⇑g) p μ<GOAL>Memℒp.toLp (⇑g) g_mem ∈ EMetric.closedBall f ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f✝ g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : ℕ → α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : ℕ → α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>g : α → β<VAR>left✝ : Measurable g<VAR>hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : ℕ → α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>g : α → β<VAR>left✝ : Measurable g<VAR>hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>Hg : AEStronglyMeasurable g μ<GOAL>∃ f_lim, StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : ℕ → α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>g : α → β<VAR>left✝ : Measurable g<VAR>hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>Hg : AEStronglyMeasurable g μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : ℕ → α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>g : α → β<VAR>left✝ : Measurable g<VAR>hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>Hg : AEStronglyMeasurable g μ<VAR>x : α<VAR>hx : Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>h'x : g x = AEStronglyMeasurable.mk g Hg x<GOAL>Tendsto (fun n => f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<GOAL>((biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) = 𝟙 M
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<GOAL>(∑ j : M.ι, (fun j_1 k => if h : j_1 = j then eqToHom ⋯ else 0) ≫ fun j_1 k => if h : j = k then eqToHom ⋯ else 0) = 𝟙 M
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>(∑ j : M.ι, (fun j_1 k => if h : j_1 = j then eqToHom ⋯ else 0) ≫ fun j_1 k => if h : j = k then eqToHom ⋯ else 0) i j = 𝟙 M i j