rintro _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
case 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
⊢ ∀ ⦃a_1 : β⦄, a_1 ∈ a • ↑s → a_1 ∉ b • ↑s
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
⊢ False