ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a✝ b✝ c d : Ordinal.{u}<VAR>a b : Ordinal.{u_1}<GOAL>b ∈ {c | ∀ a' < a, a' ⨳ 1 < c} ↔ b ∈ Set.Ici a
<VAR>a✝ b✝ c d : Ordinal.{u}<VAR>a b : Ordinal.{u_1}<GOAL>(∀ a' < a, a' ⨳ 1 < b) ↔ a ≤ b
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b : Ordinal.{u_1}<VAR>H : ∀ a' < a, a' ⨳ 1 < b<VAR>c : Ordinal.{u_1}<VAR>hc : c < a<GOAL>c < b
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b : Ordinal.{u_1}<VAR>ha : a ≤ b<VAR>c : Ordinal.{u_1}<VAR>hc : c < a<GOAL>c ⨳ 1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>s : Set (β × γ)<GOAL>κ.compProdFun η a s = ∑' (n : ℕ), (κ.seq n).compProdFun η a s
<VAR>q a b c : ℚ<GOAL>a * (b + c) = a * b + a * c
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>hM : IsNilpotent M<VAR>a✝ : Nontrivial R<VAR>p : R[X] := M.charpolyRev<GOAL>IsNilpotent (M.charpoly - X ^ Fintype.card n)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>hM : IsNilpotent M<VAR>a✝ : Nontrivial R<VAR>p : R[X] := M.charpolyRev<VAR>hp : p - 1 = X * (p /ₘ X)<GOAL>IsNilpotent (M.charpoly - X ^ Fintype.card n)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>hM : IsNilpotent M<VAR>a✝ : Nontrivial R<VAR>p : R[X] := M.charpolyRev<VAR>hp : p - 1 = X * (p /ₘ X)<VAR>this : IsNilpotent (p /ₘ X)<GOAL>IsNilpotent (M.charpoly - X ^ Fintype.card n)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>hM : IsNilpotent M<VAR>a✝ : Nontrivial R<VAR>p : R[X] := M.charpolyRev<VAR>hp : p - 1 = X * (p /ₘ X)<VAR>this : IsNilpotent (p /ₘ X)<VAR>aux : (M.charpoly - X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree<GOAL>IsNilpotent (M.charpoly - X ^ Fintype.card n)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>hM : IsNilpotent M<VAR>a✝ : Nontrivial R<VAR>p : R[X] := M.charpolyRev<VAR>hp : p - 1 = X * (p /ₘ X)<VAR>this : IsNilpotent (p /ₘ X)<VAR>aux : (M.charpoly - X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree<GOAL>IsNilpotent (M.charpolyRev - reflect M.charpoly.natDegree (X ^ Fintype.card n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<VAR>p : β → Prop<GOAL>blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>hl : (a :: l).Nodup<GOAL>(permsOfList (a :: l)).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>hl : (a :: l).Nodup<VAR>hl' : l.Nodup<GOAL>(permsOfList (a :: l)).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>hl : (a :: l).Nodup<VAR>hl' : l.Nodup<VAR>hln' : (permsOfList l).Nodup<GOAL>(permsOfList (a :: l)).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>hl : (a :: l).Nodup<VAR>hl' : l.Nodup<VAR>hln' : (permsOfList l).Nodup<VAR>hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a<GOAL>(permsOfList (a :: l)).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>l : List α<VAR>hl : (a :: l).Nodup<VAR>hl' : l.Nodup<VAR>hln' : (permsOfList l).Nodup<VAR>hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a<GOAL>(permsOfList l).Nodup ∧ ((∀ x ∈ l, (List.map (fun f => Equiv.swap a x * f) (permsOfList l)).Nodup) ∧ ∀ (i j : Fin l.length), i < j → (List.map (fun f => Equiv.swap a (l.get i) * f) (permsOfList l)).Disjoint (List.map (fun f => Equiv.swap a (l.get j) * f) (permsOfList l))) ∧ (permsOfList l).Disjoint (l.bind fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
<VAR>x y : ℝ<VAR>h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨ (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2<GOAL>tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>↑(f.pair g) =ᶠ[ae μ] fun x => (↑f x, ↑g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>↑(mk (fun x => (↑f x, ↑g x)) ⋯) =ᶠ[ae μ] fun x => (↑f x, ↑g x)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + (s + 1).Gammaℝ * -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2) (completedSinZeta (↑a) s + (s + 1).Gammaℝ * -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<GOAL>(s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s = ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<GOAL>(s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s = ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / 2 / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<GOAL>(s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑0)) / ↑0 ^ s = ((s + 1).Gammaℝ * -I * ↑(↑0).sign * cexp (2 * ↑π * I * ↑a * ↑0) + (s + 1).Gammaℝ * -I * -↑(↑0).sign * cexp (2 * ↑π * I * ↑a * -↑0)) / 2 / ↑0 ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s = ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / 2 / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(s + 1).Gammaℝ * ((cexp (-↑(2 * π * a * ↑n) * I) - cexp (↑(2 * π * a * ↑n) * I)) * I / 2) / ↑n ^ s = ((s + 1).Gammaℝ * -I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)) / 2 / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(s + 1).Gammaℝ * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) / 2 / ↑n ^ s = (s + 1).Gammaℝ * (-I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)) / 2 / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I = -I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) / ↑n ^ s / 2) (completedSinZeta (↑a) s)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>I * (cexp (-(2 * ↑π * ↑a * ↑n * I)) - cexp (2 * ↑π * ↑a * ↑n * I)) = I * (cexp (-(2 * ↑π * I * ↑a * ↑n)) - cexp (2 * ↑π * I * ↑a * ↑n))
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c₁ c₂ : 𝕜<GOAL>dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c₁ c₂ : 𝕜<GOAL>dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁
<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>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<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>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f : ContinuousAt (fun x => f x (g x)) x₀<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<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>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f✝ : ContinuousAt (fun x => f x (g x)) x₀<VAR>h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝 x₀<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<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>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f✝ : ContinuousAt (fun x => f x (g x)) x₀<VAR>h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝 x₀<VAR>h3f : ∀ᶠ (x' : N × M) in 𝓝 (x₀, g x₀), ContMDiffAt (J.prod I) I' (↑One.one) (uncurry f) x'<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<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>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f✝ : ContinuousAt (fun x => f x (g x)) x₀<VAR>h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝 x₀<VAR>h3f : ∀ᶠ (x' : N × M) in 𝓝 (x₀, g x₀), ContMDiffAt (J.prod I) I' (↑One.one) (uncurry f) x'<VAR>h2f : ∀ᶠ (x₂ : N) in 𝓝 x₀, ContMDiffAt I I' 1 (f x₂) (g x₂)<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀
<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>x₀ : N<VAR>f : N → M → M'<VAR>g : N → M<VAR>hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)<VAR>hg : ContMDiffAt J I m g x₀<VAR>hmn : m + 1 ≤ n<VAR>h4f✝ : ContinuousAt (fun x => f x (g x)) x₀<VAR>h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝 x₀<VAR>h3f : ∀ᶠ (x' : N × M) in 𝓝 (x₀, g x₀), ContMDiffAt (J.prod I) I' (↑One.one) (uncurry f) x'<VAR>h2f : ∀ᶠ (x₂ : N) in 𝓝 x₀, ContMDiffAt I I' 1 (f x₂) (g x₂)<VAR>h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝 x₀<GOAL>ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) x₀) x₀