[GOAL]
α : Type u
inst✝ : MulZeroClass α
x✝ : ULift α
⊢ ↑Equiv.ulift (0 * x✝) = ↑Equiv.ulift 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : MulZeroClass α
x✝ : ULift α
⊢ ↑Equiv.ulift (x✝ * 0) = ↑Equiv.ulift 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Distrib α
x✝² x✝¹ x✝ : ULift α
⊢ ↑Equiv.ulift (x✝² * (x✝¹ + x✝)) = ↑Equiv.ulift (x✝² * x✝¹ + x✝² * x✝)
[PROOFSTEP]
simp [left_distrib]
[GOAL]
α : Type u
inst✝ : Distrib α
x✝² x✝¹ x✝ : ULift α
⊢ ↑Equiv.ulift ((x✝² + x✝¹) * x✝) = ↑Equiv.ulift (x✝² * x✝ + x✝¹ * x✝)
[PROOFSTEP]
simp [right_distrib]
