simp only [Function.onFun, id_eq, disjoint_left] at hab ⊢
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : (fun a => a • ↑s) a ≠ (fun a => a • ↑s) b
⊢ (Disjoint on id) ((fun a => a • ↑s) a) ((fun a => a • ↑s) b)
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