ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>hm : MeasurableSet (κ.mutuallySingularSetSlice η a)<GOAL>((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a) + ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) + (((κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a) + ((κ.singularPart η) a) (s \ κ.mutuallySingularSetSlice η a)) = (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p✝ : Filter ι✝<VAR>g : ι✝ → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>V : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis p V<VAR>f : α →ᵤ[𝔖] β<GOAL>𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : c ≠ 0<GOAL>a < b / c ↔ c * succ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a b : α<VAR>inst✝ : Unique α<VAR>s : Finset α<GOAL>s.Nonempty ↔ s = {default}
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>CNF 0 o = [(0, o)]
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>x : R<GOAL>x ∈ -σ a ↔ x ∈ σ (-a)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>B : Type u_1<VAR>inst✝¹ : CommSemiring B<VAR>inst✝ : Algebra R B<VAR>I J : Submodule R A<VAR>h : A ≃ₐ[R] B<VAR>x : B<GOAL>x ∈ map h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : CommSemiring A<VAR>inst✝² : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>B : Type u_1<VAR>inst✝¹ : CommSemiring B<VAR>inst✝ : Algebra R B<VAR>I J : Submodule R A<VAR>h : A ≃ₐ[R] B<VAR>x : B<GOAL>(∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x) ↔ ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>h : Normal F E<VAR>f : E ≃ₐ[F] E'<GOAL>Normal F E'
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>h : ∀ (x : E), IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)<VAR>f : E ≃ₐ[F] E'<GOAL>∀ (x : E'), IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>f : E ≃ₐ[F] E'<VAR>x : E'<VAR>h : IsIntegral F (f.symm x) ∧ Splits (algebraMap F E) (minpoly F (f.symm x))<GOAL>IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>f : E ≃ₐ[F] E'<VAR>x : E'<VAR>h : IsIntegral F (f.symm x) ∧ Splits (algebraMap F E) (minpoly F (f.symm x))<GOAL>IsIntegral F (f (f.symm x)) ∧ Splits ((↑↑f).comp (algebraMap F E)) (minpoly F (f.symm x))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<VAR>hnk : n ≤ k<GOAL>‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<VAR>hnk : n ≤ k<VAR>hex : ∃ m, k = n + m<GOAL>‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<VAR>hnk : n ≤ k<VAR>hex : ∃ m, k = n + m<VAR>w✝ : ℕ<VAR>hex' : k = n + w✝<GOAL>‖newton_seq (n + w✝) - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<GOAL>(X n).vars = {n}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Lattice β<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : a ≤ b<GOAL>[[a, b]] = Icc a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.sublists' = map reverse l.reverse.sublists
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x - y).leadingCoeff = x.leadingCoeff
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x + -y).leadingCoeff = x.leadingCoeff
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < (-y).orderTop<GOAL>(x + -y).leadingCoeff = x.leadingCoeff
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>V : Set E<GOAL>V ∈ 𝓝 0 ↔ ∃ i, 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>V : Set E<GOAL>(∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V) ↔ ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f₁ f₂ g₁ g₂ : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<VAR>h : f₁ * g₂ = f₂ * g₁<VAR>x : ↥(unop (op U))<GOAL>↑⟨g₁, ⋯⟩ * f₂ = ↑⟨g₂, ⋯⟩ * f₁
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module A M<VAR>inst✝ : Module R M<VAR>D D1 D2 : Derivation R A M<VAR>r : R<VAR>a b : A<VAR>n : ℤ<GOAL>D ↑n = 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>2 • o.oangle (r • x) x = 0
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<VAR>hK' : IsCompact K'<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀