[GOAL]
R : Type u
M : Type v
N : Type w
inst✝³ : SMul R M
inst✝² : SMul M N
inst✝¹ : SMul R N
inst✝ : IsScalarTower R M N
x : R
y : M
z : ULift N
⊢ { down := (x • y) • z.down } = { down := x • y • z.down }
[PROOFSTEP]
rw [smul_assoc]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0
[PROOFSTEP]
{ext; simp [smul_zero]
}
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ (c • 0).down = 0.down
[PROOFSTEP]
simp [smul_zero]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift M
⊢ c • (f + g) = c • f + c • g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift M
⊢ (c • (f + g)).down = (c • f + c • g).down
[PROOFSTEP]
simp [smul_add]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝² : R
x✝¹ x✝ : ULift M
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝² : R
x✝¹ x✝ : ULift M
⊢ (x✝² • (x✝¹ * x✝)).down = (x✝² • x✝¹ * x✝² • x✝).down
[PROOFSTEP]
simp [smul_mul']
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝ : R
⊢ x✝ • 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝ : R
⊢ (x✝ • 1).down = 1.down
[PROOFSTEP]
simp [smul_one]
