ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<VAR>v : n → 𝕜<VAR>t : ℝ<VAR>ht : t ≠ 0<VAR>hv : v ≠ 0<VAR>hv' : (A - B) *ᵥ v = t • v<VAR>h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0<VAR>h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0<VAR>aux : star v ⬝ᵥ (A - B) *ᵥ v = 0<GOAL>False
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<VAR>h_ne : ¬A = B<VAR>v : n → 𝕜<VAR>t : ℝ<VAR>ht : t ≠ 0<VAR>hv : v ≠ 0<VAR>hv' : (A - B) *ᵥ v = t • v<VAR>h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0<VAR>h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0<VAR>aux : ↑t * star v ⬝ᵥ v = ↑t * 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>↑(re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>s✝ : Set M<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>f : M → N<VAR>hf : IsMonoidHom f<VAR>s : Set N<VAR>hs : IsSubmonoid s<GOAL>f 1 ∈ s
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>s✝ : Set M<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>f : M → N<VAR>hf : IsMonoidHom f<VAR>s : Set N<VAR>hs : IsSubmonoid s<VAR>a b : M<VAR>ha : f a ∈ s<VAR>hb : f b ∈ s<GOAL>f (a * b) ∈ s
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_8, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : τ₀ = τ₁ hF hG η<VAR>Y : B<GOAL>eB.inverse.map (F.map (𝟙 (G.obj Y) ≫ eA.unitIso.hom.app (G.obj Y) ≫ eA.inverse.map (hG.inv.app Y) ≫ 𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))))) ≫ (equivalence₂ eB hF).counitIso.hom.app Y = (equivalenceCounitIso η).hom.app Y
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_8, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : τ₀ = τ₁ hF hG η<VAR>Y : B<GOAL>eB.inverse.map (F.map (eA.unitIso.hom.app (G.obj Y))) ≫ eB.inverse.map (F.map (eA.inverse.map (hG.inv.app Y))) ≫ eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y)))) ≫ eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)))) ≫ eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj Y)) ≫ eB.unitIso.inv.app Y = eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_8, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : τ₀ = τ₁ hF hG η<VAR>Y : B<GOAL>eB.inverse.map (F.map (eA.unitIso.hom.app (G.obj Y)) ≫ F.map (eA.inverse.map (hG.inv.app Y)) ≫ hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))) ≫ e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫ e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫ eB.unitIso.inv.app Y = eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_8, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : τ₀ = τ₁ hF hG η<VAR>Y : B<GOAL>hF.inv.app (G.obj Y) ≫ e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫ e'.functor.map (eA.functor.map (eA.inverse.map (hG.inv.app Y))) ≫ e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫ e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y = η.hom.app Y
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_8, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : τ₀ = τ₁ hF hG η<VAR>Y : B<GOAL>hF.inv.app (G.obj Y) ≫ e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y)) ≫ eA.counit.app (eA.functor.obj (G.obj Y)) ≫ 𝟙 ((G ⋙ eA.functor).obj Y)) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y = η.hom.app Y
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_8, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_5, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>η : G ⋙ F ≅ eB.functor<VAR>hη : τ₀ = τ₁ hF hG η<VAR>Y : B<GOAL>hF.inv.app (G.obj Y) ≫ e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y)) ≫ eA.counit.app (eA.functor.obj (G.obj Y)) ≫ 𝟙 (eA.functor.obj (G.obj Y))) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y = η.hom.app Y
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>f : (n → R) →ₗ[R] m → R<VAR>i : m<VAR>j : n<GOAL>toMatrix' f i j = f (fun j' => if j' = j then 1 else 0) i
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>f : (n → R) →ₗ[R] m → R<VAR>i : m<VAR>j : n<GOAL>f ((stdBasis R (fun x => R) j) 1) i = f (fun j' => if j' = j then 1 else 0) i
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>f : (n → R) →ₗ[R] m → R<VAR>i : m<VAR>j j' : n<VAR>h : ¬j' = j<GOAL>(stdBasis R (fun x => R) j) 1 j' = 0
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g : G<VAR>hg : orderOf g = 2<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g : G<VAR>hg : orderOf g = 2<VAR>key : φ g = g<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : Function.Involutive ⇑φ<VAR>g : G<VAR>hg : 1 = 2<VAR>key : φ g = g<GOAL>False
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>x y : M₁<GOAL>B.IsOrtho x y ↔ B.flip.IsOrtho y x
<VAR>N✝ N : ℕ<VAR>x : SL(2, ℤ)<VAR>HA : x ∈ Gamma1 N<GOAL>x ∈ Gamma0 N
<VAR>N✝ N : ℕ<VAR>x : SL(2, ℤ)<VAR>HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0<GOAL>↑(↑x 1 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : Tendsto (fun x => (m x)⁻¹) f (𝓝 a⁻¹)<GOAL>Tendsto m f (𝓝 a)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜 G<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>inst✝⁷ : TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜₂ G'<VAR>inst✝⁴ : NormedSpace 𝕜' G'<VAR>inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>y : F<GOAL>(f 0) y = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : ↑{0}ᶜ<GOAL>‖↑x‖⁻¹ • ↑x ∈ sphere 0 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : ↑{0}ᶜ<GOAL>↑((fun x => ⟨↑x.2 • ↑x.1, ⋯⟩) ((fun x => (⟨‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖, ⋯⟩)) x)) = ↑x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>hx : x ∈ sphere 0 1<VAR>r : ℝ<VAR>hr : r ∈ Ioi 0<GOAL>(fun x => (⟨‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖, ⋯⟩)) ((fun x => ⟨↑x.2 • ↑x.1, ⋯⟩) (⟨x, hx⟩, ⟨r, hr⟩)) = (⟨x, hx⟩, ⟨r, hr⟩)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>hx✝ : x ∈ sphere 0 1<VAR>hx : ‖x‖ = 1<VAR>r : ℝ<VAR>hr : r ∈ Ioi 0<GOAL>(fun x => (⟨‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖, ⋯⟩)) ((fun x => ⟨↑x.2 • ↑x.1, ⋯⟩) (⟨x, hx✝⟩, ⟨r, hr⟩)) = (⟨x, hx✝⟩, ⟨r, hr⟩)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>hx✝ : x ∈ sphere 0 1<VAR>hx : ‖x‖ = 1<VAR>r : ℝ<VAR>hr✝ : r ∈ Ioi 0<VAR>hr : 0 < r<GOAL>(fun x => (⟨‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖, ⋯⟩)) ((fun x => ⟨↑x.2 • ↑x.1, ⋯⟩) (⟨x, hx✝⟩, ⟨r, hr✝⟩)) = (⟨x, hx✝⟩, ⟨r, hr✝⟩)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous { toFun := fun x => (⟨‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖, ⋯⟩), invFun := fun x => ⟨↑x.2 • ↑x.1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous fun x => ‖↑x‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>∀ (x : ↑{0}ᶜ), ‖↑x‖ ≠ 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous Subtype.val
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous fun x => ⟨‖↑x‖, ⋯⟩
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous { toFun := fun x => (⟨‖↑x‖⁻¹ • ↑x, ⋯⟩, ⟨‖↑x‖, ⋯⟩), invFun := fun x => ⟨↑x.2 • ↑x.1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.invFun
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>(descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>h : DifferentiableOn 𝕜 (fun y => c + f y) s<GOAL>DifferentiableOn 𝕜 f s
<VAR>n m k : ℕ<GOAL>n ^^^ m ^^^ k = n ^^^ (m ^^^ k)
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>x y z w : α<GOAL>(swap x y) z = w ↔ z = (swap x y) w
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : (i : ι) → LT (β i)<VAR>i : ι<VAR>inst✝ : NoMaxOrder (β i)<VAR>a : Lex ((i : ι) → β i)<GOAL>∃ b, a < b
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : (i : ι) → LT (β i)<VAR>i : ι<VAR>inst✝ : NoMaxOrder (β i)<VAR>a : Lex ((i : ι) → β i)<VAR>b : β i<VAR>hb : a i < b<GOAL>∃ b, a < b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : CompleteSpace β<VAR>f : α → β<VAR>h : Isometry f<VAR>x y : Completion α<VAR>x✝¹ x✝ : α<GOAL>dist (Completion.extension f (↑α x✝¹)) (Completion.extension f (↑α x✝)) = dist (↑α x✝¹) (↑α x✝)
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l₁✝ l₂✝ : List α✝<VAR>a : α✝<VAR>s : l₁✝ <+ l₂✝<VAR>h : (a :: l₁✝).length = (a :: l₂✝).length<GOAL>a :: l₁✝ = a :: l₂✝
<VAR>a₁ a₂ : ℤ<VAR>b : ℕ<VAR>h : a₁ % ↑b = a₂ % ↑b<GOAL>J(a₁ | b) = J(a₂ | b)
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<GOAL>↑(last n - i) = ↑i.rev
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>↑p ^ n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>↑p ^ n * wittMul p n + wittPolyProdRemainder p n = ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>wittPolyProdRemainder p n + ↑p ^ n * wittMul p n = ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>W X Y Z : C<GOAL>(ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom) (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫ (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫ (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W) (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) = (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫ (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>W X Y Z : C<GOAL>∀ (j : Discrete WalkingPair), ((ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom) (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫ (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫ (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W) (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫ (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app j = ((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫ (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫ (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app j
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝¹ q✝ r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>p✝ p q : S[X]<VAR>hp : ∃ a, map f a = p<VAR>hq : ∃ a, map f a = q<VAR>p' : R[X]<VAR>hp' : map f p' = p<VAR>q' : R[X]<VAR>hq' : map f q' = q<GOAL>map f (p' + q') = p + q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r✝ : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>p : S[X]<VAR>n : ℕ<VAR>s : S<VAR>r : R<VAR>hr : f r = s<GOAL>map f ((monomial n) r) = (monomial n) s
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩<VAR>g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'<GOAL>P f
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩<VAR>g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'<VAR>hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g<GOAL>P f
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩<VAR>g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'<VAR>hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g<GOAL>P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm g)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩<VAR>g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'<VAR>hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g<GOAL>∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s < ⊤), (fun g => P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ↑(simpleFunc.indicatorConst p hs ⋯ c)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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 F'<VAR>inst✝⁴ : NormedSpace 𝕜 F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩<VAR>g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'<VAR>hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g<GOAL>∀ ⦃f g : α → F⦄ (hf : Memℒp f p (μ.trim hm)) (hg : Memℒp g p (μ.trim hm)), Disjoint (Function.support f) (Function.support g) → (fun g => P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) (Memℒp.toLp f hf) → (fun g => P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) (Memℒp.toLp g hg) → (fun g => P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) (Memℒp.toLp f hf + Memℒp.toLp g hg)