[GOAL]
α : 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 : α ≃ₜ β
s : Set α
hs : IsOpen s
t : Set β
h : ↑e '' s = t
⊢ IsOpen (Equiv.toLocalEquivOfImageEq e.toEquiv s t h).target
[PROOFSTEP]
simpa [← h]
[GOAL]
α : 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 '' univ = univ
[PROOFSTEP]
rw [image_univ, e.surjective.range_eq]
[GOAL]
α : 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 : LocalHomeomorph α β
e' : LocalEquiv α β
h : e.toLocalEquiv = e'
⊢ replaceEquiv e e' h = e
[PROOFSTEP]
cases e
[GOAL]
case 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' 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✝ }
[PROOFSTEP]
subst e'
[GOAL]
case 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 β γ
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✝ }
[PROOFSTEP]
rfl
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
hx : x ∈ e.source
x' : α
hx' : ↑(LocalHomeomorph.symm e) (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' ∈ {x}
[PROOFSTEP]
rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']
[GOAL]
α : 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' →
    (∀ (x : α), ↑e x = ↑e' x) ∧
      (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e') x) ∧ e.source = e'.source
[PROOFSTEP]
rintro rfl
[GOAL]
α : 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 : LocalHomeomorph α β
⊢ (∀ (x : α), ↑e x = ↑e x) ∧
    (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e) x) ∧ e.source = e.source
[PROOFSTEP]
exact ⟨fun x => rfl, fun x => rfl, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ Tendsto (↑(LocalHomeomorph.symm e)) (𝓝 (↑e x)) (𝓝 x)
[PROOFSTEP]
simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ 𝓝 (↑(LocalHomeomorph.symm e) (↑e x)) = 𝓝 x
[PROOFSTEP]
rw [e.left_inv hx]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
hx : x ∈ e.source
s : Set β
⊢ map (↑e) (𝓝[↑e ⁻¹' s] x) = 𝓝[s] ↑e x
[PROOFSTEP]
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
  e.nhdsWithin_target_inter (e.map_source hx)]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : β → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝 (↑e x), p y) ↔ ∀ᶠ (b : β) in map (fun x => ↑e x) (𝓝 x), p b
[PROOFSTEP]
rw [e.map_nhds_eq hx]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : α → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝 (↑e x), p (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in 𝓝 x, p x
[PROOFSTEP]
rw [e.eventually_nhds _ hx]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : α → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (x : α) in 𝓝 x, p (↑(LocalHomeomorph.symm e) (↑e x))) ↔ ∀ᶠ (x : α) in 𝓝 x, p x
[PROOFSTEP]
refine' eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => _)
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : α → Prop
hx : x ∈ e.source
y : α
hy : ↑(LocalHomeomorph.symm e) (↑e y) = y
⊢ p (↑(LocalHomeomorph.symm e) (↑e y)) ↔ p y
[PROOFSTEP]
rw [hy]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p (↑e x)
[PROOFSTEP]
refine' Iff.trans _ eventually_map
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : β → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : β) in map (fun x => ↑e x) (𝓝[s] x), p b
[PROOFSTEP]
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (y : β) in 𝓝[↑(LocalHomeomorph.symm e) ⁻¹' s] ↑e x, p (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
[PROOFSTEP]
rw [e.eventually_nhdsWithin _ hx]
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
⊢ (∀ᶠ (x : α) in 𝓝[s] x, p (↑(LocalHomeomorph.symm e) (↑e x))) ↔ ∀ᶠ (x : α) in 𝓝[s] x, p x
[PROOFSTEP]
refine
  eventually_congr <| (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
[GOAL]
α : 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 : LocalHomeomorph α β
x : α
p : α → Prop
s : Set α
hx : x ∈ e.source
y : α
hy : ↑(LocalHomeomorph.symm e) (↑e y) = y
⊢ p (↑(LocalHomeomorph.symm e) (↑e y)) ↔ p y
[PROOFSTEP]
rw [hy]
[GOAL]
α : 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 : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑(LocalHomeomorph.symm e) ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
[PROOFSTEP]
rw [eventuallyEq_set, e.eventually_nhds _ hxe]
[GOAL]
α : 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 : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : α) in 𝓝 x,
    ↑e x ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
[PROOFSTEP]
filter_upwards [e.open_source.mem_nhds hxe, mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]
[GOAL]
case h
α : 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 : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ∀ (a : α),
    a ∈ e.source →
      (a ∈ s → a ∈ f ⁻¹' t) →
        (↑e a ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t))
[PROOFSTEP]
intro y hy hyu
[GOAL]
case h
α : 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 : LocalHomeomorph α β
s : Set α
t : Set γ
x : α
f : α → γ
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : α
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e y ∈ ↑(LocalHomeomorph.symm e) ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)
[PROOFSTEP]
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and_iff, iff_self_and, e.left_inv hy,
  iff_true_intro hyu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
⊢ IsImage e s t ↔ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s) = e.target ∩ t
[PROOFSTEP]
rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
h : IsImage e s t
hx : x ∈ e.source
⊢ map (↑e) (𝓝[s] x) = 𝓝[t] ↑e x
[PROOFSTEP]
rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x✝ : α
y : β
h : IsImage e s t
x : α
hx : x ∈ e.source
⊢ ↑e x ∈ closure t ↔ x ∈ closure s
[PROOFSTEP]
simp only [mem_closure_iff_nhdsWithin_neBot, ← h.map_nhdsWithin_eq hx, map_neBot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
h : IsImage e s t
⊢ IsImage e (interior s) (interior t)
[PROOFSTEP]
simpa only [closure_compl, compl_compl] using h.compl.closure.compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
⊢ IsOpen (↑e '' s)
[PROOFSTEP]
have : e '' s = e.target ∩ e.symm ⁻¹' s := e.toLocalEquiv.image_eq_target_inter_inv_preimage h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (↑e '' s)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
h : s ⊆ e.source
this : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s
⊢ IsOpen (e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s)
[PROOFSTEP]
exact e.continuousOn_symm.preimage_open_of_open e.open_target hs
[GOAL]
α : 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 : LocalEquiv α β
hc : ContinuousOn (↑e) e.source
ho : IsOpenMap (restrict e.source ↑e)
hs : IsOpen e.source
⊢ IsOpen e.target
[PROOFSTEP]
simpa only [range_restrict, e.image_source_eq_target] using ho.isOpen_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.restr e s).toLocalEquiv.source = e.source ∩ s
[PROOFSTEP]
rw [e.restr_source, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.restr e s).toLocalEquiv = LocalEquiv.restr e.toLocalEquiv s
[PROOFSTEP]
rw [e.restr_toLocalEquiv, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ LocalHomeomorph.restr e (e.source ∩ s) = LocalHomeomorph.restr e s
[PROOFSTEP]
refine' LocalHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ (LocalHomeomorph.restr e (e.source ∩ s)).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
[PROOFSTEP]
simp [e.open_source.interior_eq, ← inter_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ ofSet univ (_ : IsOpen univ) = LocalHomeomorph.refl α
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
x✝ : α
⊢ ↑(ofSet univ (_ : IsOpen univ)) x✝ = ↑(LocalHomeomorph.refl α) x✝
[PROOFSTEP]
simp
[GOAL]
case hinv
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
x✝ : α
⊢ ↑(LocalHomeomorph.symm (ofSet univ (_ : IsOpen univ))) x✝ = ↑(LocalHomeomorph.symm (LocalHomeomorph.refl α)) x✝
[PROOFSTEP]
simp
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
x✝ : α
⊢ x✝ ∈ (ofSet univ (_ : IsOpen univ)).toLocalEquiv.source ↔ x✝ ∈ (LocalHomeomorph.refl α).toLocalEquiv.source
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
⊢ (LocalHomeomorph.symm
          (LocalHomeomorph.restrOpen (LocalHomeomorph.symm e) e'.source (_ : IsOpen e'.source))).toLocalEquiv.target =
    (LocalHomeomorph.restrOpen e' e.target (_ : IsOpen e.target)).toLocalEquiv.source
[PROOFSTEP]
simp [inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set β
hs : IsOpen s
⊢ (LocalHomeomorph.trans e (ofSet s hs)).toLocalEquiv.source = (LocalHomeomorph.restr e (↑e ⁻¹' s)).toLocalEquiv.source
[PROOFSTEP]
rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set β
hs : IsOpen s
⊢ LocalHomeomorph.trans e (ofSet s hs) = LocalHomeomorph.restr e (e.source ∩ ↑e ⁻¹' s)
[PROOFSTEP]
rw [trans_ofSet, restr_source_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ (LocalHomeomorph.trans (ofSet s hs) e).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
[PROOFSTEP]
simp [hs.interior_eq, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
⊢ LocalHomeomorph.trans (ofSet s hs) e = LocalHomeomorph.restr e (e.source ∩ s)
[PROOFSTEP]
rw [ofSet_trans, restr_source_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.trans (ofSet s hs) (ofSet s' hs') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
[PROOFSTEP]
rw [(ofSet s hs).trans_ofSet hs']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
x✝ : α
⊢ ↑(LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s')) x✝ = ↑(ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))) x✝
[PROOFSTEP]
simp [hs'.interior_eq]
[GOAL]
case hinv
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
x✝ : α
⊢ ↑(LocalHomeomorph.symm (LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s'))) x✝ =
    ↑(LocalHomeomorph.symm (ofSet (s ∩ s') (_ : IsOpen (s ∩ s')))) x✝
[PROOFSTEP]
simp [hs'.interior_eq]
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
x✝ : α
⊢ x✝ ∈ (LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s')).toLocalEquiv.source ↔
    x✝ ∈ (ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))).toLocalEquiv.source
[PROOFSTEP]
simp [hs'.interior_eq]
[GOAL]
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ LocalHomeomorph.restr e e'.source ≈ LocalHomeomorph.restr e' e.source
[PROOFSTEP]
constructor
[GOAL]
case left
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = (LocalHomeomorph.restr e' e.source).toLocalEquiv.source
[PROOFSTEP]
rw [e'.restr_source' _ e.open_source]
[GOAL]
case left
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ (LocalHomeomorph.restr e e'.source).toLocalEquiv.source = e'.source ∩ e.source
[PROOFSTEP]
rw [e.restr_source' _ e'.open_source]
[GOAL]
case left
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source
[PROOFSTEP]
exact Set.inter_comm _ _
[GOAL]
case right
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source))
    (LocalHomeomorph.restr e e'.source).toLocalEquiv.source
[PROOFSTEP]
rw [e.restr_source' _ e'.open_source]
[GOAL]
case right
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑(LocalHomeomorph.restr e' e.source)) (e.source ∩ e'.source)
[PROOFSTEP]
refine' (EqOn.trans _ h).trans _
[GOAL]
case right.refine'_1
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑(LocalHomeomorph.restr e e'.source)) (↑e) (e.source ∩ e'.source)
[PROOFSTEP]
simp only [mfld_simps, eqOn_refl]
[GOAL]
case right.refine'_2
α : 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 α β
h : EqOn (↑e) (↑e') (e.source ∩ e'.source)
⊢ EqOn (↑e') (↑(LocalHomeomorph.restr e' e.source)) (e.source ∩ e'.source)
[PROOFSTEP]
simp only [mfld_simps, eqOn_refl]
[GOAL]
α : 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₂'
[PROOFSTEP]
obtain ⟨⟨x, y⟩, -⟩ := id h
[GOAL]
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₂'
[PROOFSTEP]
haveI : Nonempty α := ⟨x⟩
[GOAL]
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₂'
[PROOFSTEP]
haveI : Nonempty β := ⟨e₁ x⟩
[GOAL]
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₂'
[PROOFSTEP]
haveI : Nonempty γ := ⟨y⟩
[GOAL]
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₂'
[PROOFSTEP]
haveI : Nonempty δ := ⟨e₂ y⟩
[GOAL]
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₂'
[PROOFSTEP]
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]
[GOAL]
α : 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₂'
[PROOFSTEP]
rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ e₂']
[GOAL]
α : 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 α β
inst✝¹ : (x : α) → Decidable (x ∈ e.source)
inst✝ : (y : β) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ e.source ∩ frontier e.source = e'.source ∩ frontier e.source
[PROOFSTEP]
rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq]
[GOAL]
α : 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 α β
inst✝¹ : (x : α) → Decidable (x ∈ e.source)
inst✝ : (y : β) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e) (↑e') (e.source ∩ frontier e.source)
[PROOFSTEP]
rw [e.open_source.inter_frontier_eq]
[GOAL]
α : 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 α β
inst✝¹ : (x : α) → Decidable (x ∈ e.source)
inst✝ : (y : β) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn ↑e ↑e' ∅
[PROOFSTEP]
exact eqOn_empty _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
x : β
h : x ∈ e.target
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e, e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·),
  e.right_inv h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
x : β
h : x ∈ e.target
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h, preimage_univ,
  continuousWithinAt_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)
[PROOFSTEP]
simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ (∀ (x : β), x ∈ s → ContinuousWithinAt f s x) ↔
    ∀ (x : β), x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
refine' forall₂_congr fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
rw [e.continuousWithinAt_iff_continuousWithinAt_comp_right (h hx), e.symm_image_eq_source_inter_preimage h, inter_comm,
  continuousWithinAt_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑(LocalHomeomorph.symm e) x)
[PROOFSTEP]
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x
[PROOFSTEP]
refine' ⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) s x
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
rw [← continuousWithinAt_inter' h] at fe_cont ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
[PROOFSTEP]
have : ContinuousWithinAt (e.symm ∘ e ∘ f) (s ∩ f ⁻¹' e.source) x :=
  haveI : ContinuousWithinAt e.symm univ (e (f x)) := (e.continuousAt_symm (e.map_source hx)).continuousWithinAt
  ContinuousWithinAt.comp this fe_cont (subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
[PROOFSTEP]
exact this.congr (fun y hy => by simp [e.left_inv hy.2]) (by simp [e.left_inv hx])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
y : γ
hy : y ∈ s ∩ f ⁻¹' e.source
⊢ f y = (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) y
[PROOFSTEP]
simp [e.left_inv hy.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
s : Set γ
x : γ
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ f x = (↑(LocalHomeomorph.symm e) ∘ ↑e ∘ f) x
[PROOFSTEP]
simp [e.left_inv hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
[PROOFSTEP]
have hx : f x ∈ e.source := (mem_of_mem_nhds h : _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
[PROOFSTEP]
have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x
[PROOFSTEP]
rwa [nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
x : γ
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
[PROOFSTEP]
rw [← continuousWithinAt_univ, ← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ Continuous f ↔ Continuous (↑e ∘ f)
[PROOFSTEP]
simp only [continuous_iff_continuousOn_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ
[PROOFSTEP]
exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source
[PROOFSTEP]
lift x to e.source using hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ 𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source
[PROOFSTEP]
rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
  e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (↑(toHomeomorphSourceTarget e)) (comap Subtype.val (𝓝 ↑(↑(toHomeomorphSourceTarget e) x)))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))
[PROOFSTEP]
simp only [(· ∘ ·), toHomeomorphSourceTarget_apply_coe, comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : α
⊢ x ∈ e.source
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : α
⊢ x ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : β
⊢ x ∈ e.target
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
x : β
⊢ x ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
⊢ Continuous
    { toFun := ↑e, invFun := ↑(LocalHomeomorph.symm e),
        left_inv := (_ : ∀ (x : α), ↑(LocalHomeomorph.symm e) (↑e x) = x),
        right_inv := (_ : ∀ (x : β), ↑e (↑(LocalHomeomorph.symm e) x) = x) }.toFun
[PROOFSTEP]
simpa only [continuous_iff_continuousOn_univ, h] using e.continuousOn
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
h' : e.target = univ
⊢ Continuous
    { toFun := ↑e, invFun := ↑(LocalHomeomorph.symm e),
        left_inv := (_ : ∀ (x : α), ↑(LocalHomeomorph.symm e) (↑e x) = x),
        right_inv := (_ : ∀ (x : β), ↑e (↑(LocalHomeomorph.symm e) x) = x) }.invFun
[PROOFSTEP]
simpa only [continuous_iff_continuousOn_univ, h'] using e.continuousOn_symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ OpenEmbedding ↑e
[PROOFSTEP]
apply openEmbedding_of_continuous_injective_open
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Continuous ↑e
[PROOFSTEP]
apply continuous_iff_continuousOn_univ.mpr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) univ
[PROOFSTEP]
rw [← h]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) e.source
[PROOFSTEP]
exact e.continuousOn
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Injective ↑e
[PROOFSTEP]
apply Set.injective_iff_injOn_univ.mpr
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) univ
[PROOFSTEP]
rw [← h]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) e.source
[PROOFSTEP]
exact e.injOn
[GOAL]
case h₃
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ IsOpenMap ↑e
[PROOFSTEP]
intro U hU
[GOAL]
case h₃
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
U : Set α
hU : IsOpen U
⊢ IsOpen (↑e '' U)
[PROOFSTEP]
simpa only [h, subset_univ, mfld_simps] using e.image_open_of_open hU
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ (localHomeomorphSubtypeCoe s).toLocalEquiv.target = ↑s
[PROOFSTEP]
simp only [localHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ {x | x ∈ s.carrier} = ↑s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ (subtypeRestr e s).toLocalEquiv.source = Subtype.val ⁻¹' e.source
[PROOFSTEP]
simp only [subtypeRestr_def, mfld_simps]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
x : { x // x ∈ s }
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ (subtypeRestr e s).toLocalEquiv.target
[PROOFSTEP]
refine' ⟨e.map_source hxe, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
x : { x // x ∈ s }
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target
[PROOFSTEP]
rw [s.localHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
x : { x // x ∈ s }
hxe : ↑x ∈ e.source
⊢ ↑x ∈ ↑s
[PROOFSTEP]
exact x.prop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
⊢ LocalHomeomorph.trans (LocalHomeomorph.symm (subtypeRestr f s)) (subtypeRestr f' s) ≈
    LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f')
      (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
[PROOFSTEP]
simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (LocalHomeomorph.trans (Opens.localHomeomorphSubtypeCoe s) f') ≈
    LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f')
      (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
[PROOFSTEP]
have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.preimage_open_of_open_symm s.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (LocalHomeomorph.trans (Opens.localHomeomorphSubtypeCoe s) f') ≈
    LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f')
      (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
[PROOFSTEP]
rw [← ofSet_trans _ openness₁, ← trans_assoc, ← trans_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans
        (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
        (Opens.localHomeomorphSubtypeCoe s))
      f' ≈
    LocalHomeomorph.trans
      (LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f))
      f'
[PROOFSTEP]
refine'
  EqOnSource.trans' _
    (eqOnSource_refl _)
      -- f' has been eliminated !!!
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (Opens.localHomeomorphSubtypeCoe s) ≈
    LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f)
[PROOFSTEP]
have sets_identity : f.symm.source ∩ (f.target ∩ f.symm ⁻¹' s) = f.symm.source ∩ f.symm ⁻¹' s := by mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
⊢ (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
[PROOFSTEP]
mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (Opens.localHomeomorphSubtypeCoe s) ≈
    LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f)
[PROOFSTEP]
have openness₂ : IsOpen (s : Set α) := s.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ LocalHomeomorph.trans
      (LocalHomeomorph.trans (LocalHomeomorph.symm f) (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)))
      (Opens.localHomeomorphSubtypeCoe s) ≈
    LocalHomeomorph.trans (ofSet (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) openness₁) (LocalHomeomorph.symm f)
[PROOFSTEP]
rw [ofSet_trans', sets_identity, ← trans_of_set' _ openness₂, trans_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ LocalHomeomorph.trans (LocalHomeomorph.symm f)
      (LocalHomeomorph.trans (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s))
        (Opens.localHomeomorphSubtypeCoe s)) ≈
    LocalHomeomorph.trans (LocalHomeomorph.symm f) (ofSet (↑s) openness₂)
[PROOFSTEP]
refine'
  EqOnSource.trans' (eqOnSource_refl _)
    _
      -- f has been eliminated !!!
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ LocalHomeomorph.trans (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe s)) (Opens.localHomeomorphSubtypeCoe s) ≈
    ofSet (↑s) openness₂
[PROOFSTEP]
refine' Setoid.trans (trans_symm_self s.localHomeomorphSubtypeCoe) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
f f' : LocalHomeomorph α β
openness₁ : IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)
sets_identity :
  (LocalHomeomorph.symm f).toLocalEquiv.source ∩ (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s) =
    (LocalHomeomorph.symm f).toLocalEquiv.source ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ ofSet (Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target
      (_ : IsOpen (Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target) ≈
    ofSet (↑s) openness₂
[PROOFSTEP]
simp only [mfld_simps, Setoid.refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
⊢ EqOn (↑(LocalHomeomorph.symm (subtypeRestr e V))) (inclusion hUV ∘ ↑(LocalHomeomorph.symm (subtypeRestr e U)))
    (subtypeRestr e U).toLocalEquiv.target
[PROOFSTEP]
set i := Set.inclusion hUV
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
⊢ EqOn (↑(LocalHomeomorph.symm (subtypeRestr e V))) (i ∘ ↑(LocalHomeomorph.symm (subtypeRestr e U)))
    (subtypeRestr e U).toLocalEquiv.target
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ (subtypeRestr e U).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (subtypeRestr e V)) y = (i ∘ ↑(LocalHomeomorph.symm (subtypeRestr e U))) y
[PROOFSTEP]
dsimp [LocalHomeomorph.subtypeRestr_def] at hy ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) =
    inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y))
[PROOFSTEP]
have hyV : e.symm y ∈ V.localHomeomorphSubtypeCoe.target :=
  by
  rw [Opens.localHomeomorphSubtypeCoe_target] at hy ⊢
  exact hUV hy.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
[PROOFSTEP]
rw [Opens.localHomeomorphSubtypeCoe_target] at hy ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' ↑U
⊢ ↑(LocalHomeomorph.symm e) y ∈ ↑V
[PROOFSTEP]
exact hUV hy.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) =
    inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y))
[PROOFSTEP]
refine' V.localHomeomorphSubtypeCoe.injOn _ trivial _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) ∈
    (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.source
[PROOFSTEP]
rw [← LocalHomeomorph.symm_target]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y) ∈
    (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)).toLocalEquiv.target
[PROOFSTEP]
apply LocalHomeomorph.map_source
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y ∈ (LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)).toLocalEquiv.source
[PROOFSTEP]
rw [LocalHomeomorph.symm_source]
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
[PROOFSTEP]
exact hyV
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(Opens.localHomeomorphSubtypeCoe V)
      (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe V)) (↑(LocalHomeomorph.symm e) y)) =
    ↑(Opens.localHomeomorphSubtypeCoe V)
      (inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y)))
[PROOFSTEP]
rw [V.localHomeomorphSubtypeCoe.right_inv hyV]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y =
    ↑(Opens.localHomeomorphSubtypeCoe V)
      (inclusion hUV (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y)))
[PROOFSTEP]
show _ = U.localHomeomorphSubtypeCoe _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝² : Nonempty { x // x ∈ s }
U V : Opens α
inst✝¹ : Nonempty { x // x ∈ U }
inst✝ : Nonempty { x // x ∈ V }
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : β
hy : y ∈ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (Opens.localHomeomorphSubtypeCoe U).toLocalEquiv.target
hyV : ↑(LocalHomeomorph.symm e) y ∈ (Opens.localHomeomorphSubtypeCoe V).toLocalEquiv.target
⊢ ↑(LocalHomeomorph.symm e) y =
    ↑(Opens.localHomeomorphSubtypeCoe U)
      (↑(LocalHomeomorph.symm (Opens.localHomeomorphSubtypeCoe U)) (↑(LocalHomeomorph.symm e) y))
[PROOFSTEP]
rw [U.localHomeomorphSubtypeCoe.right_inv hy.2]


[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine LinearEquiv.ofLinear (R := R) (R₂ := R) ?toFun ?invFun ?left ?right
[GOAL]
case toFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine lift ?_
[GOAL]
case toFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ (⨁ (i₁ : ι₁), M₁ i₁) →ₗ[R] (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine DirectSum.toModule R _ _ fun i₁ => ?_
[GOAL]
case toFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
⊢ M₁ i₁ →ₗ[R] (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine @LinearMap.flip R _ R _ R _ R _ _ _ _ _ _ _ _ _ _ _ _ _ _ ?_
[GOAL]
case toFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
⊢ (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine DirectSum.toModule R _ _ fun i₂ => LinearMap.flip <| ?_
[GOAL]
case toFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
i₂ : ι₂
⊢ M₁ i₁ →ₗ[R] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
refine curry ?_
[GOAL]
case toFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
i₂ : ι₂
⊢ M₁ i₁ ⊗[R] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd
[PROOFSTEP]
exact DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)
[GOAL]
case invFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ (⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
[PROOFSTEP]
refine DirectSum.toModule R _ _ fun i => ?_
[GOAL]
case invFun
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁ × ι₂
⊢ M₁ i.fst ⊗[R] M₂ i.snd →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
[PROOFSTEP]
exact map (DirectSum.lof R _ M₁ i.1) (DirectSum.lof R _ M₂ i.2)
[GOAL]
case left
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ comp
      (lift
        (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
          LinearMap.flip
            (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
              LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
      (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
        map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)) =
    LinearMap.id
[PROOFSTEP]
refine DirectSum.linearMap_ext R fun ⟨i₁, i₂⟩ => ?_
[GOAL]
case left
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x✝ : ι₁ × ι₂
i₁ : ι₁
i₂ : ι₂
⊢ comp
      (comp
        (lift
          (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
            LinearMap.flip
              (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
        (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
          map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)))
      (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)) =
    comp LinearMap.id (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))
[PROOFSTEP]
refine TensorProduct.ext ?_
[GOAL]
case left
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x✝ : ι₁ × ι₂
i₁ : ι₁
i₂ : ι₂
⊢ compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
      (comp
        (comp
          (lift
            (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
              LinearMap.flip
                (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                  LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
          (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
            map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)))
        (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))) =
    compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
      (comp LinearMap.id (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)))
[PROOFSTEP]
refine
  LinearMap.ext₂ fun m₁ m₂ =>
    ?_
      -- porting note: seems much nicer than the `repeat` lean 3 proof.
[GOAL]
case left
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x✝ : ι₁ × ι₂
i₁ : ι₁
i₂ : ι₂
m₁ : M₁ (i₁, i₂).fst
m₂ : M₂ (i₁, i₂).snd
⊢ ↑(↑(compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
              (comp
                (comp
                  (lift
                    (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                      LinearMap.flip
                        (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                          LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))
                  (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                    map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd)))
                (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))
          m₁)
      m₂ =
    ↑(↑(compr₂ (mk R (M₁ (i₁, i₂).fst) (M₂ (i₁, i₂).snd))
              (comp LinearMap.id (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))
          m₁)
      m₂
[PROOFSTEP]
simp only [compr₂_apply, comp_apply, id_apply, mk_apply, DirectSum.toModule_lof, map_tmul, lift.tmul, flip_apply,
  curry_apply]
[GOAL]
case right
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ comp
      (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
        map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
      (lift
        (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
          LinearMap.flip
            (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
              LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)))))) =
    LinearMap.id
[PROOFSTEP]
refine TensorProduct.ext ?_
[GOAL]
case right
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
⊢ compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
      (comp
        (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
          map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
        (lift
          (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
            LinearMap.flip
              (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))) =
    compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id
[PROOFSTEP]
refine @DirectSum.linearMap_ext R _ _ _ _ _ _ _ _ (_) _ _ fun i₁ => ?_
[GOAL]
case right
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
⊢ comp
      (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
        (comp
          (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
            map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
          (lift
            (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
              LinearMap.flip
                (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                  LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
      (lof R ι₁ (fun i => M₁ i) i₁) =
    comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁)
[PROOFSTEP]
refine @LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ fun x₁ => ?_
[GOAL]
case right
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
x₁ : M₁ i₁
⊢ ↑(comp
          (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
            (comp
              (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
              (lift
                (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                  LinearMap.flip
                    (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                      LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
          (lof R ι₁ (fun i => M₁ i) i₁))
      x₁ =
    ↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁)) x₁
[PROOFSTEP]
refine @DirectSum.linearMap_ext R _ _ _ _ _ _ _ _ (_) _ _ fun i₂ => ?_
[GOAL]
case right
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
x₁ : M₁ i₁
i₂ : ι₂
⊢ comp
      (↑(comp
            (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
              (comp
                (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                  map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
                (lift
                  (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                    LinearMap.flip
                      (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                        LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
            (lof R ι₁ (fun i => M₁ i) i₁))
        x₁)
      (lof R ι₂ (fun i => M₂ i) i₂) =
    comp
      (↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁)) x₁)
      (lof R ι₂ (fun i => M₂ i) i₂)
[PROOFSTEP]
refine
  LinearMap.ext fun x₂ =>
    ?_
      -- porting note: seems much nicer than the `repeat` lean 3 proof.
[GOAL]
case right
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
x₁ : M₁ i₁
i₂ : ι₂
x₂ : M₂ i₂
⊢ ↑(comp
          (↑(comp
                (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂))
                  (comp
                    (toModule R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i =>
                      map (lof R ι₁ M₁ i.fst) (lof R ι₂ M₂ i.snd))
                    (lift
                      (toModule R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₁ =>
                        LinearMap.flip
                          (toModule R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗[R] M₂ i.snd) fun i₂ =>
                            LinearMap.flip (curry (lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂))))))))
                (lof R ι₁ (fun i => M₁ i) i₁))
            x₁)
          (lof R ι₂ (fun i => M₂ i) i₂))
      x₂ =
    ↑(comp
          (↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) (⨁ (i₂ : ι₂), M₂ i₂)) LinearMap.id) (lof R ι₁ (fun i => M₁ i) i₁))
            x₁)
          (lof R ι₂ (fun i => M₂ i) i₂))
      x₂
[PROOFSTEP]
simp only [compr₂_apply, comp_apply, id_apply, mk_apply, DirectSum.toModule_lof, map_tmul, lift.tmul, flip_apply,
  curry_apply]
  /- was:

      refine'
        LinearEquiv.ofLinear
          (lift <|
            DirectSum.toModule R _ _ fun i₁ => LinearMap.flip <| DirectSum.toModule R _ _ fun i₂ =>
                  LinearMap.flip <| curry <|
                    DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))
          (DirectSum.toModule R _ _ fun i => map (DirectSum.lof R _ _ _) (DirectSum.lof R _ _ _)) _
          _ <;>
      [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5]
    repeat'
      first
        |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof]
        |rw [map_tmul]|rw [lift.tmul]|rw [flip_apply]|rw [curry_apply]
    -/

  /- alternative with explicit types:
    refine'
        LinearEquiv.ofLinear
          (lift <|
            DirectSum.toModule
              (R := R) (M := M₁) (N := (⨁ i₂, M₂ i₂) →ₗ[R] ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2)
              (φ := fun i₁ => LinearMap.flip <|
                DirectSum.toModule (R := R) (M := M₂) (N := ⨁ i : ι₁ × ι₂, M₁ i.1 ⊗[R] M₂ i.2)
                (φ := fun i₂ => LinearMap.flip <| curry <|
                    DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))))
          (DirectSum.toModule
            (R := R)
            (M := fun i : ι₁ × ι₂ => M₁ i.1 ⊗[R] M₂ i.2)
            (N := (⨁ i₁, M₁ i₁) ⊗[R] ⨁ i₂, M₂ i₂)
            (φ := fun i : ι₁ × ι₂ => map (DirectSum.lof R _ M₁ i.1) (DirectSum.lof R _ M₂ i.2))) _
          _ <;>
      [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5]
    repeat'
      first
        |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof]
        |rw [map_tmul]|rw [lift.tmul]|rw [flip_apply]|rw [curry_apply]
  -/
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
m₁ : M₁ i
m₂ : M₂'
⊢ ↑(↑(compr₂ (mk R (M₁ i) M₂')
              (comp
                (comp
                  (lift
                    (toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
                      compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)))
                  (toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i)))
                (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)))
          m₁)
      m₂ =
    ↑(↑(compr₂ (mk R (M₁ i) M₂') (comp LinearMap.id (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i))) m₁) m₂
[PROOFSTEP]
dsimp only [comp_apply, compr₂_apply, id_apply, mk_apply]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
m₁ : M₁ i
m₂ : M₂'
⊢ ↑(lift
          (toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
            compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)))
      (↑(toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i))
        (↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (m₁ ⊗ₜ[R] m₂))) =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (m₁ ⊗ₜ[R] m₂)
[PROOFSTEP]
simp_rw [DirectSum.toModule_lof, rTensor_tmul, lift.tmul, DirectSum.toModule_lof, compr₂_apply, mk_apply]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
m₁ : M₁ i
m₂ : M₂'
⊢ ↑(↑(comp
              (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) M₂')
                (comp (toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i))
                  (lift
                    (toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
                      compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)))))
              (lof R ι₁ (fun i => M₁ i) i))
          m₁)
      m₂ =
    ↑(↑(comp (compr₂ (mk R (⨁ (i₁ : ι₁), M₁ i₁) M₂') LinearMap.id) (lof R ι₁ (fun i => M₁ i) i)) m₁) m₂
[PROOFSTEP]
dsimp only [comp_apply, compr₂_apply, id_apply, mk_apply]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
m₁ : M₁ i
m₂ : M₂'
⊢ ↑(toModule R ι₁ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') fun i => rTensor M₂' (lof R ι₁ M₁ i))
      (↑(lift
            (toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
              compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)))
        (↑(lof R ι₁ (fun i => M₁ i) i) m₁ ⊗ₜ[R] m₂)) =
    ↑(lof R ι₁ (fun i => M₁ i) i) m₁ ⊗ₜ[R] m₂
[PROOFSTEP]
simp_rw [lift.tmul, DirectSum.toModule_lof, compr₂_apply, mk_apply, DirectSum.toModule_lof, rTensor_tmul]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ ↑(TensorProduct.directSum R M₁ M₂) (↑(lof R ι₁ M₁ i₁) m₁ ⊗ₜ[R] ↑(lof R ι₂ M₂ i₂) m₂) =
    ↑(lof R (ι₁ × ι₂) (fun i => M₁ i.fst ⊗[R] M₂ i.snd) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
[PROOFSTEP]
simp [TensorProduct.directSum]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ ↑(directSumLeft R M₁ M₂') (↑(lof R ι₁ M₁ i) x ⊗ₜ[R] y) = ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
[PROOFSTEP]
dsimp only [directSumLeft, LinearEquiv.ofLinear_apply, lift.tmul]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ ↑(↑(toModule R ι₁ (M₂' →ₗ[R] ⨁ (i : ι₁), M₁ i ⊗[R] M₂') fun i =>
              compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i))
          (↑(lof R ι₁ M₁ i) x))
      y =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [DirectSum.toModule_lof R i]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ ↑(↑(compr₂ (mk R (M₁ i) M₂') (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i)) x) y =
    ↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ ↑(LinearEquiv.symm (directSumLeft R M₁ M₂')) (↑(lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) =
    ↑(lof R ι₁ M₁ i) x ⊗ₜ[R] y
[PROOFSTEP]
rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(directSumRight R M₁' M₂) (x ⊗ₜ[R] ↑(lof R ι₂ M₂ i) y) = ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
[PROOFSTEP]
dsimp only [directSumRight, LinearEquiv.trans_apply, TensorProduct.comm_tmul]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      (↑(directSumLeft R M₂ M₁') (↑(lof R ι₂ M₂ i) y ⊗ₜ[R] x)) =
    ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [directSumLeft_tmul_lof]
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁')
      (↑(lof R ι₂ (fun i => M₂ i ⊗[R] M₁') i) (y ⊗ₜ[R] x)) =
    ↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
[PROOFSTEP]
exact DFinsupp.mapRange_single (hf := fun _ => rfl)
[GOAL]
R : Type u
inst✝¹⁰ : CommRing R
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁹ : DecidableEq ι₁
inst✝⁸ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝⁷ : (i₁ : ι₁) → AddCommGroup (M₁ i₁)
inst✝⁶ : AddCommGroup M₁'
inst✝⁵ : (i₂ : ι₂) → AddCommGroup (M₂ i₂)
inst✝⁴ : AddCommGroup M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₁'
inst✝¹ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝ : Module R M₂'
x : M₁'
i : ι₂
y : M₂ i
⊢ ↑(LinearEquiv.symm (directSumRight R M₁' M₂)) (↑(lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)) =
    x ⊗ₜ[R] ↑(lof R ι₂ M₂ i) y
[PROOFSTEP]
rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]