case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.392411
δ : Type ?u.392414
δ' : Type ?u.392417
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
e₁ : α ≃ β
measurable_toFun✝¹ : Measurable ↑e₁
measurable_invFun✝¹ : Measurable ↑e₁.symm
measurable_toFun✝ : Measurable ↑e₁
measurable_invFun✝ : Measurable ↑e₁.symm
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun✝¹, measurable_invFun := measurable_invFun✝¹ } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun✝, measurable_invFun := measurable_invFun✝ }
α : Type u_1
β : Type u_2
γ : Type ?u.392411
δ : Type ?u.392414
δ' : Type ?u.392417
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
⊢ Injective toEquiv
rintro ⟨e₁, _, _⟩ ⟨e₂, _, _⟩ (rfl : e₁ = e₂)
no goals
case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.392411
δ : Type ?u.392414
δ' : Type ?u.392417
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
e₁ : α ≃ β
measurable_toFun✝¹ : Measurable ↑e₁
measurable_invFun✝¹ : Measurable ↑e₁.symm
measurable_toFun✝ : Measurable ↑e₁
measurable_invFun✝ : Measurable ↑e₁.symm
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun✝¹, measurable_invFun := measurable_invFun✝¹ } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun✝, measurable_invFun := measurable_invFun✝ }
rfl