awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)

Tactic:
(hφ' _ (φ.map_source hx)).differentiableWithinAt hn

Premises used: PartialEquiv.map_source, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)

Tactic:
exact (hφ' _ (φ.map_source hx)).differentiableWithinAt hn

Premises used: PartialEquiv.map_source, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ MapsTo (↑φ.symm : E → E) φ.target φ.source

Tactic:
φ.symm_mapsTo

Premises used: PartialEquiv.symm_mapsTo
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ MapsTo (↑φ.symm : E → E) φ.target φ.source

Tactic:
exact φ.symm_mapsTo

Premises used: PartialEquiv.symm_mapsTo
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_2 : UniqueDiffWithinAt 𝕜 φ.source x
refine_2₁ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
refine_2₂ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source x
refine_2₃ : MapsTo (↑φ : E → E) φ.source φ.target
refine_2₄ : UniqueDiffWithinAt 𝕜 φ.source x
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
    (ContinuousLinearMap.id 𝕜 E)

Tactic:
rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]

Premises used: fderivWithin_congr', fderivWithin_id, Set.LeftInvOn.eqOn, PartialEquiv.leftInvOn, fderivWithin_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.source x

Tactic:
I.uniqueDiffOn_extendCoordChange_source _ hx

Premises used: ModelWithCorners.uniqueDiffOn_extendCoordChange_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ UniqueDiffWithinAt 𝕜 φ.source x

Tactic:
exact I.uniqueDiffOn_extendCoordChange_source _ hx

Premises used: ModelWithCorners.uniqueDiffOn_extendCoordChange_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source x

Tactic:
(hφ _ hx).differentiableWithinAt hn

Premises used: ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source x

Tactic:
exact (hφ _ hx).differentiableWithinAt hn

Premises used: ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ MapsTo (↑φ : E → E) φ.source φ.target

Tactic:
φ.mapsTo

Premises used: PartialEquiv.mapsTo
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ MapsTo (↑φ : E → E) φ.source φ.target

Tactic:
exact φ.mapsTo

Premises used: PartialEquiv.mapsTo
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x) : M → E) = (↑I : H → E) ∘ (↑(chartAt H x) : M → H)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x).symm : E → M) = (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (extChartAt I x).source = (toPartialEquiv (chartAt H x)).source

Tactic:
extend_source _

Premises used: OpenPartialHomeomorph.extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ IsOpen[inst_4] (extChartAt I x).source

Tactic:
isOpen_extend_source _

Premises used: OpenPartialHomeomorph.isOpen_extend_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ x ∈ (extChartAt I x).source

Tactic:
simp only [extChartAt_source, mem_chart_source]

Premises used: mem_chart_source, extChartAt_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target

Tactic:
(extChartAt I x).map_source <| mem_extChartAt_source _

Premises used: extChartAt, PartialEquiv.map_source, mem_extChartAt_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (extChartAt I x).target = (↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E)

Tactic:
extend_target _

Premises used: OpenPartialHomeomorph.extend_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
rw : UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E))
⊢ UniqueDiffOn 𝕜 (extChartAt I x).target

Tactic:
rw [extChartAt_target]

Premises used: extChartAt_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E))

Tactic:
I.uniqueDiffOn_preimage (chartAt H x).open_target

Premises used: chartAt, ModelWithCorners.uniqueDiffOn_preimage, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E))

Tactic:
exact I.uniqueDiffOn_preimage (chartAt H x).open_target

Premises used: chartAt, ModelWithCorners.uniqueDiffOn_preimage, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ UniqueDiffWithinAt 𝕜 (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)

Tactic:
uniqueDiffOn_extChartAt_target x _ <| mem_extChartAt_target x

Premises used: mem_extChartAt_target, uniqueDiffOn_extChartAt_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
(extChartAt I x).left_inv (mem_extChartAt_source x)

Premises used: extChartAt, mem_extChartAt_source, PartialEquiv.left_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x : M
hs : s ⊆ (toPartialEquiv (chartAt H x)).source
⊢ MapsTo (↑(extChartAt I x) : M → E) s ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))

Tactic:
mapsTo_extend _ hs

Premises used: extChartAt, OpenPartialHomeomorph.mapsTo_extend
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x x' : M
h rwa rwa₁ rwa₂ rwa₃ : x' ∈ (extChartAt I x).source
⊢ x' ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
rwa [← extChartAt_source I]

Premises used: extChartAt_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (extChartAt I x).source ∈ 𝓝 x

Tactic:
extChartAt_source_mem_nhds' (mem_extChartAt_source x)

Premises used: mem_extChartAt_source, extChartAt_source_mem_nhds'
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
⊢ (extChartAt I x).source ∈ 𝓝[s] x'

Tactic:
mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds' h)

Premises used: mem_nhdsWithin_of_mem_nhds, extChartAt_source_mem_nhds'
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x : M
⊢ (extChartAt I x).source ∈ 𝓝[s] x

Tactic:
mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds x)

Premises used: mem_nhdsWithin_of_mem_nhds, extChartAt_source_mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ ContinuousOn (↑(extChartAt I x) : M → E) (extChartAt I x).source

Tactic:
continuousOn_extend _

Premises used: OpenPartialHomeomorph.continuousOn_extend
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ ContinuousAt (↑(extChartAt I x) : M → E) x

Tactic:
continuousAt_extChartAt' (mem_extChartAt_source x)

Premises used: mem_extChartAt_source, continuousAt_extChartAt'
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x y : M
hy rwa rwa₁ rwa₂ rwa₃ : y ∈ (extChartAt I x).source
⊢ y ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
rwa [← extChartAt_source I]

Premises used: extChartAt_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ map (↑(extChartAt I x) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
map_extChartAt_nhds' <| mem_extChartAt_source x

Premises used: mem_extChartAt_source, map_extChartAt_nhds'
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
rw :
  map (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) (𝓝 x) =
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)
⊢ map (↑(extChartAt I x) : M → E) (𝓝 x) = 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [extChartAt]

Premises used: extChartAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
⊢ map (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) (𝓝 x) =
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)

Tactic:
map_extend_nhds_of_boundaryless (chartAt H x) (mem_chart_source H x)

Premises used: OpenPartialHomeomorph.map_extend_nhds_of_boundaryless, mem_chart_source, chartAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
⊢ map (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) (𝓝 x) =
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)

Tactic:
exact map_extend_nhds_of_boundaryless (chartAt H x) (mem_chart_source H x)

Premises used: OpenPartialHomeomorph.map_extend_nhds_of_boundaryless, mem_chart_source, chartAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : (↑(extChartAt I x) : M → E) y ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 y
rw :
  (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) y)
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) y)

Tactic:
rw [extChartAt]

Premises used: extChartAt
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : (↑(extChartAt I x) : M → E) y ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 y
⊢ y ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
simpa using hx