M : Type ?u.9269
N : Type ?u.9272
G : Type ?u.9275
A : Type ?u.9278
B : Type ?u.9281
α : Type ?u.9284
β : Type ?u.9287
γ : Type ?u.9290
δ : Type ?u.9293
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Sort ?u.9343
M : Type ?u.9269
N : Type ?u.9272
G : Type ?u.9275
A : Type ?u.9278
B : Type ?u.9281
α : Type ?u.9284
β : Type ?u.9287
γ : Type ?u.9290
δ : Type ?u.9293
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
⊢ Sort ?u.9343
haveI := comp α g
M : Type ?u.9269
N : Type ?u.9272
G : Type ?u.9275
A : Type ?u.9278
B : Type ?u.9281
α : Type ?u.9284
β : Type ?u.9287
γ : Type ?u.9290
δ : Type ?u.9293
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.9343
M : Type ?u.9269
N : Type ?u.9272
G : Type ?u.9275
A : Type ?u.9278
B : Type ?u.9281
α : Type ?u.9284
β : Type ?u.9287
γ : Type ?u.9290
δ : Type ?u.9293
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this : SMul N α
⊢ Sort ?u.9343
haveI := comp β g
no goals
M : Type ?u.9269
N : Type ?u.9272
G : Type ?u.9275
A : Type ?u.9278
B : Type ?u.9281
α : Type ?u.9284
β : Type ?u.9287
γ : Type ?u.9290
δ : Type ?u.9293
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.9343
exact IsScalarTower N α β