case refine_1
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x

case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'
refine LocalEquiv.ext (fun x => ?_) (fun x => ?_) h.1
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source
case refine_1
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x
apply h.2
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source
rw [s]
no goals
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ
exact mem_univ _
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ (LocalEquiv.symm e).source
case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
apply h.symm'.2
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ (LocalEquiv.symm e).source
rw [symm_source, t]
no goals
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type ?u.59180
δ : Type ?u.59183
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ
exact mem_univ _