case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.56162
δ : Type ?u.56165
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑(LocalEquiv.symm e')) (↑e) e'.target
α : Type u_1
β : Type u_2
γ : Type ?u.56162
δ : Type ?u.56165
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ LocalEquiv.symm e ≈ LocalEquiv.symm e'
refine' ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn _ _⟩ <;>
  simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.56162
δ : Type ?u.56165
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑(LocalEquiv.symm e')) (↑e) e'.target
exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)