F : Type ?u.857977
α : Type u_2
β : Type u_1
γ : Type ?u.857986
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑s • Set.univ = Set.univ
F : Type ?u.857977
α : Type u_2
β : Type u_1
γ : Type ?u.857986
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑(s • univ) = ↑univ
push_cast
no goals
F : Type ?u.857977
α : Type u_2
β : Type u_1
γ : Type ?u.857986
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : Finset.Nonempty s
⊢ ↑s • Set.univ = Set.univ
exact Set.smul_univ hs