[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x✝ : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
x : Option α
⊢ (a • b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
⊢ (a • b) • none = a • b • none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
val✝ : α
⊢ (a • b) • some val✝ = a • b • some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (smul_assoc _ _ _)]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x✝ : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
x : Option α
⊢ MulOpposite.op a • x = a • x
[PROOFSTEP]
cases x
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
⊢ MulOpposite.op a • none = a • none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
val✝ : α
⊢ MulOpposite.op a • some val✝ = a • some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (op_smul_eq_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : SMul M α
inst✝¹ : SMul N α
a : M
b✝ : α
x : Option α
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : Option α), m₁✝ • a = m₂✝ • a
b : α
⊢ m₁✝ • b = m₂✝ • b
[PROOFSTEP]
injection h (some b)
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
b : Option α
⊢ 1 • b = b
[PROOFSTEP]
cases b
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
⊢ 1 • none = none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
val✝ : α
⊢ 1 • some val✝ = some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (one_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
b : Option α
⊢ (a₁ * a₂) • b = a₁ • a₂ • b
[PROOFSTEP]
cases b
[GOAL]
case none
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
⊢ (a₁ * a₂) • none = a₁ • a₂ • none
case some
M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
val✝ : α
⊢ (a₁ * a₂) • some val✝ = a₁ • a₂ • some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (mul_smul _ _ _)]
