Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
this :
  ∀ {𝕜 : 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 ℕ∞} [IsManifold I n M]
    {e e' : OpenPartialHomeomorph M H} {x : M},
    n ≠ 0 →
      e ∈ atlas H M →
        e' ∈ atlas H M →
          x ∈ e.source →
            x ∈ e'.source →
              ↑(e.extend I) x ∈ interior (e.extend I).target →
                let φ := extendCoordChange e e';
                ContDiffOn 𝕜 n (↑φ) φ.source →
                  Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x)) →
                    IsRCLikeNormedField 𝕜 → ↑(e'.extend I) x ∈ interior (range ↑I)
h✝ : ¬IsRCLikeNormedField 𝕜
⊢ ↑(e'.extend I) x ∈ interior (range ↑I)

pp: 𝕜✝ : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝¹¹ : NormedAddCommGroup E✝
inst✝¹⁰ : NormedSpace 𝕜✝ E✝
H✝ : Type u_3
inst✝⁹ : TopologicalSpace H✝
I✝ : ModelWithCorners 𝕜✝ E✝ H✝
M✝ : Type u_4
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : ChartedSpace H✝ M✝
n✝ : WithTop ℕ∞
e✝ e'✝ : OpenPartialHomeomorph M✝ H✝
x✝ : M✝
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
h✝ : IsRCLikeNormedField 𝕜
⊢ ↑(e'.extend I) x ∈ interior (range ↑I)

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
this :
  ∀ {𝕜 : 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 ℕ∞} [IsManifold I n M]
    {e e' : OpenPartialHomeomorph M H} {x : M},
    n ≠ 0 →
      e ∈ atlas H M →
        e' ∈ atlas H M →
          x ∈ e.source →
            x ∈ e'.source →
              ↑(e.extend I) x ∈ interior (e.extend I).target →
                let φ := extendCoordChange e e';
                ContDiffOn 𝕜 n (↑φ) φ.source →
                  Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x)) →
                    IsRCLikeNormedField 𝕜 → ↑(e'.extend I) x ∈ interior (range ↑I)
h✝ : ¬IsRCLikeNormedField 𝕜
⊢ ↑(e'.extend I) x ∈ interior (range ↑I)