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
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:
exact ⟨U.toOpenPartialHomeomorph, hyp⟩
-- 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
rw : IsLocalHomeomorphOn f univ
⊢ IsLocalHomeomorph f

Tactic:
rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ]

Premises used: isLocalHomeomorph_iff_isLocalHomeomorphOn_univ
-- 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
⊢ IsLocalDiffeomorphOn I J n f univ

Tactic:
rw [isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ] at hf

Premises used: isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ
-- 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 : IsLocalDiffeomorphOn I J n f univ
⊢ IsLocalHomeomorphOn f univ

Tactic:
hf.isLocalHomeomorphOn

Premises used: IsLocalDiffeomorphOn.isLocalHomeomorphOn
-- 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 : IsLocalDiffeomorphOn I J n f univ
⊢ IsLocalHomeomorphOn f univ

Tactic:
exact hf.isLocalHomeomorphOn

Premises used: IsLocalDiffeomorphOn.isLocalHomeomorphOn
-- 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
⊢ IsOpenMap f

Tactic:
(hf.isLocalHomeomorph).isOpenMap

Premises used: IsLocalDiffeomorph.isLocalHomeomorph, IsLocalHomeomorph.isOpenMap
-- 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
⊢ IsOpen (range f)

Tactic:
(hf.isOpenMap).isOpen_range

Premises used: IsLocalDiffeomorph.isOpenMap, IsOpenMap.isOpen_range
-- 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
⊢ hf.image.carrier = range f

Tactic:
rfl

Premises used: setOf, Set.range, 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
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
choose : (g : N → M) → (hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f) → M ≃ₘ^n⟮I, J⟯ N
⊢ M ≃ₘ^n⟮I, J⟯ N

Tactic:
choose g hgInverse using (Function.bijective_iff_has_inverse).mp hf'

Premises used: Function.bijective_iff_has_inverse, Iff.mp
-- 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
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
choose :
  (Φ : (x : M) → PartialDiffeomorph I J M N n) →
    (hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source) → M ≃ₘ^n⟮I, J⟯ N
⊢ M ≃ₘ^n⟮I, J⟯ N

Tactic:
choose Φ hyp using (fun x ↦ hf x)
-- 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
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
⊢ ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target

Tactic:
have aux (x) : EqOn g (Φ x).symm (Φ x).target :=
    eqOn_of_leftInvOn_of_rightInvOn (fun x' _ ↦ hgInverse.1 x')
      (LeftInvOn.congr_left ((Φ x).toOpenPartialHomeomorph).rightInvOn
        ((Φ x).toOpenPartialHomeomorph).symm_mapsTo (hyp x).2.symm)
      (fun _y hy ↦ (Φ x).map_target hy)
-- 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
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
⊢ x ∈ (Φ x).source

Tactic:
obtain ⟨hx, hfx⟩ := hyp x
-- 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
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
⊢ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source

Tactic:
obtain ⟨hx, hfx⟩ := hyp x
-- 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
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
apply : y ∈ (Φ x).target
⊢ ContMDiffAt.{u_1, u_3, u_5, u_7, u_2, u_4, u_6} J I (M' := M) n
    (⇑{ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : M ≃ N }.symm : (a : N) → M) y

Tactic:
apply ((Φ x).symm.contMDiffOn.congr (aux x)).contMDiffAt (((Φ x).open_target).mem_nhds ?_)

Premises used: PartialDiffeomorph.contMDiffOn, PartialDiffeomorph.symm, ContMDiffOn.contMDiffAt, ContMDiffOn.congr, IsOpen.mem_nhds, PartialDiffeomorph.open_target
-- 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
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
⊢ y = (↑(Φ x).toPartialEquiv : M → N) x

Tactic:
have : y = (Φ x) x := ((hgInverse.2 y).congr (hfx hx)).mp 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
s : Set M
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
this : y = (↑(Φ x).toPartialEquiv : M → N) x
⊢ y ∈ (Φ x).target

Tactic:
this ▸ (Φ x).map_source hx

Premises used: Eq.rec, PartialEquiv.map_source, Eq.symm, 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
s : Set M
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
this : y = (↑(Φ x).toPartialEquiv : M → N) x
⊢ y ∈ (Φ x).target

Tactic:
exact this ▸ (Φ x).map_source hx
-- 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
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
⊢ M ≃ₘ^n⟮I, J⟯ N

Tactic:
exact {
    toFun := f
    invFun := g
    left_inv := hgInverse.1
    right_inv := hgInverse.2
    contMDiff_toFun := hf.contMDiff
    contMDiff_invFun := by
      intro y
      let x := g y
      obtain ⟨hx, hfx⟩ := hyp x
      apply ((Φ x).symm.contMDiffOn.congr (aux x)).contMDiffAt (((Φ x).open_target).mem_nhds ?_)
      have : y = (Φ x) x := ((hgInverse.2 y).congr (hfx hx)).mp rfl
      exact this ▸ (Φ x).map_source hx }
-- 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
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
m : 𝕜
x_1 : TangentSpace I x
⊢ ((mfderiv% f x : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace J (f x))) :
        (a : TangentSpace I x) → TangentSpace J (f x))
      (m • x_1) =
    HSMul.hSMul (α := 𝕜) (β := TangentSpace J (f x)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜)
      (((mfderiv% f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace J (f x))) :
            (a : TangentSpace I x) → TangentSpace J (f x))
          x_1 :
        TangentSpace J (f x))

Tactic:
simp
-- 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
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hinv :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
      (mfderiv% f x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ Function.LeftInverse.{u_2 + 1, u_3 + 1} (α := TangentSpace I x) (β := TangentSpace J (f x))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace J (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace J (f x))

Tactic:
apply ContinuousLinearMap.leftInverse_of_comp

Premises used: ContinuousLinearMap.leftInverse_of_comp
-- 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
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hinv :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
      (mfderiv% f x))
    (mfderiv% ((↑hf.localInverse.toPartialEquiv : N → M) ∘ f) x)
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
      (mfderiv% f x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_left.mfderiv_eq]

Premises used: IsLocalDiffeomorphAt.localInverse_eventuallyEq_left, Filter.EventuallyEq.mfderiv_eq, mfderiv_id
-- 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
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
      (mfderiv% f x))
    (mfderiv% ((↑hf.localInverse.toPartialEquiv : N → M) ∘ f) x)

Tactic:
(mfderiv_comp _ (hf.localInverse_mdifferentiableAt hn) (hf.mdifferentiableAt hn)).symm

Premises used: mfderiv_comp, IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, instModuleTangentSpace._aux_1, IsLocalDiffeomorphAt.mdifferentiableAt, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, Eq.symm, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- 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
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
      (mfderiv% f x))
    (mfderiv% ((↑hf.localInverse.toPartialEquiv : N → M) ∘ f) x)

Tactic:
exact (mfderiv_comp _ (hf.localInverse_mdifferentiableAt hn) (hf.mdifferentiableAt hn)).symm

Premises used: mfderiv_comp, IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, IsLocalDiffeomorphAt.mdifferentiableAt, Eq.symm
-- 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
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hinv :
  Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace J (f x)))
⊢ Function.RightInverse.{u_2 + 1, u_3 + 1} (α := TangentSpace I x) (β := TangentSpace J (f x))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace J (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace J (f x))

Tactic:
apply ContinuousLinearMap.rightInverse_of_comp

Premises used: ContinuousLinearMap.rightInverse_of_comp