-- 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
𝕜 : 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
⊢ I.IsInteriorPoint x

Tactic:
have hp : p ∈ Sum.inl '' (ModelWithCorners.interior (I := I) M) := by
  obtain (good | ⟨y, hy, hxy⟩) := hp
  exacts [good, (not_isLeft_and_isRight ⟨h, by rw [← hxy]; exact rfl⟩).elim]

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
hp : p ∈ Sum.inl '' ModelWithCorners.interior M
⊢ I.IsInteriorPoint x

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'
hp : p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
⊢ p ∈ ModelWithCorners.interior (M ⊕ 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 ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : p.isLeft = true
⊢ p ∈ ModelWithCorners.interior (M ⊕ 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 ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : ¬p.isLeft = true
⊢ p ∈ ModelWithCorners.interior (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'
p : M ⊕ M'
h : p.isLeft = true
x : M := p.getLeft h
x_eq : x = p.getLeft h
y : M'
hy : y ∈ ModelWithCorners.interior M'
hxy : Sum.inr y = p
⊢ (Sum.inr y).isRight = true

Tactic:
exact rfl

Result:
no goals

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
x : M := p.getLeft h
x_eq : x = p.getLeft h
⊢ p ∈ ModelWithCorners.interior (M ⊕ M')

Tactic:
rw [Sum.eq_left_getLeft_of_isLeft h]

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
⊢ Sum.inl (p.getLeft h) ∈ ModelWithCorners.interior (M ⊕ M')

Proof state:
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 ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : ¬p.isLeft = true
x : M' := p.getRight ⋯
x_eq : x = p.getRight ⋯
⊢ Sum.inr (p.getRight ⋯) ∈ ModelWithCorners.interior (M ⊕ M')

Tactic:
apply interiorPoint_inr x

Result:
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 ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : ¬p.isLeft = true
x : M' := p.getRight ⋯
x_eq : x = p.getRight ⋯
⊢ I.IsInteriorPoint x

Proof state:
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 ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : ¬p.isLeft = true
x : M' := p.getRight ⋯
x_eq : x = p.getRight ⋯
⊢ I.IsInteriorPoint x

Tactic:
have hp : p ∈ Sum.inr '' (ModelWithCorners.interior (I := I) M') := by
  obtain (⟨y, hy, hxy⟩ | good) := hp
  exacts [(not_isLeft_and_isRight ⟨by rw [← hxy]; exact rfl, Sum.not_isLeft.mp h⟩).elim, good]

Result:
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 ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
h : ¬p.isLeft = true
x : M' := p.getRight ⋯
x_eq : x = p.getRight ⋯
hp : p ∈ Sum.inr '' ModelWithCorners.interior M'
⊢ I.IsInteriorPoint x