-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
lemma interiorPoint_inl (x : M) (hx : I.IsInteriorPoint x) :
    I.IsInteriorPoint (.inl x: M ⊕ M')

Proof state:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑I (↑(chartAt H x) x) ∈ interior (I.target ∩ ↑I.symm ⁻¹' (chartAt H x).target)

Tactic:
simpa [I.isInteriorPoint_iff, extChartAt] using hx

Result:
no goals

Proof state:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑I (Function.extend Sum.inl (↑(chartAt H x)) (fun x_1 => Classical.arbitrary H) (Sum.inl x)) ∈
    interior (I.target ∩ ↑I.symm ⁻¹' (chartAt H x).target)

Tactic:
rw [Sum.inl_injective.extend_apply (chartAt H x)]

Result:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑I (↑(chartAt H x) x) ∈ interior (I.target ∩ ↑I.symm ⁻¹' (chartAt H x).target)

Proof state:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ I.IsInteriorPoint (Sum.inl x)

Tactic:
rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]

Result:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑(((chartAt H x).lift_openEmbedding ⋯).extend I) (Sum.inl x) ∈
    interior (((chartAt H x).lift_openEmbedding ⋯).extend I).target

Proof state:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑(((chartAt H x).lift_openEmbedding ⋯).extend I) (Sum.inl x) ∈
    interior (((chartAt H x).lift_openEmbedding ⋯).extend I).target

Tactic:
dsimp

Result:
𝕜 : 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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑I (Function.extend Sum.inl (↑(chartAt H x)) (fun x_1 => Classical.arbitrary H) (Sum.inl x)) ∈
    interior (I.target ∩ ↑I.symm ⁻¹' (chartAt H x).target)