ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm) (e.baseSet ∩ e'.baseSet)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm) (e'.baseSet ∩ e.baseSet)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>b : B<VAR>hb : b ∈ e'.baseSet ∩ e.baseSet<GOAL>↑(Trivialization.coordChangeL 𝕜 e e' b).symm = ↑(Trivialization.coordChangeL 𝕜 e' e b)
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<GOAL>(Measure.pi μ) univ = ∏ i : ι, (μ i) univ
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.reverse.reverse.reverse.rotate n = (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.reverse = l.reverse.rotate (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length + (l.reverse.length - n % l.reverse.length))
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<GOAL>IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<GOAL>∃ M A_1, ∀ (z : ℍ), A_1 ≤ z.im → Complex.abs ((eisensteinSeries a k ∣[k] A) z) ≤ M
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<GOAL>∀ (z : ℍ), 2 ≤ z.im → Complex.abs ((eisensteinSeries a k ∣[k] A) z) ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<GOAL>Complex.abs ((eisensteinSeries a k ∣[k] A) z) ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<VAR>n : ℤ<VAR>hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im<GOAL>Complex.abs ((eisensteinSeries a k ∣[k] A) z) ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<VAR>n : ℤ<VAR>hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im<GOAL>Complex.abs ((eisensteinSeries_SIF (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod ↑N))) A)) k) (ModularGroup.T ^ (↑↑N * n) • z)) ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<VAR>n : ℤ<VAR>hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im<GOAL>∑' (x : Fin 2 → ℤ), Complex.abs (eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)) ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<VAR>n : ℤ<VAR>hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im<VAR>hk' : 2 < ↑k<GOAL>∑' (x : Fin 2 → ℤ), Complex.abs (eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)) ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<VAR>n : ℤ<VAR>hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im<VAR>hk' : 2 < ↑k<GOAL>Summable fun i => r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖i‖ ^ (-k)
<VAR>N : ℕ+<VAR>a : Fin 2 → ZMod ↑N<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : 2 ≤ z.im<VAR>n : ℤ<VAR>hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im<VAR>hk' : 2 < ↑k<GOAL>∀ (i : Fin 2 → ℤ), ‖eisSummand k i (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖i‖ ^ (-k)
<VAR>ι : Type u<VAR>X : ι → Type<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J K : ι → Prop<VAR>a b : ↑C<VAR>i : ι<VAR>h : (π_app C fun x => x ∈ {i}) a = (π_app C fun x => x ∈ {i}) b<GOAL>↑a i = ↑b i
<VAR>ι : Type u<VAR>X : ι → Type<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J K : ι → Prop<VAR>a b : ↑C<VAR>i : ι<VAR>h : ↑((π_app C fun x => x ∈ {i}) a) = ↑((π_app C fun x => x ∈ {i}) b)<GOAL>↑a i = ↑b i
<VAR>ι : Type u<VAR>X : ι → Type<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>C : Set ((i : ι) → X i)<VAR>J K : ι → Prop<VAR>a b : ↑C<VAR>i : ι<VAR>h : (fun j => ↑a ↑j) = fun j => ↑b ↑j<GOAL>↑a i = ↑b i
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : (ZMod p)[X]<GOAL>(expand (ZMod p) p) f = f ^ p
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : (ZMod p)[X]<VAR>h : (expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)<GOAL>(expand (ZMod p) p) f = f ^ p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Nontrivial M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>n m : ℕ<VAR>h : ↑n = ↑m<GOAL>n = m
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Nontrivial M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>n m : ℕ<VAR>h : ↑n = ↑m<VAR>x : M<VAR>hx : x ≠ 0<GOAL>n = m
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Nontrivial M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>n m : ℕ<VAR>x : M<VAR>hx : x ≠ 0<VAR>h : ↑n • x = ↑m • x<GOAL>n = m
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<GOAL>s ⊆ let i := i; let S := ⋃ j, generateMeasurableRec s ↑j; s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<GOAL>s ⊆ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b \ a = b \ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Monoid R<VAR>inst✝ : HasDistribNeg R<GOAL>(-1) ^ 2 = 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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>m_le_n : m ≤ n<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>m_le_n : m ≤ n<VAR>one_le_n : 1 ≤ n<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>m_le_n : m ≤ n<VAR>one_le_n : 1 ≤ n<VAR>U' : UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>m_le_n : m ≤ n<VAR>one_le_n : 1 ≤ n<VAR>U' : UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)<GOAL>ContinuousOn (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) ∧ ∀ (x : TangentBundle I H) (y : TangentBundle I' H'), ContDiffOn 𝕜 m (↑(extChartAt I'.tangent y) ∘ tangentMapWithin I I' f s ∘ ↑(extChartAt I.tangent x).symm) ((extChartAt I.tangent x).target ∩ ↑(extChartAt I.tangent x).symm ⁻¹' (TotalSpace.proj ⁻¹' s ∩ tangentMapWithin I I' f s ⁻¹' (extChartAt I'.tangent 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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>m_le_n : m ≤ n<VAR>one_le_n : 1 ≤ n<VAR>U' : UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)<VAR>p : TangentBundle I H<VAR>q : TangentBundle I' H'<GOAL>ContDiffOn 𝕜 m (↑(extChartAt I'.tangent q) ∘ tangentMapWithin I I' f s ∘ ↑(extChartAt I.tangent p).symm) ((extChartAt I.tangent p).target ∩ ↑(extChartAt I.tangent p).symm ⁻¹' (TotalSpace.proj ⁻¹' s ∩ tangentMapWithin I I' f s ⁻¹' (extChartAt I'.tangent q).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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>m_le_n : m ≤ n<VAR>one_le_n : 1 ≤ n<VAR>U' : UniqueDiffOn 𝕜 (range ↑I ∩ ↑I.symm ⁻¹' s)<VAR>p : TangentBundle I H<VAR>q : TangentBundle I' H'<GOAL>ContDiffOn 𝕜 m (fun p => (↑I' (f (↑I.symm p.1)), (mfderivWithin I I' f s (↑I.symm p.1)) p.2)) ((range ↑I ∩ ↑I.symm ⁻¹' s) ×ˢ univ)