-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
lemma interior_disjointUnion :
    ModelWithCorners.interior (I := I) (M ⊕ M') =
      Sum.inl '' (ModelWithCorners.interior (I := I) M)
      ∪ Sum.inr '' (ModelWithCorners.interior (I := I) M')

Proof state:
case pos.intro.intro
𝕜 : 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 : p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : p.isLeft = true
x : M := p.getLeft h
x_eq : x = p.getLeft h
x' : M
hx' : x' ∈ ModelWithCorners.interior M
hx'p : Sum.inl x' = p
⊢ I.IsInteriorPoint x

Tactic:
simpa [x_eq, ← hx'p, Sum.getLeft_inl]

Result:
no goals

Proof state:
case h.mp
𝕜 : 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 : p ∈ ModelWithCorners.interior (M ⊕ M')
⊢ p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'

Tactic:
by_cases h : Sum.isLeft p

Result:
case pos
𝕜 : 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 : p ∈ ModelWithCorners.interior (M ⊕ M')
h : p.isLeft = true
⊢ p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'

case neg
𝕜 : 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 : p ∈ ModelWithCorners.interior (M ⊕ M')
h : ¬p.isLeft = true
⊢ p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'

Proof state:
case h.mpr
𝕜 : 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'
⊢ p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M' →
    p ∈ ModelWithCorners.interior (M ⊕ M')

Tactic:
intro hp

Result:
case h.mpr
𝕜 : 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 : p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
⊢ p ∈ ModelWithCorners.interior (M ⊕ M')

Proof state:
case pos
𝕜 : 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 : p ∈ ModelWithCorners.interior (M ⊕ M')
h : p.isLeft = true
⊢ p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'

Tactic:
left

Result:
case pos.h
𝕜 : 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 : p ∈ ModelWithCorners.interior (M ⊕ M')
h : p.isLeft = true
⊢ p ∈ Sum.inl '' ModelWithCorners.interior M

Proof state:
case pos
𝕜 : 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 : p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : p.isLeft = true
⊢ p ∈ ModelWithCorners.interior (M ⊕ M')

Tactic:
set x := Sum.getLeft p h with x_eq

Result:
case pos
𝕜 : 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 : p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : p.isLeft = true
x : M := p.getLeft h
x_eq : x = p.getLeft h
⊢ p ∈ ModelWithCorners.interior (M ⊕ M')