α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.824632
δ' : Type ?u.824635
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ↑e)
this : Measurable (f ∘ ↑(trans (symm e) e).toEquiv)
⊢ Measurable f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.824632
δ' : Type ?u.824635
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ↑e)
⊢ Measurable f
have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.824632
δ' : Type ?u.824635
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ↑e)
this : Measurable (f ∘ ↑(trans (symm e) e).toEquiv)
⊢ Measurable f
rwa [coe_toEquiv, symm_trans_self] at this