[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulOneClass α
⊢ ∀ (x y : ULift α), ↑Equiv.ulift (x * y) = ↑Equiv.ulift x * ↑Equiv.ulift y
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulOneClass α
x✝ y✝ : ULift α
⊢ ↑Equiv.ulift (x✝ * y✝) = ↑Equiv.ulift x✝ * ↑Equiv.ulift y✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulZeroOneClass α
⊢ ∀ (a b : ULift α), ↑Equiv.ulift (a * b) = ↑Equiv.ulift a * ↑Equiv.ulift b
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type u_1
x y : ULift α
inst✝ : MulZeroOneClass α
a✝ b✝ : ULift α
⊢ ↑Equiv.ulift (a✝ * b✝) = ↑Equiv.ulift a✝ * ↑Equiv.ulift b✝
[PROOFSTEP]
rfl
