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

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