case mk
α : Type u_1
β : Type u_2
γ : Type ?u.22794
δ : Type ?u.22797
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e' toLocalEquiv✝ : LocalEquiv α β
open_source✝ : IsOpen toLocalEquiv✝.source
open_target✝ : IsOpen toLocalEquiv✝.target
continuous_toFun✝ : ContinuousOn (↑toLocalEquiv✝) toLocalEquiv✝.source
continuous_invFun✝ : ContinuousOn toLocalEquiv✝.invFun toLocalEquiv✝.target
h :
  { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv =
    e'
⊢ replaceEquiv
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
      e' h =
    { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
α : Type u_1
β : Type u_2
γ : Type ?u.22794
δ : Type ?u.22797
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e : LocalHomeomorph α β
e' : LocalEquiv α β
h : e.toLocalEquiv = e'
⊢ replaceEquiv e e' h = e
cases e
case mk
α : Type u_1
β : Type u_2
γ : Type ?u.22794
δ : Type ?u.22797
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
toLocalEquiv✝ : LocalEquiv α β
open_source✝ : IsOpen toLocalEquiv✝.source
open_target✝ : IsOpen toLocalEquiv✝.target
continuous_toFun✝ : ContinuousOn (↑toLocalEquiv✝) toLocalEquiv✝.source
continuous_invFun✝ : ContinuousOn toLocalEquiv✝.invFun toLocalEquiv✝.target
⊢ replaceEquiv
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv
      (_ :
        { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
              continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv =
          { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
              continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv) =
    { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
case mk
α : Type u_1
β : Type u_2
γ : Type ?u.22794
δ : Type ?u.22797
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e'✝ : LocalHomeomorph β γ
e' toLocalEquiv✝ : LocalEquiv α β
open_source✝ : IsOpen toLocalEquiv✝.source
open_target✝ : IsOpen toLocalEquiv✝.target
continuous_toFun✝ : ContinuousOn (↑toLocalEquiv✝) toLocalEquiv✝.source
continuous_invFun✝ : ContinuousOn toLocalEquiv✝.invFun toLocalEquiv✝.target
h :
  { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv =
    e'
⊢ replaceEquiv
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
      e' h =
    { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
subst e'
no goals
case mk
α : Type u_1
β : Type u_2
γ : Type ?u.22794
δ : Type ?u.22797
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
toLocalEquiv✝ : LocalEquiv α β
open_source✝ : IsOpen toLocalEquiv✝.source
open_target✝ : IsOpen toLocalEquiv✝.target
continuous_toFun✝ : ContinuousOn (↑toLocalEquiv✝) toLocalEquiv✝.source
continuous_invFun✝ : ContinuousOn toLocalEquiv✝.invFun toLocalEquiv✝.target
⊢ replaceEquiv
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
      { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv
      (_ :
        { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
              continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv =
          { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
              continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toLocalEquiv) =
    { toLocalEquiv := toLocalEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
rfl