case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
obtain ⟨⟨x, y⟩, -⟩ := id h
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this : Nonempty α
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
haveI : Nonempty α := ⟨x⟩
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝ : Nonempty α
this : Nonempty β
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this : Nonempty α
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
haveI : Nonempty β := ⟨e₁ x⟩
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝¹ : Nonempty α
this✝ : Nonempty β
this : Nonempty γ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝ : Nonempty α
this : Nonempty β
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
haveI : Nonempty γ := ⟨y⟩
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝² : Nonempty α
this✝¹ : Nonempty β
this✝ : Nonempty γ
this : Nonempty δ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝¹ : Nonempty α
this✝ : Nonempty β
this : Nonempty γ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
haveI : Nonempty δ := ⟨e₂ y⟩
no goals
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e₁ e₁' : LocalHomeomorph α β
e₂ e₂' : LocalHomeomorph γ δ
h : Set.Nonempty (prod e₁ e₂).toLocalEquiv.source
x : α
y : γ
this✝² : Nonempty α
this✝¹ : Nonempty β
this✝ : Nonempty γ
this : Nonempty δ
⊢ prod e₁ e₂ = prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'
simp_rw [LocalHomeomorph.ext_iff, prod_apply, prod_symm_apply, prod_source, Prod.ext_iff,
  Set.prod_eq_prod_iff_of_nonempty h, forall_and, Prod.forall, forall_const,
  and_assoc, and_left_comm]