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} (α := 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))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ (↑(extChartAt I x) : M → E) x ∈ range (↑I : H → E)

Tactic:
simp
-- 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))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))

Tactic:
rw [fderivWithin_eq_fderiv (I.uniqueDiffOn _ <| by simp) hf''] at hf'

Premises used: fderivWithin_eq_fderiv, ModelWithCorners.uniqueDiffOn
-- 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))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
hf'₁ :
  Surjective.{u_2 + 1, u_5 + 1} (α := TangentSpace I x) (β := TangentSpace I' (f x))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(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:
rw [fderivWithin_eq_fderiv (I.uniqueDiffOn _ <| by simp) hf''] at hf'

Premises used: fderivWithin_eq_fderiv, ModelWithCorners.uniqueDiffOn
-- 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))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
rwa :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(ContinuousLinearMap.restrictScalars ℝ
          (fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x))) :
      (a : E) → E')
rwa₁ rwa₂ rwa₃ rwa₄ :
  Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')

Tactic:
rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars']

Premises used: Real, DifferentiableAt.fderiv_restrictScalars, ContinuousLinearMap.coe_restrictScalars'
-- 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))
    (⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) :
      (a : TangentSpace I x) → TangentSpace I' (f x))
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
⊢ Surjective.{u_2 + 1, u_5 + 1} (α := E) (β := E')
    (⇑(fderiv ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)) : (a : E) → E')

Tactic:
replace hf' : Surjective (fderiv ℝ (writtenInExtChartAt I I' x f) (extChartAt I x x)) := by
    rwa [hf''.fderiv_restrictScalars (𝕜 := ℝ), ContinuousLinearMap.coe_restrictScalars']
-- 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'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)
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')
⊢ DifferentiableAt ℝ (writtenInExtChartAt I I' x f) ((↑(extChartAt I x) : M → E) x)

Tactic:
replace hf'' := hf''.restrictScalars ℝ
-- 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)
refine_4 :
  ∀ (this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) ∈ interior (range (↑I' : H' → E'))),
    I'.IsInteriorPoint (f x)
refine_1 : (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
refine_2 : f ∘ (↑(extChartAt I x).symm : E → M) ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
refine_3 : (extChartAt I' (f x)).target ⊆ range (↑I' : H' → E')
⊢ I'.IsInteriorPoint (f x)

Tactic:
have := hf''.mem_interior_convex_of_surjective_fderiv (Filter.inter_mem ?_ ?_) I'.convex_range
    I'.isClosed_range I'.nonempty_interior (writtenInExtChartAt_mapsTo.mono_right ?_) hf'
-- 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)
this : writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x) ∈ interior (range (↑I' : H' → E'))
⊢ I'.IsInteriorPoint (f x)

Tactic:
simpa using this
-- 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)
refine_1 : (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [← nhdsWithin_eq_nhds.2 (mem_interior_iff_mem_nhds.1 hx)]

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, nhdsWithin_eq_nhds, Iff.mp
-- 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 x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
extChartAt_target_mem_nhdsWithin x

Premises used: extChartAt_target_mem_nhdsWithin
-- 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 x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
exact extChartAt_target_mem_nhdsWithin x

Premises used: extChartAt_target_mem_nhdsWithin
-- 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:
extChartAt_preimage_mem_nhds <| hf.continuousAt.preimage_mem_nhds <|
      extChartAt_source_mem_nhds _

Premises used: MDifferentiableAt.continuousAt, Set.Mem, setOf, ContinuousAt.preimage_mem_nhds, extChartAt_preimage_mem_nhds, Set.inter, extChartAt_source_mem_nhds, Set.preimage