α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
⊢ LocalEquiv.trans e (LocalEquiv.symm e) ≈ ofSet e.source
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ LocalEquiv.trans e (LocalEquiv.symm e) ≈ ofSet e.source
have A : (e.trans e.symm).source = e.source := by mfld_set_tac
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
x : α
hx : x ∈ (LocalEquiv.trans e (LocalEquiv.symm e)).source
⊢ ↑(LocalEquiv.trans e (LocalEquiv.symm e)) x = ↑(ofSet e.source) x
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
⊢ LocalEquiv.trans e (LocalEquiv.symm e) ≈ ofSet e.source
refine' ⟨by rw [A, ofSet_source], fun x hx => _⟩
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(LocalEquiv.trans e (LocalEquiv.symm e)) x = ↑(ofSet e.source) x
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
x : α
hx : x ∈ (LocalEquiv.trans e (LocalEquiv.symm e)).source
⊢ ↑(LocalEquiv.trans e (LocalEquiv.symm e)) x = ↑(ofSet e.source) x
rw [A] at hx
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(LocalEquiv.trans e (LocalEquiv.symm e)) x = ↑(ofSet e.source) x
simp only [hx, mfld_simps]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
mfld_set_tac
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.58218
δ : Type ?u.58221
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
⊢ (LocalEquiv.trans e (LocalEquiv.symm e)).source = (ofSet e.source).source
rw [A, ofSet_source]