awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this :
  (↑hf.localInverse.toPartialEquiv : N → M) y ∈
    (Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
        x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).source
⊢ (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
              x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
        M → N)
      ((↑hf.localInverse.toPartialEquiv : N → M) y) =
    y

Tactic:
hf.choose.right_inv hy

Premises used: PartialEquiv.right_inv, Exists.choose, PartialDiffeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this :
  (↑hf.localInverse.toPartialEquiv : N → M) y ∈
    (Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
        x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).source
⊢ (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
              x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
        M → N)
      ((↑hf.localInverse.toPartialEquiv : N → M) y) =
    y

Tactic:
exact hf.choose.right_inv hy

Premises used: PartialEquiv.right_inv, Exists.choose, PartialDiffeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ EqOn (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) id hf.localInverse.source

Tactic:
fun _y hy ↦ hf.localInverse_right_inv hy

Premises used: Set.EqOn, IsLocalDiffeomorphAt.localInverse_right_inv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ f ∘ (↑hf.localInverse.toPartialEquiv : N → M) =ᶠ[nhds (f x)] id

Tactic:
Filter.eventuallyEq_of_mem
    (hf.localInverse.open_source.mem_nhds hf.localInverse_mem_source)
    hf.localInverse_eqOn_right

Premises used: Filter.eventuallyEq_of_mem, IsLocalDiffeomorphAt.localInverse, IsLocalDiffeomorphAt.localInverse_eqOn_right, IsOpen.mem_nhds, IsLocalDiffeomorphAt.localInverse_mem_source, PartialDiffeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
rw :
  (↑hf.localInverse.toPartialEquiv : N → M)
      ((↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
                x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
          M → N)
        x') =
    x'
⊢ (↑hf.localInverse.toPartialEquiv : N → M) (f x') = x'

Tactic:
rw [hf.choose_spec.2 (hf.choose.symm_target ▸ hx')]

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ (↑hf.localInverse.toPartialEquiv : N → M)
      ((↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
                x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
          M → N)
        x') =
    x'

Tactic:
hf.choose.left_inv hx'

Premises used: Exists.choose, PartialEquiv.left_inv, PartialDiffeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ (↑hf.localInverse.toPartialEquiv : N → M)
      ((↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
                x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
          M → N)
        x') =
    x'

Tactic:
exact hf.choose.left_inv hx'

Premises used: Exists.choose, PartialEquiv.left_inv, PartialDiffeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ EqOn ((↑hf.localInverse.toPartialEquiv : N → M) ∘ f) id hf.localInverse.target

Tactic:
fun _ hx ↦ hf.localInverse_left_inv hx

Premises used: Set.EqOn, IsLocalDiffeomorphAt.localInverse_left_inv
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ (↑hf.localInverse.toPartialEquiv : N → M) ∘ f =ᶠ[nhds x] id

Tactic:
Filter.eventuallyEq_of_mem
    (hf.localInverse.open_target.mem_nhds hf.localInverse_mem_target) hf.localInverse_eqOn_left

Premises used: Filter.eventuallyEq_of_mem, IsLocalDiffeomorphAt.localInverse_mem_target, IsLocalDiffeomorphAt.localInverse, IsOpen.mem_nhds, PartialDiffeomorph.open_target, IsLocalDiffeomorphAt.localInverse_eqOn_left
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ IsLocalDiffeomorphAt J I n (↑hf.localInverse.toPartialEquiv : N → M) (f x)

Tactic:
hf.localInverse.isLocalDiffeomorphAt _ _ _ hf.localInverse_mem_source

Premises used: PartialDiffeomorph.isLocalDiffeomorphAt, IsLocalDiffeomorphAt.localInverse, IsLocalDiffeomorphAt.localInverse_mem_source
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ ContMDiffAt J I n (↑hf.localInverse.toPartialEquiv : N → M) (f x)

Tactic:
hf.localInverse_contMDiffOn.contMDiffAt
    (hf.localInverse.open_source.mem_nhds hf.localInverse_mem_source)

Premises used: IsLocalDiffeomorphAt.localInverse_contMDiffOn, IsLocalDiffeomorphAt.localInverse, ContMDiffOn.contMDiffAt, IsOpen.mem_nhds, IsLocalDiffeomorphAt.localInverse_mem_source, PartialDiffeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ MDiffAt (↑hf.localInverse.toPartialEquiv : N → M) (f x)

Tactic:
hf.localInverse_contMDiffAt.mdifferentiableAt hn

Premises used: ContMDiffAt.mdifferentiableAt, IsLocalDiffeomorphAt.localInverse_contMDiffAt
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
⊢ IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : (↑s : Type u_6)), IsLocalDiffeomorphAt I J n f (↑x : M)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
⊢ IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
⊢ IsLocalDiffeomorph I J n f ↔ IsLocalDiffeomorphOn I J n f univ

Tactic:
⟨fun hf x ↦ hf x, fun hf x ↦ hf ⟨x, trivial⟩⟩

Premises used: trivial, Subtype.mk, Iff.intro, Subtype.val
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
s : Set M
⊢ IsLocalDiffeomorphOn I J n f s

Tactic:
fun x ↦ hf x

Premises used: IsLocalDiffeomorphOn, Subtype.val
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
choose :
  ∀ (Φ : PartialDiffeomorph I J M N n) (hx : x ∈ Φ.source) (heq : EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source),
    ContMDiffAt I J n f x
⊢ ContMDiffAt I J n f x

Tactic:
choose Φ hx heq using hf
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source
⊢ ContMDiffAt I J n f x

Tactic:
((Φ.contMDiffOn_toFun).congr heq).contMDiffAt (Φ.open_source.mem_nhds hx)

Premises used: PartialDiffeomorph.contMDiffOn_toFun, ContMDiffOn.contMDiffAt, ContMDiffOn.congr, IsOpen.mem_nhds, PartialDiffeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source
⊢ ContMDiffAt I J n f x

Tactic:
exact ((Φ.contMDiffOn_toFun).congr heq).contMDiffAt (Φ.open_source.mem_nhds hx)

Premises used: PartialDiffeomorph.contMDiffOn_toFun, ContMDiffOn.contMDiffAt, ContMDiffOn.congr, IsOpen.mem_nhds, PartialDiffeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ MDiffAt f x

Tactic:
hf.contMDiffAt.mdifferentiableAt hn

Premises used: ContMDiffAt.mdifferentiableAt, IsLocalDiffeomorphAt.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ ContMDiffOn I J n f s

Tactic:
fun x hx ↦ (hf ⟨x, hx⟩).contMDiffAt.contMDiffWithinAt

Premises used: ContMDiffAt.contMDiffWithinAt, Subtype.mk, IsLocalDiffeomorphAt.contMDiffAt, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
hn : n ≠ 0
⊢ MDiff[s] f

Tactic:
hf.contMDiffOn.mdifferentiableOn hn

Premises used: IsLocalDiffeomorphOn.contMDiffOn, ContMDiffOn.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ ContMDiff I J n f

Tactic:
fun x ↦ (hf x).contMDiffAt

Premises used: ContMDiff, IsLocalDiffeomorphAt.contMDiffAt
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
hn : n ≠ 0
⊢ MDiff f

Tactic:
fun x ↦ (hf x).mdifferentiableAt hn

Premises used: IsLocalDiffeomorphAt.mdifferentiableAt, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
Φ : M ≃ₘ^n⟮I, J⟯ N
_x : M
⊢ _x ∈ Φ.toPartialDiffeomorph.source

Tactic:
trivial
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source
⊢ IsLocalHomeomorphOn f s

Tactic:
apply IsLocalHomeomorphOn.mk

Premises used: IsLocalHomeomorphOn.mk
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
h :
  ∀ (U : PartialDiffeomorph I J M N n)
    (hyp :
      (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx) : M) ∈ U.source ∧ EqOn f (↑U.toPartialEquiv : M → N) U.source),
    ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source
⊢ ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source

Tactic:
choose U hyp using hf ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.Geometry.Manifold.LocalDiffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
x : M
hx : x ∈ s
U : PartialDiffeomorph I J M N n
hyp : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx) : M) ∈ U.source ∧ EqOn f (↑U.toPartialEquiv : M → N) U.source
⊢ ∃ (e : OpenPartialHomeomorph M N), x ∈ e.source ∧ EqOn f (↑e : M → N) e.source

Tactic:
⟨U.toOpenPartialHomeomorph, hyp⟩

Premises used: Exists.intro, PartialDiffeomorph.toOpenPartialHomeomorph