awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
exact extChartAt_preimage_mem_nhds <| hf.continuousAt.preimage_mem_nhds <|
      extChartAt_source_mem_nhds _

Premises used: MDifferentiableAt.continuousAt, ContinuousAt.preimage_mem_nhds, extChartAt_preimage_mem_nhds, extChartAt_source_mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ (extChartAt I' (f x)).target ⊆ range (↑I' : H' → E')

Tactic:
extChartAt_target_subset_range _

Premises used: extChartAt_target_subset_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
E'_1 : Type u_5
inst_6 : NormedAddCommGroup E'_1
inst_7 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_8 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
N_1 : Type u_7
inst_9 : TopologicalSpace N_1
inst_10 : ChartedSpace H'_1 N_1
𝕜 : Type u_1
inst_11 : NontriviallyNormedField 𝕜
E : Type u_2
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
H : Type u_3
inst_14 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
E' : Type u_5
inst_17 : NormedAddCommGroup E'
inst_18 : NormedSpace 𝕜 E'
H' : Type u_6
inst_19 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_20 : TopologicalSpace N
inst_21 : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h : IsRCLikeNormedField 𝕜
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ (extChartAt I' (f x)).target ⊆ range (↑I' : H' → E')

Tactic:
exact extChartAt_target_subset_range _

Premises used: extChartAt_target_subset_range
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
⊢ I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
refine_1 : ∀ (h : I.IsInteriorPoint x), I'.IsInteriorPoint (f x)
refine_2 : ∀ (h : I'.IsInteriorPoint (f x)), I.IsInteriorPoint x
⊢ I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I.IsInteriorPoint x
⊢ I'.IsInteriorPoint (f x)

Tactic:
(hf.mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h

Premises used: IsLocalDiffeomorphAt.mdifferentiableAt, MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I.IsInteriorPoint x
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x))

Tactic:
(hf.mfderivToContinuousLinearEquiv hn).surjective

Premises used: ContinuousLinearEquiv.surjective, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I.IsInteriorPoint x
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace I' (f x))

Tactic:
exact (hf.mfderivToContinuousLinearEquiv hn).surjective

Premises used: ContinuousLinearEquiv.surjective, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
refine_2 : I.IsInteriorPoint ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
⊢ I.IsInteriorPoint x

Tactic:
rw [← hf.localInverse_left_inv hf.localInverse_mem_target]

Premises used: IsLocalDiffeomorphAt.localInverse_mem_target, IsLocalDiffeomorphAt.localInverse_left_inv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ I.IsInteriorPoint ((↑hf.localInverse.toPartialEquiv : N → M) (f x))

Tactic:
(hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h

Premises used: IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
refine_2 :
  Surjective.{u_5 + 1, u_2 + 1} (α := TangentSpace I' (f x)) (β :=
    TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace I' (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
⊢ I.IsInteriorPoint ((↑hf.localInverse.toPartialEquiv : N → M) (f x))

Tactic:
refine (hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h

Premises used: IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ Surjective.{u_5 + 1, u_2 + 1} (α := TangentSpace I' (f x)) (β :=
    TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace I' (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))

Tactic:
(hf.mfderivToContinuousLinearEquiv hn).symm.surjective

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.surjective, TangentSpace, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv, instAddCommGroupTangentSpace._aux_1
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ Surjective.{u_5 + 1, u_2 + 1} (α := TangentSpace I' (f x)) (β :=
    TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace I' (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))

Tactic:
exact (hf.mfderivToContinuousLinearEquiv hn).symm.surjective

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.surjective, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
⊢ I.IsBoundaryPoint x ↔ I'.IsBoundaryPoint (f x)

Tactic:
simp [isBoundaryPoint_iff_not_isInteriorPoint, hf.isInteriorPoint_iff hn]

Premises used: ModelWithCorners.isBoundaryPoint_iff_not_isInteriorPoint, IsLocalDiffeomorphAt.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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I I' n f s
h :
  ∀ (x : M),
    x ∈ f ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s ↔
      x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s
⊢ f ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s

Tactic:
ext x
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I I' n f s
x : M
⊢ x ∈ f ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s ↔
    x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s

Tactic:
simpa using fun hx ↦ ((hf ⟨x, hx⟩).isInteriorPoint_iff hn).symm

Premises used: Subtype.mk, IsLocalDiffeomorphAt.isInteriorPoint_iff, Iff.symm
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I I' n f s
h :
  ∀ (x : M),
    x ∈ f ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s ↔
      x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s
⊢ f ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s =
    ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s

Tactic:
ext x
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I I' n f s
x : M
⊢ x ∈ f ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N ∩ s ↔
    x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∩ s

Tactic:
simpa using fun hx ↦ ((hf ⟨x, hx⟩).isBoundaryPoint_iff hn).symm

Premises used: Subtype.mk, IsLocalDiffeomorphAt.isBoundaryPoint_iff, Iff.symm
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
hf : IsLocalDiffeomorph I I' n f
⊢ f ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
simpa using (hf.isLocalDiffeomorphOn univ).preimage_interior_inter hn

Premises used: Set.univ, IsLocalDiffeomorphOn.preimage_interior_inter, IsLocalDiffeomorph.isLocalDiffeomorphOn
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
hf : IsLocalDiffeomorph I I' n f
⊢ f ⁻¹' ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N =
    ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
simpa using (hf.isLocalDiffeomorphOn univ).preimage_boundary_inter hn

Premises used: Set.univ, IsLocalDiffeomorph.isLocalDiffeomorphOn, IsLocalDiffeomorphOn.preimage_boundary_inter
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
hf : IsLocalDiffeomorph I I' n f
inst_11 : BoundarylessManifold I' N
⊢ BoundarylessManifold I M

Tactic:
simp [← Boundaryless.iff_boundary_eq_empty, ← hf.preimage_boundary hn,
    Boundaryless.boundary_eq_empty]

Premises used: ModelWithCorners.Boundaryless.iff_boundary_eq_empty, ModelWithCorners.Boundaryless.boundary_eq_empty, IsLocalDiffeomorph.preimage_boundary
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
Φ : M ≃ₘ^n⟮I, I'⟯ N
⊢ (⇑Φ : (a : M) → N) ⁻¹' ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := I') N =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
Φ.isLocalDiffeomorph.preimage_interior hn

Premises used: Diffeomorph.isLocalDiffeomorph, IsLocalDiffeomorph.preimage_interior