F : Type ?u.841640
α : Type u_2
β : Type u_1
γ : Type ?u.841649
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
F : Type ?u.841640
α : Type u_2
β : Type u_1
γ : Type ?u.841649
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t
simp_rw [← coe_subset]
F : Type ?u.841640
α : Type u_2
β : Type u_1
γ : Type ?u.841649
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t
F : Type ?u.841640
α : Type u_2
β : Type u_1
γ : Type ?u.841649
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
push_cast
no goals
F : Type ?u.841640
α : Type u_2
β : Type u_1
γ : Type ?u.841649
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
b : β
⊢ ↑s ⊆ a • ↑t ↔ a⁻¹ • ↑s ⊆ ↑t
exact Set.subset_set_smul_iff