no goals
α : Type u_1
β : Type u_2
γ : Type ?u.20183
δ : Type ?u.20186
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : x = ↑(LocalEquiv.symm e) y
⊢ ↑e x = y
rw [← e.right_inv hy, h]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.20183
δ : Type ?u.20186
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : ↑e x = y
⊢ x = ↑(LocalEquiv.symm e) y
rw [← e.left_inv hx, h]