-- Mathlib/Geometry/Manifold/ChartedSpace.lean
lemma ChartedSpace.mem_atlas_sum [h : Nonempty H]
    {e : PartialHomeomorph (M ⊕ M') H} (he : e ∈ atlas H (M ⊕ M')) :
    (∃ f : PartialHomeomorph M H, f ∈ (atlas H M) ∧ e = (f.lift_openEmbedding IsOpenEmbedding.inl))
    ∨ (∃ f' : PartialHomeomorph M' H, f' ∈ (atlas H M') ∧
      e = (f'.lift_openEmbedding IsOpenEmbedding.inr))

Proof state:
case inl.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, (fun e => e.lift_openEmbedding ⋯) x = f.lift_openEmbedding ⋯) ∨
    ∃ f' ∈ atlas H M', (fun e => e.lift_openEmbedding ⋯) x = f'.lift_openEmbedding ⋯

Tactic:
left

Result:
case inl.intro.intro.h
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ ∃ f ∈ atlas H M, (fun e => e.lift_openEmbedding ⋯) x = f.lift_openEmbedding ⋯

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
he : e ∈ ChartedSpace.atlas
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he

Result:
case inl.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

case inr.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Proof state:
case inr.intro.intro.h
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ ∃ f' ∈ atlas H M', (fun e => e.lift_openEmbedding ⋯) x = f'.lift_openEmbedding ⋯

Tactic:
use x

Result:
no goals

Proof state:
case inr.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, (fun e => e.lift_openEmbedding ⋯) x = f.lift_openEmbedding ⋯) ∨
    ∃ f' ∈ atlas H M', (fun e => e.lift_openEmbedding ⋯) x = f'.lift_openEmbedding ⋯

Tactic:
right

Result:
case inr.intro.intro.h
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ ∃ f' ∈ atlas H M', (fun e => e.lift_openEmbedding ⋯) x = f'.lift_openEmbedding ⋯

Proof state:
case inl.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
rw [← hxe]

Result:
case inl.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, (fun e => e.lift_openEmbedding ⋯) x = f.lift_openEmbedding ⋯) ∨
    ∃ f' ∈ atlas H M', (fun e => e.lift_openEmbedding ⋯) x = f'.lift_openEmbedding ⋯

Proof state:
case inr.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
rw [← hxe]

Result:
case inr.intro.intro
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, (fun e => e.lift_openEmbedding ⋯) x = f.lift_openEmbedding ⋯) ∨
    ∃ f' ∈ atlas H M', (fun e => e.lift_openEmbedding ⋯) x = f'.lift_openEmbedding ⋯

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
simp only [atlas, sum, h, ↓reduceDIte] at he

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
he : e ∈ ChartedSpace.atlas
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Proof state:
case inl.intro.intro.h
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : PartialHomeomorph (M ⊕ M') H
x : PartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e => e.lift_openEmbedding ⋯) x = e
⊢ ∃ f ∈ atlas H M, (fun e => e.lift_openEmbedding ⋯) x = f.lift_openEmbedding ⋯

Tactic:
use x

Result:
no goals