[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c : β
x : α ⊕ β
⊢ swap (a • x) = a • swap x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c : β
val✝ : α
⊢ swap (a • inl val✝) = a • swap (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul N α
inst✝ : SMul N β
a : M
b : α
c val✝ : β
⊢ swap (a • inr val✝) = a • swap (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
⊢ (a • b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
val✝ : α
⊢ (a • b) • inl val✝ = a • b • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
val✝ : β
⊢ (a • b) • inr val✝ = a • b • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
x : α ⊕ β
⊢ a • b • x = b • a • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
val✝ : α
⊢ a • b • inl val✝ = b • a • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
val✝ : β
⊢ a • b • inr val✝ = b • a • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (smul_comm _ _ _), congr_arg inr (smul_comm _ _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x✝ : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
x : α ⊕ β
⊢ MulOpposite.op a • x = a • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
val✝ : α
⊢ MulOpposite.op a • inl val✝ = a • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
val✝ : β
⊢ MulOpposite.op a • inr val✝ = a • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
a : α
⊢ m₁✝ • a = m₂✝ • a
[PROOFSTEP]
injection h (inl a)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a : M
b✝ : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
b : β
⊢ m₁✝ • b = m₂✝ • b
[PROOFSTEP]
injection h (inr b)
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x : α ⊕ β
⊢ 1 • x = x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
val✝ : α
⊢ 1 • inl val✝ = inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
val✝ : β
⊢ 1 • inr val✝ = inr val✝
[PROOFSTEP]
exacts [congr_arg inl (one_smul _ _), congr_arg inr (one_smul _ _)]
[GOAL]
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
x : α ⊕ β
⊢ (a * b) • x = a • b • x
[PROOFSTEP]
cases x
[GOAL]
case inl
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
val✝ : α
⊢ (a * b) • inl val✝ = a • b • inl val✝
case inr
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
val✝ : β
⊢ (a * b) • inr val✝ = a • b • inr val✝
[PROOFSTEP]
exacts [congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)]
