case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e
cases e
no goals
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
rfl