α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (↑e '' (e.source ∩ s))
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (e.target ∩ t)
rw [← h.image_eq]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (↑e '' (e.source ∩ s))
rintro y ⟨x, hx, rfl⟩
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
have hx' := hx
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
rw [hs] at hx'
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.30876
δ : Type ?u.30879
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]