awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
rw : (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈ frontier (range (↑I : H → E))
⊢ (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    frontier (range (↑I : H → E))

Tactic:
rw [Sum.inl_injective.extend_apply (chartAt H x)]

Premises used: chartAt, Sum.inl_injective, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈ frontier (range (↑I : H → E))

Tactic:
simpa [I.isBoundaryPoint_iff, extChartAt] using hx

Premises used: extChartAt, ModelWithCorners.isBoundaryPoint_iff
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
dsimp :
  (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inr x) ∈
    interior
      (PartialEquiv.target (α := M ⊕ M')
        (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I))

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
rw :
  (↑I : H → E) ((↑(chartAt H x) : M' → H) x) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
⊢ (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)

Tactic:
rw [Sum.inr_injective.extend_apply (chartAt H x)]

Premises used: Sum.inr_injective, chartAt, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
⊢ (↑I : H → E) ((↑(chartAt H x) : M' → H) x) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)

Tactic:
simpa [I.isInteriorPoint_iff, extChartAt] using hx

Premises used: extChartAt, ModelWithCorners.isInteriorPoint_iff
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
rw :
  (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inr x) ∈
    frontier (range (↑I : H → E))
⊢ I.IsBoundaryPoint (M := M ⊕ M') (Sum.inr x)

Tactic:
rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, ModelWithCorners.isBoundaryPoint_iff
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
dsimp :
  (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
    frontier (range (↑I : H → E))
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inr x) ∈
    frontier (range (↑I : H → E))

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
rw : (↑I : H → E) ((↑(chartAt H x) : M' → H) x) ∈ frontier (range (↑I : H → E))
⊢ (↑I : H → E) (extend Sum.inr (↑(chartAt H x) : M' → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inr x)) ∈
    frontier (range (↑I : H → E))

Tactic:
rw [Sum.inr_injective.extend_apply (chartAt H x)]

Premises used: Sum.inr_injective, chartAt, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ (↑I : H → E) ((↑(chartAt H x) : M' → H) x) ∈ frontier (range (↑I : H → E))

Tactic:
simpa [I.isBoundaryPoint_iff, extChartAt] using hx

Premises used: extChartAt, ModelWithCorners.isBoundaryPoint_iff
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
⊢ I.IsInteriorPoint (p.getLeft hleft)

Tactic:
grind [isInteriorPoint_iff_not_isBoundaryPoint, boundaryPoint_inl]

Premises used: ModelWithCorners.boundaryPoint_inl, ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hright : p.isRight = true
⊢ I.IsInteriorPoint (p.getRight hright)

Tactic:
grind [isInteriorPoint_iff_not_isBoundaryPoint, boundaryPoint_inr]

Premises used: ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint, ModelWithCorners.boundaryPoint_inr
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
⊢ ModelWithCorners.interior (𝕜 := 𝕜) (E := E) (H := H) (I := I) (M ⊕ M') =
    Sum.inl '' ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∪
      Sum.inr '' ModelWithCorners.interior.{u_1, u_2, u_3, u_5} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M'

Tactic:
grind [boundaryPoint_inl, boundaryPoint_inr, interior.eq_def, interiorPoint_inl,
    interiorPoint_inr, isInteriorPoint_iff_not_isBoundaryPoint]

Premises used: ModelWithCorners.interior.eq_def, ModelWithCorners.boundaryPoint_inl, ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint, ModelWithCorners.boundaryPoint_inr, ModelWithCorners.interiorPoint_inl, ModelWithCorners.interiorPoint_inr
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
⊢ ModelWithCorners.boundary (𝕜 := 𝕜) (E := E) (H := H) (I := I) (M ⊕ M') =
    Sum.inl '' ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∪
      Sum.inr '' ModelWithCorners.boundary.{u_1, u_2, u_3, u_5} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M'

Tactic:
simp only [← ModelWithCorners.compl_interior, interior_disjointUnion, inl_compl_union_inr_compl]

Premises used: ModelWithCorners.interior_disjointUnion, ModelWithCorners.compl_interior, Set.inl_compl_union_inr_compl
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
hM : BoundarylessManifold I M
hM' : BoundarylessManifold I M'
rw :
  ∀ (hM : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅)
    (hM' : ModelWithCorners.boundary.{u_1, u_2, u_3, u_5} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M' = ∅),
    Eq (α := Set (M ⊕ M')) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E) (H := H) (I := I) (M ⊕ M')) ∅
⊢ BoundarylessManifold I (M ⊕ M')

Tactic:
rw [← Boundaryless.iff_boundary_eq_empty] at hM hM' ⊢

Premises used: ModelWithCorners.Boundaryless.iff_boundary_eq_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
hM : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
hM' : ModelWithCorners.boundary.{u_1, u_2, u_3, u_5} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M' = ∅
⊢ Eq (α := Set (M ⊕ M')) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E) (H := H) (I := I) (M ⊕ M')) ∅

Tactic:
simp [boundary_disjointUnion, hM, hM']

Premises used: ModelWithCorners.boundary_disjointUnion
-- 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 ℕ∞
Φ : PartialDiffeomorph I J M N n
⊢ ContMDiffOn I J n (↑Φ.toPartialEquiv : M → N) Φ.source

Tactic:
Φ.contMDiffOn_toFun

Premises used: PartialDiffeomorph.contMDiffOn_toFun
-- 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 ℕ∞
Φ : PartialDiffeomorph I J M N n
hn : n ≠ 0
⊢ MDiff[Φ.source] (↑Φ.toPartialEquiv : M → N)

Tactic:
(Φ.contMDiffOn).mdifferentiableOn hn

Premises used: PartialDiffeomorph.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 ℕ∞
Φ : PartialDiffeomorph I J M N n
hn : n ≠ 0
x : M
hx : x ∈ Φ.source
⊢ MDiffAt (↑Φ.toPartialEquiv : M → N) x

Tactic:
(Φ.mdifferentiableOn hn x hx).mdifferentiableAt (Φ.open_source.mem_nhds hx)

Premises used: PartialDiffeomorph.mdifferentiableOn, MDifferentiableWithinAt.mdifferentiableAt, 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 ℕ∞
φ : PartialDiffeomorph I J M N n
x : M
hx : x ∈ φ.source
⊢ IsLocalDiffeomorphAt I J n (↑φ.toPartialEquiv : M → N) x

Tactic:
⟨φ, hx, Set.eqOn_refl _ _⟩

Premises used: IsLocalDiffeomorphAt, And.intro, Exists.intro, Set.eqOn_refl
-- 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
⊢ IsOpen hf.localInverse.source

Tactic:
PartialDiffeomorph.open_source _

Premises used: 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
rw :
  (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
              x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
        M → N)
      x ∈
    hf.localInverse.source
⊢ f x ∈ hf.localInverse.source

Tactic:
rw [(hf.choose_spec.2 hf.choose_spec.1)]

Premises used: Exists.choose_spec, And.right, And.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
⊢ (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
              x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
        M → N)
      x ∈
    hf.localInverse.source

Tactic:
(Classical.choose hf).map_source hf.choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, PartialEquiv.map_source, And.left, Classical.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
⊢ (↑(Exists.choose (p := fun (Φ : PartialDiffeomorph I J M N n) ↦
              x ∈ Φ.source ∧ EqOn f (↑Φ.toPartialEquiv : M → N) Φ.source) hf).toPartialEquiv :
        M → N)
      x ∈
    hf.localInverse.source

Tactic:
exact (Classical.choose hf).map_source hf.choose_spec.1

Premises used: Exists.choose_spec, PartialEquiv.map_source, And.left, Classical.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
⊢ x ∈ hf.localInverse.target

Tactic:
hf.choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, And.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
⊢ ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv : N → M) hf.localInverse.source

Tactic:
hf.localInverse.contMDiffOn_toFun

Premises used: PartialDiffeomorph.contMDiffOn_toFun, IsLocalDiffeomorphAt.localInverse
-- 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
⊢ (↑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).symm.target

Tactic:
hf.choose.symm.map_source hy

Premises used: PartialDiffeomorph.symm, Set.Mem, PartialEquiv.map_source, 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
⊢ (↑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).symm.target

Tactic:
exact hf.choose.symm.map_source hy

Premises used: PartialDiffeomorph.symm, PartialEquiv.map_source, 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
⊢ (↑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

Tactic:
have : hf.localInverse y ∈ hf.choose.source := by
    rw [← hf.choose.symm_target]
    exact hf.choose.symm.map_source 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
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
rw :
  (↑(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
⊢ f ((↑hf.localInverse.toPartialEquiv : N → M) y) = y

Tactic:
rw [hf.choose_spec.2 this]

Premises used: Exists.choose_spec, And.right