ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>x : M<VAR>n : ℕ∞<VAR>g : N → N'<VAR>y : N<VAR>hf : ContMDiffAt I I' n f x<VAR>hg : ContMDiffAt J J' n g y<GOAL>ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>n : ℕ∞<VAR>g : N → N'<VAR>p : M × N<VAR>hf : ContMDiffAt I I' n f p.1<VAR>hg : ContMDiffAt J J' n g p.2<GOAL>ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>g : N → N'<VAR>r : Set N<VAR>hf : ContMDiffOn I I' n f s<VAR>hg : ContMDiffOn J J' n g r<GOAL>ContMDiffOn (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>n : ℕ∞<VAR>g : N → N'<VAR>hf : ContMDiff I I' n f<VAR>hg : ContMDiff J J' n g<GOAL>ContMDiff (I.prod J) (I'.prod J') n (Prod.map f g)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>g : N → N'<VAR>r : Set N<VAR>y : N<VAR>hf : SmoothWithinAt I I' f s x<VAR>hg : SmoothWithinAt J J' g r y<GOAL>SmoothWithinAt (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>x : M<VAR>g : N → N'<VAR>y : N<VAR>hf : SmoothAt I I' f x<VAR>hg : SmoothAt J J' g y<GOAL>SmoothAt (I.prod J) (I'.prod J') (Prod.map f g) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>s : Set M<VAR>g : N → N'<VAR>r : Set N<VAR>hf : SmoothOn I I' f s<VAR>hg : SmoothOn J J' g r<GOAL>SmoothOn (I.prod J) (I'.prod J') (Prod.map f g) (s ×ˢ r)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>f : M → M'<VAR>g : N → N'<VAR>hf : Smooth I I' f<VAR>hg : Smooth J J' g<GOAL>Smooth (I.prod J) (I'.prod J') (Prod.map f g)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>ContMDiffWithinAt I 𝓘(𝕜, (i : ι) → Fi i) n φ s x ↔ ∀ (i : ι), ContMDiffWithinAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>n : ℕ∞<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>ContMDiffOn I 𝓘(𝕜, (i : ι) → Fi i) n φ s ↔ ∀ (i : ι), ContMDiffOn I 𝓘(𝕜, Fi i) n (fun x => φ x i) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>n : ℕ∞<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>ContMDiffAt I 𝓘(𝕜, (i : ι) → Fi i) n φ x ↔ ∀ (i : ι), ContMDiffAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>n : ℕ∞<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>ContMDiff I 𝓘(𝕜, (i : ι) → Fi i) n φ ↔ ∀ (i : ι), ContMDiff I 𝓘(𝕜, Fi i) n fun x => φ x i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>x : M<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>SmoothWithinAt I 𝓘(𝕜, (i : ι) → Fi i) φ s x ↔ ∀ (i : ι), SmoothWithinAt I 𝓘(𝕜, Fi i) (fun x => φ x i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>SmoothOn I 𝓘(𝕜, (i : ι) → Fi i) φ s ↔ ∀ (i : ι), SmoothOn I 𝓘(𝕜, Fi i) (fun x => φ x i) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>SmoothAt I 𝓘(𝕜, (i : ι) → Fi i) φ x ↔ ∀ (i : ι), SmoothAt I 𝓘(𝕜, Fi i) (fun x => φ x i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>ι : Type u_21<VAR>Fintype ι<VAR>Fi : ι → Type u_22<VAR>(i : ι) → NormedAddCommGroup (Fi i)<VAR>(i : ι) → NormedSpace 𝕜 (Fi i)<VAR>φ : M → (i : ι) → Fi i<GOAL>Smooth I 𝓘(𝕜, (i : ι) → Fi i) φ ↔ ∀ (i : ι), Smooth I 𝓘(𝕜, Fi i) fun x => φ x i
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>φ φ' : B → F ≃L[𝕜] F<VAR>U U' : Set B<VAR>hU : IsOpen U<VAR>hφ : ContinuousOn (fun x => ↑(φ x)) U<VAR>h2φ : ContinuousOn (fun x => ↑(φ x).symm) U<VAR>hU' : IsOpen U'<VAR>hφ' : ContinuousOn (fun x => ↑(φ' x)) U'<VAR>h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'<VAR>b : B<VAR>v : F<GOAL>↑(FiberwiseLinear.partialHomeomorph φ hU hφ h2φ ≫ₕ FiberwiseLinear.partialHomeomorph φ' hU' hφ' h2φ') (b, v) = (b, (φ' b) ((φ b) v))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>φ φ' : B → F ≃L[𝕜] F<VAR>U U' : Set B<VAR>hU : IsOpen U<VAR>hφ : ContinuousOn (fun x => ↑(φ x)) U<VAR>h2φ : ContinuousOn (fun x => ↑(φ x).symm) U<VAR>hU' : IsOpen U'<VAR>hφ' : ContinuousOn (fun x => ↑(φ' x)) U'<VAR>h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'<GOAL>(FiberwiseLinear.partialHomeomorph φ hU hφ h2φ ≫ₕ FiberwiseLinear.partialHomeomorph φ' hU' hφ' h2φ').source = (U ∩ U') ×ˢ Set.univ
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>φ φ' : B → F ≃L[𝕜] F<VAR>U U' : Set B<VAR>hU : IsOpen U<VAR>hφ : ContinuousOn (fun x => ↑(φ x)) U<VAR>h2φ : ContinuousOn (fun x => ↑(φ x).symm) U<VAR>hU' : IsOpen U'<VAR>hφ' : ContinuousOn (fun x => ↑(φ' x)) U'<VAR>h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'<GOAL>(FiberwiseLinear.partialHomeomorph φ hU hφ h2φ ≫ₕ FiberwiseLinear.partialHomeomorph φ' hU' hφ' h2φ').target = (U ∩ U') ×ˢ Set.univ
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>TopologicalSpace HB<VAR>ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>h : ∀ p ∈ e.source, ∃ s, IsOpen s ∧ p ∈ s ∧ ∃ φ u, ∃ (hu : IsOpen u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr s).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)<GOAL>∃ U, e.source = U ×ˢ Set.univ ∧ ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>TopologicalSpace HB<VAR>ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>U : Set B<VAR>hU : e.source = U ×ˢ Set.univ<VAR>h : ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)<GOAL>∃ Φ U, ∃ (hU₀ : IsOpen U) (hΦ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(Φ x)) U) (h2Φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(Φ x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph Φ hU₀ ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>TopologicalSpace HB<VAR>ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<GOAL>e ∈ ⋃ φ, ⋃ U, ⋃ (hU : IsOpen U), ⋃ (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) U), ⋃ (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) U), {e | e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)} ↔ ∃ φ U, ∃ (hU : IsOpen U) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) U) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>TopologicalSpace B<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>TopologicalSpace HB<VAR>ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<GOAL>e ∈ smoothFiberwiseLinear B F IB ↔ ∃ φ U, ∃ (hU : IsOpen U) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) U) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)
<VAR>self : AlgebraicGeometry.LocallyRingedSpace<VAR>x : ↑↑self.toPresheafedSpace<GOAL>LocalRing ↑(self.presheaf.stalk x)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>self : X.Hom Y<VAR>x : ↑↑X.toPresheafedSpace<GOAL>IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap self.val x)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>h : f.val = g.val<GOAL>f = g
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>X.id.val = 𝟙 X.toSheafedSpace
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.map f = f.val
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.obj X = X.toSheafedSpace
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>AlgebraicGeometry.LocallyRingedSpace.forgetToTop.obj X = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace
<GOAL>∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y), AlgebraicGeometry.LocallyRingedSpace.forgetToTop.map f = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map f.val
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).val = f.val ≫ g.val
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>(𝟙 X).val = 𝟙 X.toSheafedSpace
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f.val ≫ g.val).c = g.val.c ≫ (TopCat.Presheaf.pushforward CommRingCat g.val.base).map f.val.c
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : (TopologicalSpace.Opens ↑Z.toTopCat)ᵒᵖ<GOAL>(f ≫ g).val.c.app U = g.val.c.app U ≫ f.val.c.app (Opposite.op ((TopologicalSpace.Opens.map g.val.base).obj (Opposite.unop U)))
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X.toSheafedSpace ⟶ Y.toSheafedSpace<VAR>CategoryTheory.IsIso f<GOAL>(AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso f).val = f
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<GOAL>∀ {X_1 Y : (TopologicalSpace.Opens ↑U)ᵒᵖ} (f_1 : X_1 ⟶ Y), (X.restrict h).presheaf.map f_1 = X.presheaf.map (⋯.functor.map f_1.unop).op
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑U)ᵒᵖ), (X.restrict h).presheaf.obj X_1 = X.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop X_1)))
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<GOAL>↑(X.restrict h).toPresheafedSpace = U
<GOAL>AlgebraicGeometry.LocallyRingedSpace.Γ = AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.op ⋙ AlgebraicGeometry.SheafedSpace.Γ
<VAR>X : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ<GOAL>AlgebraicGeometry.LocallyRingedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<GOAL>AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.LocallyRingedSpace.Γ.map f = f.unop.val.c.app (Opposite.op ⊤)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.LocallyRingedSpace.Γ.map f.op = f.val.c.app (Opposite.op ⊤)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<VAR>s : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>(TopologicalSpace.Opens.map f.val.base).obj (Y.toRingedSpace.basicOpen s) = X.toRingedSpace.basicOpen ((f.val.c.app (Opposite.op U)) s)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<GOAL>X.toRingedSpace.basicOpen 0 = ⊥
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>hf : IsNilpotent f<GOAL>X.toRingedSpace.basicOpen f = ⊥
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<GOAL>e.hom.val.base ≫ e.inv.val.base = 𝟙 ↑X.toPresheafedSpace
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<VAR>x : ↑X.toTopCat<GOAL>e.inv.val.base (e.hom.val.base x) = x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<GOAL>e.inv.val.base ≫ e.hom.val.base = 𝟙 ↑Y.toPresheafedSpace
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<VAR>y : ↑Y.toTopCat<GOAL>e.hom.val.base (e.inv.val.base y) = y
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>x : ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)
<VAR>X Y Z : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (f ≫ g) x = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g (f.val.base x) ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x x' : ↑X.toTopCat<VAR>h : x ⤳ x'<GOAL>Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x' ≫ X.presheaf.stalkSpecializes h
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x x' : ↑X.toTopCat<VAR>h : x ⤳ x'<VAR>y : ↑(Y.presheaf.stalk (f.val.base x'))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) ((Y.presheaf.stalkSpecializes ⋯) y) = (X.presheaf.stalkSpecializes h) ((AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x') y)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>hfg : f = g<VAR>x x' : ↑X.toTopCat<VAR>hxx' : x = x'<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g x'
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>hfg : f = g<VAR>x : ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x x' : ↑X.toTopCat<VAR>hxx' : x = x'<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x'
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<VAR>y : ↑Y.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom (e.inv.val.base y) ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y = Y.presheaf.stalkSpecializes ⋯
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<VAR>y : ↑Y.toTopCat<VAR>z : ↑(Y.presheaf.stalk (e.hom.val.base (e.inv.val.base y)))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y) ((AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom (e.inv.val.base y)) z) = (Y.presheaf.stalkSpecializes ⋯) z
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<VAR>x : ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv (e.hom.val.base x) ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom x = X.presheaf.stalkSpecializes ⋯