ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := -k +ᵥ t<VAR>k'_comp : IsCompact k'<VAR>g' : P × G → G → E' := fun p x => g p.1 (p.2 - x)<VAR>s' : Set (P × G) := s ×ˢ t<VAR>A : ContinuousOn (uncurry g') (s' ×ˢ univ)<VAR>B : ContinuousOn (fun a => ∫ (x : G), (L (f x)) (g' a x) ∂μ) s'<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := -k +ᵥ t<VAR>k'_comp : IsCompact k'<VAR>g' : P × G → G → E' := fun p x => g p.1 (p.2 - x)<VAR>s' : Set (P × G) := s ×ˢ t<VAR>A : ContinuousOn (uncurry g') (s' ×ˢ univ)<VAR>B : ContinuousOn (fun a => ∫ (x : G), (L (f x)) (g' a x) ∂μ) s'<GOAL>s' ∈ 𝓝[s ×ˢ univ] (q₀, x₀)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s : Set β<GOAL>MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<VAR>inst✝ : Mono f<GOAL>Mono t.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<VAR>inst✝ : Mono f<VAR>W : C<VAR>h k : W ⟶ t.pt<VAR>i : h ≫ t.snd = k ≫ t.snd<GOAL>h ≫ t.fst = k ≫ t.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<VAR>inst✝ : Mono f<VAR>W : C<VAR>h k : W ⟶ t.pt<VAR>i : h ≫ t.snd = k ≫ t.snd<GOAL>h ≫ t.snd ≫ g = k ≫ t.snd ≫ g
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>E : Type u_6<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : UniformSpace E<VAR>f : α → β → E<VAR>s : Set α<VAR>k : Set β<VAR>q : α<VAR>u : Set (E × E)<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)<VAR>hq : q ∈ s<VAR>hu : u ∈ 𝓤 E<GOAL>∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>E : Type u_6<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : UniformSpace E<VAR>f : α → β → E<VAR>s : Set α<VAR>k : Set β<VAR>q : α<VAR>u : Set (E × E)<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)<VAR>hq : q ∈ s<VAR>hu : u ∈ 𝓤 E<GOAL>∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ ∅, (f p x, f q x) ∈ u
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>E : Type u_6<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : UniformSpace E<VAR>f : α → β → E<VAR>s : Set α<VAR>k : Set β<VAR>q : α<VAR>u : Set (E × E)<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)<VAR>hq : q ∈ s<VAR>hu : u ∈ 𝓤 E<GOAL>∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>E : Type u_6<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : UniformSpace E<VAR>f : α → β → E<VAR>s : Set α<VAR>k : Set β<VAR>q : α<VAR>u : Set (E × E)<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)<VAR>hq : q ∈ s<VAR>hu : u ∈ 𝓤 E<GOAL>∀ ⦃s_1 t : Set β⦄, (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) → (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α✝<VAR>inst✝³ : UniformSpace β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>E : Type u_6<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : UniformSpace E<VAR>f : α → β → E<VAR>s : Set α<VAR>k : Set β<VAR>q : α<VAR>u : Set (E × E)<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)<VAR>hq : q ∈ s<VAR>hu : u ∈ 𝓤 E<GOAL>∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B' X✝ Y✝ Y' : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i' : B✝ ⟶ B'<VAR>p✝ : X✝ ⟶ Y✝<VAR>p' : Y✝ ⟶ Y'<VAR>A B X Y : Cᵒᵖ<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>h : HasLiftingProperty i p<VAR>f : Opposite.unop Y ⟶ Opposite.unop B<VAR>g : Opposite.unop X ⟶ Opposite.unop A<VAR>sq : CommSq f p.unop i.unop g<GOAL>sq.HasLift
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B' X✝ Y✝ Y' : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i' : B✝ ⟶ B'<VAR>p✝ : X✝ ⟶ Y✝<VAR>p' : Y✝ ⟶ Y'<VAR>A B X Y : Cᵒᵖ<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>h : HasLiftingProperty i p<VAR>f : Opposite.unop Y ⟶ Opposite.unop B<VAR>g : Opposite.unop X ⟶ Opposite.unop A<VAR>sq : CommSq f p.unop i.unop g<GOAL>⋯.HasLift
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>h : t ⊆ s<GOAL>(s + t).dedup = s.dedup
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<GOAL>ContMDiff I I n e
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<GOAL>ContMDiff I I n e
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<GOAL>Continuous e ∧ ∀ (x : M) (y : H), ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source))
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<GOAL>∀ (x : M) (y : H), ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source))
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<VAR>x : M<VAR>y : H<GOAL>ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source))
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<VAR>x : M<VAR>y : H<GOAL>∀ x_1 ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source), (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm) x_1 = id x_1
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<VAR>x : M<VAR>y : H<VAR>z : E<VAR>hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)<GOAL>↑I (e (↑(OpenEmbedding.toPartialHomeomorph e h).symm (↑I.symm z))) = z
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<VAR>x : M<VAR>y : H<VAR>z : E<VAR>hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)<GOAL>↑I (↑I.symm z) = z
<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<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<VAR>x : M<VAR>y : H<VAR>z : E<VAR>hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)<GOAL>↑I.symm z ∈ range e
<VAR>α : Type u_1<VAR>inst✝² : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝¹ : UniformSpace β<VAR>f : α → β<VAR>inst✝ : T2Space β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>pkg.extend f (pkg.coe a) = f a
<VAR>α : Type u_1<VAR>inst✝² : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝¹ : UniformSpace β<VAR>f : α → β<VAR>inst✝ : T2Space β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>⋯.extend f (pkg.coe a) = f a
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>s s₁ t u✝ : Set E<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra 𝕜 A<VAR>A' : Type u_4<VAR>inst✝³ : NormedCommRing A'<VAR>inst✝² : NormedAlgebra 𝕜 A'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : NormOneClass A'<VAR>u : Finset ι<VAR>f : ι → E → A'<VAR>N : ℕ∞<VAR>hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)<VAR>x : E<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun x => ∏ j ∈ u, f j x) x‖ ≤ ∑ p ∈ u.sym n, ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : 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 F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace 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>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>condexpIndL1 hm μ s x = condexpIndL1Fin hm hs hμs x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : Set (UniformSpace α)<VAR>u₂ : UniformSpace β<VAR>u : UniformSpace α<VAR>h₁ : u ∈ u₁<VAR>hf : UniformContinuous f<GOAL>Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : Set (UniformSpace α)<VAR>u₂ : UniformSpace β<VAR>u : UniformSpace α<VAR>h₁ : u ∈ u₁<VAR>hf : UniformContinuous f<GOAL>Tendsto (fun x => (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>(𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | dist p.1 p.2 < ε}
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>Pairwise (fun a_1 b_1 => ∀ c ∈ if a = a_1.fst then some ⟨a, b⟩ else none, ∀ d ∈ if a = b_1.fst then some ⟨a, b⟩ else none, a_1 = b_1 ∧ c = d) l₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>∀ {a_1 b_1 : Sigma β}, a_1.fst ≠ b_1.fst → ∀ c ∈ if a = a_1.fst then some ⟨a, b⟩ else none, ∀ d ∈ if a = b_1.fst then some ⟨a, b⟩ else none, a_1 = b_1 ∧ c = d
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<VAR>x y : Sigma β<VAR>h : x.fst ≠ y.fst<VAR>h_2 : a = x.fst<VAR>h_1 : a = y.fst<GOAL>x = y ∧ ⟨a, b⟩ = ⟨a, b⟩
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L →ₐ[K] L<VAR>hσ : IsOfFinOrder σ<GOAL>minpoly K σ.toLinearMap = X ^ orderOf σ - C 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L →ₐ[K] L<VAR>hσ : IsOfFinOrder σ<VAR>this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)<GOAL>minpoly K σ.toLinearMap = X ^ orderOf σ - C 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L →ₐ[K] L<VAR>hσ : IsOfFinOrder σ<VAR>this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)<GOAL>minpoly K σ.toLinearMap = minpoly K ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap