-- 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 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

Tactic:
obtain ⟨x', hx', hx'p⟩ := hp

Result:
case neg.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.getRight ⋯
x_eq : x = p.getRight ⋯
x' : M'
hx' : x' ∈ ModelWithCorners.interior M'
hx'p : Sum.inr x' = p
⊢ I.IsInteriorPoint x

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

Tactic:
intro hp

Result:
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'

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'
⊢ ModelWithCorners.interior (M ⊕ M') = Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'

Tactic:
ext p

Result:
case 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'
⊢ p ∈ ModelWithCorners.interior (M ⊕ M') ↔
    p ∈ Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior 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.getRight ⋯
x_eq : x = p.getRight ⋯
y : M
hy : y ∈ ModelWithCorners.interior M
hxy : Sum.inl y = p
⊢ (Sum.inl y).isLeft = true

Tactic:
exact rfl

Result:
no goals

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

Tactic:
replace h := Sum.not_isLeft.mp h

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

Proof state:
case neg.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.isRight = true
⊢ p ∈ Sum.inr '' ModelWithCorners.interior M'

Tactic:
exact ⟨Sum.getRight p h, isInteriorPoint_disjointUnion_right hp h, Sum.inr_getRight p h⟩

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'
h : ¬p.isLeft = true
x : M' := p.getRight ⋯
x_eq : x = p.getRight ⋯
y : M
hy : y ∈ ModelWithCorners.interior M
hxy : Sum.inl y = p
⊢ p.isLeft = true

Tactic:
rw [← hxy]

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'
h : ¬p.isLeft = true
x : M' := p.getRight ⋯
x_eq : x = p.getRight ⋯
y : M
hy : y ∈ ModelWithCorners.interior M
hxy : Sum.inl y = p
⊢ (Sum.inl y).isLeft = true

Proof state:
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

Tactic:
exact ⟨Sum.getLeft p h, isInteriorPoint_disjointUnion_left hp h, Sum.inl_getLeft p h⟩

Result:
no goals