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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
simp_rw : (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)

Tactic:
simp_rw [φ, extendCoordChange, PartialEquiv.trans_source, PartialEquiv.symm_source,
      Filter.inter_mem_iff, mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source]

Premises used: PartialEquiv.trans_source, mem_interior_iff_mem_nhds, PartialEquiv.symm_source, OpenPartialHomeomorph.extend_source, Iff.mp, Filter.inter_mem_iff, ModelWithCorners.extendCoordChange, true_and
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)

Tactic:
e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex'

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.extend_preimage_mem_nhds, IsOpen.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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ (↑(e.extend I).symm : E → M) ⁻¹' e'.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)

Tactic:
exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex'

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.extend_preimage_mem_nhds, IsOpen.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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)

Tactic:
have hφx : φ.source ∈ 𝓝 (e.extend I x) := by
    simp_rw [φ, extendCoordChange, PartialEquiv.trans_source, PartialEquiv.symm_source,
      Filter.inter_mem_iff, mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source]
    exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex'
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' :
  Surjective (α := E) (β := E)
    (⇑(ContinuousLinearMap.restrictScalars ℝ (fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x))) :
      (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ (↑(e.extend I) : M → E) x ∈ φ.source

Tactic:
simp [φ, hex, hex']
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)

Tactic:
rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ),
    (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ)
      (uniqueDiffWithinAt_of_mem_nhds hφx), fderivWithin_of_mem_nhds <| hφx] at hφx'

Premises used: Real, uniqueDiffWithinAt_of_mem_nhds, ContDiffOn.differentiableOn, fderivWithin_of_mem_nhds, DifferentiableWithinAt.restrictScalars_fderivWithin, 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφx' : Surjective (α := E) (β := E) (⇑(fderivWithin 𝕜 (↑φ : E → E) φ.source ((↑(e.extend I) : M → E) x)) : (a : E) → E)
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
hφx'₁ : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
⊢ φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)

Tactic:
rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ),
    (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ)
      (uniqueDiffWithinAt_of_mem_nhds hφx), fderivWithin_of_mem_nhds <| hφx] at hφx'

Premises used: Real, uniqueDiffWithinAt_of_mem_nhds, ContDiffOn.differentiableOn, fderivWithin_of_mem_nhds, DifferentiableWithinAt.restrictScalars_fderivWithin, 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ (↑(e'.extend I) : M → E) x = (↑φ : E → E) ((↑(e.extend I) : M → E) x)

Tactic:
simp [φ, hex]
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
rw : (↑φ : E → E) ((↑(e.extend I) : M → E) x) ∈ interior (range (↑I : H → E))
⊢ (↑(e'.extend I) : M → E) x ∈ interior (range (↑I : H → E))

Tactic:
rw [show e'.extend I x = φ (e.extend I x) by simp [φ, hex]]
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
⊢ DifferentiableAt ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)

Tactic:
replace hφ := ((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt hφx
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
hφ : DifferentiableAt ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)
⊢ φ.target ⊆ range (↑I : H → E)

Tactic:
simp [φ, inter_assoc]

Premises used: Set.inter_assoc
-- 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
n_1 : WithTop ℕ∞
e_1 e'_1 : OpenPartialHomeomorph M_1 H_1
x_1 : M_1
𝕜 : Type u_1
inst_6 : NontriviallyNormedField 𝕜
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
H : Type u_3
inst_9 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
n : WithTop ℕ∞
inst_12 : 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
hx : (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_4, u_3} (𝕜 := 𝕜) (I := I) e e'
h : IsRCLikeNormedField 𝕜
x_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hφx' : Surjective (α := E) (β := E) (⇑(fderiv ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)) : (a : E) → E)
hφx : φ.source ∈ 𝓝 ((↑(e.extend I) : M → E) x)
hφ : DifferentiableAt ℝ (↑φ : E → E) ((↑(e.extend I) : M → E) x)
⊢ (↑φ : E → E) ((↑(e.extend I) : M → E) x) ∈ interior (range (↑I : H → E))

Tactic:
exact hφ.mem_interior_convex_of_surjective_fderiv hφx I.convex_range I.isClosed_range
    I.nonempty_interior (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hφx'

Premises used: Set.MapsTo.mono_right, ModelWithCorners.nonempty_interior, ModelWithCorners.convex_range, ModelWithCorners.isClosed_range, PartialEquiv.mapsTo, DifferentiableAt.mem_interior_convex_of_surjective_fderiv
-- 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
mp :
  (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target → (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target
mpr :
  (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target → (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target
⊢ (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target ↔ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target

Tactic:
constructor
-- 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
mp : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
mp₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
mp₂ : x ∈ e.source
mp₃ : x ∈ e'.source
⊢ (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target → (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target

Tactic:
apply mem_interior_range_of_mem_interior_range_of_mem_atlas hn

Premises used: ModelWithCorners.mem_interior_range_of_mem_interior_range_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 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
mpr : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
mpr₁ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
mpr₂ : x ∈ e'.source
mpr₃ : x ∈ e.source
⊢ (↑(e'.extend I) : M → E) x ∈ interior (e'.extend I).target → (↑(e.extend I) : M → E) x ∈ interior (e.extend I).target

Tactic:
apply mem_interior_range_of_mem_interior_range_of_mem_atlas hn

Premises used: ModelWithCorners.mem_interior_range_of_mem_interior_range_of_mem_atlas