rw [← smul_coe hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe hc, smul_coe hd]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s
no goals