Cancellable_Element_is_Cancellable_in_Subset

import Mathlib.Data.Set.Basic
import Mathlib.Algebra.Group.Defs

theorem Cancellable_Element_is_Cancellable_in_Subset {α : Type _} [Mul α] {S T : Set α} (hTS : T ⊆ S) {x : α} (hxT : x ∈ T) (hlc : ∀ a b : α, a ∈ S → b ∈ S → x * a = x * b → a = b) (hrc : ∀ a b : α, a ∈ S → b ∈ S → a * x = b * x → a = b) : (∀ a b : α, a ∈ T → b ∈ T → x * a = x * b → a = b) ∧ (∀ a b : α, a ∈ T → b ∈ T → a * x = b * x → a = b) := by sorry