ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>self : ChartedSpace H M<VAR>x : M<GOAL>ChartedSpace.chartAt x ∈ ChartedSpace.atlas
<VAR>H : Type u_5<VAR>M : Type u_6<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>x ∈ (chartAt H x).source
<VAR>H : Type u_5<VAR>M : Type u_6<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>chartAt H x ∈ atlas H M
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>e : PartialHomeomorph H H<GOAL>e ∈ atlas H H ↔ e = PartialHomeomorph.refl H
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>x : H<GOAL>chartAt H x = PartialHomeomorph.refl H
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(chartAt H x) x ∈ (chartAt H x).target
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>(chartAt H x).source ∈ 𝓝 x
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>(chartAt H x).target ∈ 𝓝 (↑(chartAt H x) x)
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<GOAL>⋃ x, (chartAt H x).source = Set.univ
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<GOAL>IsOpen s ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>achart H x = ⟨chartAt H x, ⋯⟩
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(achart H x) = chartAt H x
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>x ∈ (↑(achart H x)).source
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SecondCountableTopology H<VAR>s : Set M<VAR>hs : ⋃ x ∈ s, (chartAt H x).source = Set.univ<VAR>hsc : s.Countable<GOAL>SecondCountableTopology M
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SecondCountableTopology H<VAR>SigmaCompactSpace M<GOAL>SecondCountableTopology M
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>LocallyCompactSpace H<GOAL>LocallyCompactSpace M
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>LocallyConnectedSpace H<GOAL>LocallyConnectedSpace M
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>M : Type u_7<VAR>TopologicalSpace M<VAR>ChartedSpace H H'<VAR>ChartedSpace H' M<VAR>x : M<GOAL>chartAt H x = chartAt H' x ≫ₕ chartAt H (↑(chartAt H' x) x)
<VAR>H : Type u_5<VAR>H' : Type u_6<VAR>α : Type u_7<VAR>f : H → α<GOAL>(Set.range fun p => (f p.1, p.2)) = Set.range f ×ˢ Set.univ
<VAR>H : Type u<VAR>H' : Type u_1<VAR>x y : ModelProd H H'<VAR>h₁ : x.1 = y.1<VAR>h₂ : x.2 = y.2<GOAL>x = y
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>x : M × M'<GOAL>chartAt (ModelProd H H') x = (chartAt H x.1).prod (chartAt H' x.2)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<GOAL>prodChartedSpace H H H' H' = chartedSpaceSelf (H × H')
<VAR>ι : Type u_5<VAR>Finite ι<VAR>H : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (H i)<VAR>M : ι → Type u_7<VAR>(i : ι) → TopologicalSpace (M i)<VAR>(i : ι) → ChartedSpace (H i) (M i)<VAR>f : (i : ι) → M i<GOAL>chartAt (ModelPi H) f = PartialHomeomorph.pi fun i => chartAt (H i) (f i)
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>self : ChartedSpaceCore H M<VAR>x : M<GOAL>self.chartAt x ∈ self.atlas
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>self : ChartedSpaceCore H M<VAR>e e' : PartialEquiv M H<GOAL>e ∈ self.atlas → e' ∈ self.atlas → ContinuousOn (↑(e.symm ≫ e')) (e.symm ≫ e').source
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>self : ChartedSpaceCore H M<VAR>e e' : PartialEquiv M H<GOAL>e ∈ self.atlas → e' ∈ self.atlas → IsOpen (e.symm ≫ e').source
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>self : ChartedSpaceCore H M<VAR>x : M<GOAL>x ∈ (self.chartAt x).source
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>c : ChartedSpaceCore H M<VAR>e : PartialEquiv M H<VAR>he : e ∈ c.atlas<GOAL>IsOpen e.source
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>c : ChartedSpaceCore H M<VAR>e : PartialEquiv M H<VAR>he : e ∈ c.atlas<GOAL>IsOpen e.target
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>self : HasGroupoid M G<VAR>e e' : PartialHomeomorph M H<GOAL>e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ G
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>HasGroupoid M G<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>he' : e' ∈ atlas H M<GOAL>e.symm ≫ₕ e' ∈ G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G₁ G₂ : StructureGroupoid H<VAR>h : HasGroupoid M G₁<VAR>hle : G₁ ≤ G₂<GOAL>HasGroupoid M G₂
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G₁ G₂ : StructureGroupoid H<GOAL>HasGroupoid M (G₁ ⊓ G₂) ↔ HasGroupoid M G₁ ∧ HasGroupoid M G₂
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>PG : Pregroupoid H<VAR>h : ∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → PG.property (↑(e.symm ≫ₕ e')) (e.symm ≫ₕ e').source<GOAL>HasGroupoid M PG.groupoid
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>e e' : PartialHomeomorph M H<VAR>G : StructureGroupoid H<VAR>he : e ∈ atlas H M<VAR>he' : e' ∈ atlas H M<VAR>HasGroupoid M G<VAR>ClosedUnderRestriction G<VAR>s : TopologicalSpace.Opens M<VAR>hs : Nonempty ↥s<GOAL>(e.subtypeRestr hs).symm ≫ₕ e'.subtypeRestr hs ∈ G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>HasGroupoid M G<GOAL>atlas H M ⊆ StructureGroupoid.maximalAtlas M G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>HasGroupoid M G<VAR>x : M<GOAL>chartAt H x ∈ StructureGroupoid.maximalAtlas M G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph M H<GOAL>e ∈ StructureGroupoid.maximalAtlas M G ↔ ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>he' : e' ∈ StructureGroupoid.maximalAtlas M G<GOAL>e.symm ≫ₕ e' ∈ G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>h : e' ≈ e<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<GOAL>e' ∈ StructureGroupoid.maximalAtlas M G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<GOAL>PartialHomeomorph.refl H ∈ StructureGroupoid.maximalAtlas H G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>f : PartialHomeomorph H H<VAR>hf : f ∈ G<GOAL>f ∈ StructureGroupoid.maximalAtlas H G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = Set.univ<VAR>x : α<GOAL>chartAt H x = e
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = Set.univ<VAR>x : α<GOAL>(chartAt H x).source = Set.univ
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = Set.univ<VAR>e' : PartialHomeomorph α H<VAR>h' : e' ∈ ChartedSpace.atlas<GOAL>e' = e
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = Set.univ<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<GOAL>HasGroupoid α G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>Nonempty α<VAR>f : α → H<VAR>h : OpenEmbedding f<VAR>x : α<GOAL>↑(chartAt H x) = f
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>Nonempty α<VAR>f : α → H<VAR>h : OpenEmbedding f<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<GOAL>HasGroupoid α G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : TopologicalSpace.Opens M<VAR>hs : Nonempty ↥s<VAR>e : PartialHomeomorph (↥s) H<VAR>he : e ∈ atlas H ↥s<GOAL>∃ x, e = (chartAt H ↑x).subtypeRestr hs
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>t : TopologicalSpace.Opens H<VAR>ht : Nonempty ↥t<VAR>e' : PartialHomeomorph (↥t) H<VAR>he' : e' ∈ atlas H ↥t<GOAL>∃ x, e' = (chartAt H ↑x).subtypeRestr ht
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>U : TopologicalSpace.Opens M<VAR>x : ↥U<GOAL>↑(chartAt H ↑x).symm =ᶠ[𝓝 (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(chartAt H x).symm
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>U V : TopologicalSpace.Opens M<VAR>hUV : U ≤ V<VAR>x : ↥U<GOAL>↑(chartAt H (Set.inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (Set.inclusion hUV x)) (Set.inclusion hUV x))] Set.inclusion hUV ∘ ↑(chartAt H x).symm
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>s : TopologicalSpace.Opens M<VAR>hs : Nonempty ↥s<VAR>G : StructureGroupoid H<VAR>HasGroupoid M G<VAR>ClosedUnderRestriction G<GOAL>e.subtypeRestr hs ∈ StructureGroupoid.maximalAtlas (↥s) G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>TopologicalSpace M<VAR>TopologicalSpace M'<VAR>ChartedSpace H M<VAR>ChartedSpace H M'<VAR>self : Structomorph G M M'<VAR>c : PartialHomeomorph M H<VAR>c' : PartialHomeomorph M' H<GOAL>c ∈ atlas H M → c' ∈ atlas H M' → c.symm ≫ₕ self.toPartialHomeomorph ≫ₕ c' ∈ G
<VAR>H : Type u<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>HasGroupoid M G<VAR>ClosedUnderRestriction G<GOAL>let s := { carrier := e.source, is_open' := ⋯ };
let t := { carrier := e.target, is_open' := ⋯ };
∀ c' ∈ atlas H ↥t, e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ StructureGroupoid.maximalAtlas (↥s) G
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>EB : Type u_8<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜 F₁ E₁<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜 F₂ E₂<VAR>e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj<VAR>SmoothVectorBundle F₁ E₁ IB<VAR>SmoothVectorBundle F₂ E₂ IB<VAR>MemTrivializationAtlas e₁<VAR>MemTrivializationAtlas e₁'<VAR>MemTrivializationAtlas e₂<VAR>MemTrivializationAtlas e₂'<GOAL>SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) (Pretrivialization.continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>HB : Type u_9<VAR>TopologicalSpace HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜 F₁ E₁<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜 F₂ E₂<VAR>y₀ y : LE₁E₂<GOAL>↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y = (↑(chartAt HB y₀.proj) y.proj, ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>M : Type u_5<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>EB : Type u_8<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_10<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜 F₁ E₁<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜 F₂ E₂<VAR>f : M → LE₁E₂<VAR>x₀ : M<VAR>n : ℕ∞<GOAL>ContMDiffAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n f x₀ ↔ ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧ ContMDiffAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n (fun x => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>M : Type u_5<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>(x : B) → AddCommGroup (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>(x : B) → AddCommGroup (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>EB : Type u_8<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_10<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>FiberBundle F₁ E₁<VAR>VectorBundle 𝕜 F₁ E₁<VAR>FiberBundle F₂ E₂<VAR>VectorBundle 𝕜 F₂ E₂<VAR>f : M → LE₁E₂<VAR>x₀ : M<GOAL>SmoothAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) f x₀ ↔ SmoothAt IM IB (fun x => (f x).proj) x₀ ∧ SmoothAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun x => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd) x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>self : LieAddGroup I G<GOAL>Smooth I I fun a => -a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>Group G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>self : LieGroup I G<GOAL>Smooth I I fun a => a⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<GOAL>Smooth I I fun x => x⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<GOAL>Smooth I I fun x => -x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<GOAL>TopologicalAddGroup G
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<GOAL>TopologicalGroup G
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContMDiffWithinAt I' I n f s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContMDiffWithinAt I' I n f s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => -f x) s x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>x₀ : M<VAR>hf : ContMDiffAt I' I n f x₀<GOAL>ContMDiffAt I' I n (fun x => -f x) x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>x₀ : M<VAR>hf : ContMDiffAt I' I n f x₀<GOAL>ContMDiffAt I' I n (fun x => (f x)⁻¹) x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<GOAL>ContMDiffOn I' I n (fun x => (f x)⁻¹) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<GOAL>ContMDiffOn I' I n (fun x => -f x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>hf : ContMDiff I' I n f<GOAL>ContMDiff I' I n fun x => -f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>n : ℕ∞<VAR>f : M → G<VAR>hf : ContMDiff I' I n f<GOAL>ContMDiff I' I n fun x => (f x)⁻¹
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : SmoothWithinAt I' I f s x₀<GOAL>SmoothWithinAt I' I (fun x => -f x) s x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>f : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : SmoothWithinAt I' I f s x₀<GOAL>SmoothWithinAt I' I (fun x => (f x)⁻¹) s x₀