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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e

Tactic:
assumption
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'

Tactic:
assumption
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
⊢ x ∈ e.source

Tactic:
assumption
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
hex : x ∈ e.source
hex' : x ∈ e'.source
⊢ x ∈ e'.source

Tactic:
assumption
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
rw :
  (↑(extChartAt I x) : M → E) x ∈ interior (extChartAt I x).target ↔
    (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
⊢ I.IsInteriorPoint x ↔ (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target

Tactic:
rw [isInteriorPoint_iff]

Premises used: 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
⊢ (↑(extChartAt I x) : M → E) x ∈ interior (extChartAt I x).target ↔
    (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target

Tactic:
mem_interior_range_iff_of_mem_atlas hn (chart_mem_atlas H x) he (mem_chart_source H x) hx

Premises used: mem_chart_source, Set.Mem, ModelWithCorners.mem_interior_range_iff_of_mem_atlas, chart_mem_atlas
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
⊢ (↑(extChartAt I x) : M → E) x ∈ interior (extChartAt I x).target ↔
    (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target

Tactic:
exact mem_interior_range_iff_of_mem_atlas hn (chart_mem_atlas H x) he (mem_chart_source H x) hx

Premises used: mem_chart_source, ModelWithCorners.mem_interior_range_iff_of_mem_atlas, chart_mem_atlas
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
rw : (↑(e.extend I) : M → E) x ∈ (e.extend I).target
⊢ I.IsBoundaryPoint x ↔ (↑(e.extend I) : M → E) x ∈ frontier (e.extend I).target

Tactic:
rw [← not_iff_not, ← I.isInteriorPoint_iff_not_isBoundaryPoint,
    I.isInteriorPoint_iff_of_mem_atlas hn he hx, mem_interior_iff_notMem_frontier]

Premises used: not_iff_not, mem_interior_iff_notMem_frontier, ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint, ModelWithCorners.isInteriorPoint_iff_of_mem_atlas
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
⊢ (↑(e.extend I) : M → E) x ∈ (e.extend I).target

Tactic:
(e.extend I).mapsTo <| e.extend_source (I := I) ▸ hx

Premises used: Eq.rec, OpenPartialHomeomorph.extend_source, Eq.symm, PartialEquiv.mapsTo, OpenPartialHomeomorph.extend
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
hx : x ∈ e.source
⊢ (↑(e.extend I) : M → E) x ∈ (e.extend I).target

Tactic:
exact (e.extend I).mapsTo <| e.extend_source (I := I) ▸ hx

Premises used: PartialEquiv.mapsTo, OpenPartialHomeomorph.extend
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
⊢ IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨_, ?_, isOpen_extChartAt_preimage (I := I) x
    isOpen_interior, mem_chart_source H x, isInteriorPoint_iff.1 hx⟩

Premises used: Iff.mpr, mem_chart_source, extChartAt, chartAt, PartialEquiv.target, isOpen_interior, isOpen_extChartAt_preimage, isOpen_iff_forall_mem_open, Inter.inter, Set.preimage, And.intro, interior, Exists.intro, Iff.mp, ModelWithCorners.isInteriorPoint_iff, PartialEquiv.source, PartialEquiv.toFun, OpenPartialHomeomorph.toPartialEquiv
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
refine :
  ∀ (x : M) (hx : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M),
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩
        (↑(extChartAt I x) : M → E) ⁻¹' interior (extChartAt I x).target ⊆
      ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨_, ?_, isOpen_extChartAt_preimage (I := I) x
    isOpen_interior, mem_chart_source H x, isInteriorPoint_iff.1 hx⟩

Premises used: Iff.mpr, mem_chart_source, extChartAt, chartAt, PartialEquiv.target, isOpen_interior, isOpen_extChartAt_preimage, isOpen_iff_forall_mem_open, Inter.inter, Set.preimage, And.intro, interior, Exists.intro, Iff.mp, ModelWithCorners.isInteriorPoint_iff, PartialEquiv.source, PartialEquiv.toFun, OpenPartialHomeomorph.toPartialEquiv
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
x : M
hx : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩
      (↑(extChartAt I x) : M → E) ⁻¹' interior (extChartAt I x).target ⊆
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
fun y hy ↦ (I.isInteriorPoint_iff_of_mem_atlas hn (chart_mem_atlas H x) hy.1).2 hy.2

Premises used: Iff.mpr, ModelWithCorners.IsInteriorPoint, Set.Mem, ModelWithCorners.interior, setOf, Set.sUnion, Set.Subset, chart_mem_atlas, And.right, And.left, interior, ModelWithCorners.isInteriorPoint_iff_of_mem_atlas
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
x : M
hx : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∩
      (↑(extChartAt I x) : M → E) ⁻¹' interior (extChartAt I x).target ⊆
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
exact fun y hy ↦ (I.isInteriorPoint_iff_of_mem_atlas hn (chart_mem_atlas H x) hy.1).2 hy.2

Premises used: Iff.mpr, chart_mem_atlas, ModelWithCorners.isInteriorPoint_iff_of_mem_atlas
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
rw : IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
⊢ IsClosed[inst_4] (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
rw [← I.compl_interior, isClosed_compl_iff]

Premises used: ModelWithCorners.compl_interior, isClosed_compl_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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
⊢ IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
I.isOpen_interior hn

Premises used: ModelWithCorners.isOpen_interior
-- 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
n : WithTop ℕ∞
inst_6 : IsManifold I n M
hn : n ≠ 0
⊢ IsOpen[inst_4] (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
exact I.isOpen_interior hn

Premises used: ModelWithCorners.isOpen_interior
-- 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
f : M → N
x : M
hf : MDiffAt f x
hf' :
  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))
hx : I.IsInteriorPoint x
inr :
  ∀
    (this :
      ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_11 : NormedAddCommGroup E]
        [inst_12 : NormedSpace 𝕜 E] {H : Type u_3} [inst_13 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
        {M : Type u_4} [inst_14 : TopologicalSpace M] [inst_15 : ChartedSpace H M] {E' : Type u_5}
        [inst_16 : NormedAddCommGroup E'] [inst_17 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_18 : TopologicalSpace H']
        {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [inst_19 : TopologicalSpace N] [inst_20 : ChartedSpace H' N]
        {f : M → N} {x : M} (hf : MDiffAt f x)
        (hf' :
          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)))
        (hx : I.IsInteriorPoint x) (h : IsRCLikeNormedField 𝕜), I'.IsInteriorPoint (f x)),
    ¬IsRCLikeNormedField 𝕜 → I'.IsInteriorPoint (f x)
wlog :
  ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_11 : NormedAddCommGroup E]
    [inst_12 : NormedSpace 𝕜 E] {H : Type u_3} [inst_13 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
    {M : Type u_4} [inst_14 : TopologicalSpace M] [inst_15 : ChartedSpace H M] {E' : Type u_5}
    [inst_16 : NormedAddCommGroup E'] [inst_17 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_18 : TopologicalSpace H']
    {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [inst_19 : TopologicalSpace N] [inst_20 : ChartedSpace H' N]
    {f : M → N} {x : M} (hf : MDiffAt f x)
    (hf' :
      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)))
    (hx : I.IsInteriorPoint x), IsRCLikeNormedField 𝕜 → I'.IsInteriorPoint (f x)
⊢ I'.IsInteriorPoint (f x)

Tactic:
wlog _ : IsRCLikeNormedField 𝕜

Premises used: IsRCLikeNormedField
-- 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
f : M → N
x : M
hf : MDiffAt f x
hf' :
  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))
hx : I.IsInteriorPoint x
this :
  ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_11 : NormedAddCommGroup E]
    [inst_12 : NormedSpace 𝕜 E] {H : Type u_3} [inst_13 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
    {M : Type u_4} [inst_14 : TopologicalSpace M] [inst_15 : ChartedSpace H M] {E' : Type u_5}
    [inst_16 : NormedAddCommGroup E'] [inst_17 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_18 : TopologicalSpace H']
    {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_7} [inst_19 : TopologicalSpace N] [inst_20 : ChartedSpace H' N]
    {f : M → N} {x : M} (hf : MDiffAt f x)
    (hf' :
      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)))
    (hx : I.IsInteriorPoint x) (h : IsRCLikeNormedField 𝕜), I'.IsInteriorPoint (f x)
h : ¬IsRCLikeNormedField 𝕜
⊢ I'.IsInteriorPoint (f x)

Tactic:
simp [IsInteriorPoint, I'.range_eq_univ_of_not_isRCLikeNormedField ‹_›]

Premises used: ModelWithCorners.IsInteriorPoint, ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField
-- 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
hf' :
  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))
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'
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))

Tactic:
simp only [mfderiv, hf, ite_true] at hf'

Premises used: mfderiv, ite_true
-- 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} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
⊢ range (↑I : H → E) ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
simpa [← mem_interior_iff_mem_nhds] using hx

Premises used: mem_interior_iff_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} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
⊢ DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)

Tactic:
have hf'' := hf.differentiableWithinAt_writtenInExtChartAt.differentiableAt <| by
    simpa [← mem_interior_iff_mem_nhds] using hx