case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (LocalEquiv.trans e f).source = (LocalEquiv.trans e' f').source

case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(LocalEquiv.trans e f)) (↑(LocalEquiv.trans e' f')) (LocalEquiv.trans e f).source
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ LocalEquiv.trans e f ≈ LocalEquiv.trans e' f'
constructor
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑(LocalEquiv.symm e) '' (e.target ∩ f.source) = ↑(LocalEquiv.symm e') '' (e.target ∩ f.source)
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (LocalEquiv.trans e f).source = (LocalEquiv.trans e' f').source
rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]
no goals
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑(LocalEquiv.symm e) '' (e.target ∩ f.source) = ↑(LocalEquiv.symm e') '' (e.target ∩ f.source)
exact (he.symm'.eqOn.mono <| inter_subset_left _ _).image_eq
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (LocalEquiv.trans e f).source
⊢ ↑(LocalEquiv.trans e f) x = ↑(LocalEquiv.trans e' f') x
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(LocalEquiv.trans e f)) (↑(LocalEquiv.trans e' f')) (LocalEquiv.trans e f).source
intro x hx
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ e.source ∩ ↑e ⁻¹' f.source
⊢ ↑(LocalEquiv.trans e f) x = ↑(LocalEquiv.trans e' f') x
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (LocalEquiv.trans e f).source
⊢ ↑(LocalEquiv.trans e f) x = ↑(LocalEquiv.trans e' f') x
rw [trans_source] at hx
no goals
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.56904
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ e.source ∩ ↑e ⁻¹' f.source
⊢ ↑(LocalEquiv.trans e f) x = ↑(LocalEquiv.trans e' f') x
simp [Function.comp_apply, LocalEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]