case refine'_1
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (n : N) (a : α), 1 • n • a = n • 1 • a

case refine'_2
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ SMulCommClass M N α
refine' ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x _ _⟩
case refine'_1
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ 1 • y • z = y • 1 • z
case refine'_1
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (n : N) (a : α), 1 • n • a = n • 1 • a
intro y z
no goals
case refine'_1
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ 1 • y • z = y • 1 • z
rw [one_smul, one_smul]
case refine'_2
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ ∀ (x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
case refine'_2
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
clear x
case refine'_2
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
⊢ (x * x') • y • z = y • (x * x') • z
case refine'_2
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
⊢ ∀ (x : M),
    x ∈ s → ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
intro x hx x' hx' y z
no goals
case refine'_2
M : Type u_3
A : Type ?u.240612
B : Type ?u.240615
N : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ (x : M), x ∈ s → ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (n : N) (a : α), x' • n • a = n • x' • a
y : N
z : α
⊢ (x * x') • y • z = y • (x * x') • z
rw [mul_smul, mul_smul, hx', hs x hx]