-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
lemma isInteriorPoint_disjointUnion_left {p : M ⊕ M'} (hp : I.IsInteriorPoint p)
    (hleft : Sum.isLeft p) : I.IsInteriorPoint (Sum.getLeft p hleft)

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : ¬I.IsInteriorPoint x
⊢ False

Tactic:
rw [isInteriorPoint_iff_not_isBoundaryPoint x, not_not] at h

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
⊢ False

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
⊢ False

Tactic:
rw [isInteriorPoint_iff_not_isBoundaryPoint p] at hp

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
⊢ False

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
⊢ IsBoundaryPoint ?m.61839 x

Tactic:
tauto

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
⊢ I.IsInteriorPoint (p.getLeft hleft)

Tactic:
by_contra h

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
h : ¬I.IsInteriorPoint (p.getLeft hleft)
⊢ False

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
this : I.IsBoundaryPoint p
⊢ False

Tactic:
exact hp this

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
this : I.IsBoundaryPoint (Sum.inl x)
⊢ False

Tactic:
rw [← Sum.eq_left_getLeft_of_isLeft hleft] at this

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
this : I.IsBoundaryPoint p
⊢ False

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
h : ¬I.IsInteriorPoint (p.getLeft hleft)
⊢ False

Tactic:
set x := Sum.getLeft p hleft

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'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : ¬I.IsInteriorPoint x
⊢ False

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
⊢ False

Tactic:
have := boundaryPoint_inl (M' := M') x (by tauto)

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'
p : M ⊕ M'
hp : ¬I.IsBoundaryPoint p
hleft : p.isLeft = true
x : M := p.getLeft hleft
h : I.IsBoundaryPoint x
this : I.IsBoundaryPoint (Sum.inl x)
⊢ False