no goals
F : Type ?u.142914
α : Type u_1
β : Type ?u.142920
γ : Type ?u.142923
inst✝¹ : Group α
inst✝ : MulAction α β
s✝ t✝ A B : Set β
a : α
x✝ : β
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
simp_rw [smul_inter_ne_empty_iff, div_eq_mul_inv]