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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e' e))

Tactic:
uniqueDiffOn_extendCoordChange_source

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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e' e))

Tactic:
exact uniqueDiffOn_extendCoordChange_source

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
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
rw :
  ContDiffOn 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
    ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
    (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))

Tactic:
rw [I.extendCoordChange_source, I.image_eq]

Premises used: ModelWithCorners.image_eq, ModelWithCorners.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
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
    ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))

Tactic:
(StructureGroupoid.compatible_of_mem_maximalAtlas he he').1

Premises used: ContDiffOn, StructureGroupoid.compatible_of_mem_maximalAtlas, OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', And.left
-- 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
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
    ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))

Tactic:
exact (StructureGroupoid.compatible_of_mem_maximalAtlas he he').1

Premises used: StructureGroupoid.compatible_of_mem_maximalAtlas, And.left
-- 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
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
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
apply : PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈ 𝓝[range (↑I : H → E)] x
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E) (range (↑I : H → E)) x

Tactic:
apply (I.contDiffOn_extendCoordChange he he' x hx).mono_of_mem_nhdsWithin

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, ModelWithCorners.contDiffOn_extendCoordChange
-- 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
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
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
rw : ∀ (hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source), (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x
⊢ PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') ∈ 𝓝[range (↑I : H → E)] x

Tactic:
rw [I.extendCoordChange_source] at hx ⊢

Premises used: ModelWithCorners.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
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
hx : x ∈ (↑I : H → E) '' (e.symm ≫ₕ e').source
obtain :
  ∀ (z : H) (hz : z ∈ (e.symm ≫ₕ e').source),
    (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) z
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] x

Tactic:
obtain ⟨z, hz, rfl⟩ := hx

Premises used: 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
z : H
hz : z ∈ (e.symm ≫ₕ e').source
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) z

Tactic:
I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)

Premises used: OpenPartialHomeomorph.open_source, ModelWithCorners.image_mem_nhdsWithin, IsOpen.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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
z : H
hz : z ∈ (e.symm ≫ₕ e').source
⊢ (↑I : H → E) '' (e.symm ≫ₕ e').source ∈ 𝓝[range (↑I : H → E)] (↑I : H → E) z

Tactic:
exact I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)

Premises used: OpenPartialHomeomorph.open_source, ModelWithCorners.image_mem_nhdsWithin, IsOpen.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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
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 : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E) (range (↑I : H → E))
    ((↑(e.extend I) : M → E) x)

Tactic:
I.contDiffWithinAt_extendCoordChange he he' ?_

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange
-- 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
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 : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
refine :
  Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E) (range (↑I : H → E))
    ((↑(e.extend I) : M → E) x)

Tactic:
refine I.contDiffWithinAt_extendCoordChange he he' ?_

Premises used: ModelWithCorners.contDiffWithinAt_extendCoordChange
-- 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
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 : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
rw : (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)
⊢ Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))
    ((↑(e.extend I) : M → E) x)

Tactic:
rw [← OpenPartialHomeomorph.extend_image_source_inter]

Premises used: OpenPartialHomeomorph.extend_image_source_inter
-- 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
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 : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)

Tactic:
mem_image_of_mem _ ⟨hxe, hxe'⟩

Premises used: Set.mem_image_of_mem, And.intro
-- 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
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 : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ (↑(e.extend I) : M → E) x ∈ (↑(e.extend I) : M → E) '' (e.source ∩ e'.source)

Tactic:
exact mem_image_of_mem _ ⟨hxe, hxe'⟩
-- 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
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
⊢ ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n
    (↑(PartialEquiv.symm (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) : E → E)
    (PartialEquiv.target (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'))

Tactic:
I.contDiffOn_extendCoordChange he' he

Premises used: PartialEquiv.trans, PartialEquiv.symm, PartialEquiv.trans', ModelWithCorners.contDiffOn_extendCoordChange, OpenPartialHomeomorph.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
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
hx : Membership.mem (γ := Set E) (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x
set :
  let φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e';
  ∀ (hx : x ∈ φ.source), ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)
⊢ ContinuousLinearMap.IsInvertible
    (fderivWithin 𝕜 (↑(extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e') : E → E)
      (PartialEquiv.source (extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e')) x)

Tactic:
set φ := I.extendCoordChange e e'

Premises used: ModelWithCorners.extendCoordChange
-- 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
⊢ ContDiffOn 𝕜 n (↑φ : E → E) φ.source

Tactic:
have hφ : ContDiffOn 𝕜 n φ φ.source := I.contDiffOn_extendCoordChange he he'
-- 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
⊢ ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target

Tactic:
have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extendCoordChange_symm he he'
-- 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
⊢ ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)

Tactic:
.of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_

Premises used: ContinuousLinearMap.IsInvertible.of_inverse
-- 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_1 :
  Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)
refine_2 :
  Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
    (ContinuousLinearMap.id 𝕜 E)
⊢ ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)

Tactic:
refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_
-- 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_1 : UniqueDiffWithinAt 𝕜 φ.target ((↑φ : E → E) x)
refine_1₁ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source ((↑φ.symm : E → E) ((↑φ : E → E) x))
refine_1₂ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
refine_1₃ : MapsTo (↑φ.symm : E → E) φ.target φ.source
refine_1₄ : UniqueDiffWithinAt 𝕜 φ.target ((↑φ : E → E) x)
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)

Tactic:
rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]

Premises used: Set.RightInvOn.eqOn, fderivWithin_congr', fderivWithin_id, PartialEquiv.map_source, PartialEquiv.right_inv, PartialEquiv.left_inv, fderivWithin_comp, PartialEquiv.rightInvOn
-- 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 𝕜 φ.target ((↑φ : E → E) x)

Tactic:
I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)

Premises used: PartialEquiv.trans, PartialEquiv.symm, PartialEquiv.map_source, ModelWithCorners.uniqueDiffOn_extendCoordChange_source, PartialEquiv.trans', OpenPartialHomeomorph.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
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 𝕜 φ.target ((↑φ : E → E) x)

Tactic:
exact I.uniqueDiffOn_extendCoordChange_source _ (φ.map_source hx)

Premises used: PartialEquiv.map_source, 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 ((↑φ.symm : E → E) ((↑φ : E → E) x))

Tactic:
(φ.left_inv hx ▸ ((hφ _ hx).differentiableWithinAt hn) :)
-- 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 ((↑φ.symm : E → E) ((↑φ : E → E) x))

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