F : Type ?u.897847
α : Type u_2
β : Type u_1
γ : Type ?u.897856
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ
F : Type ?u.897847
α : Type u_2
β : Type u_1
γ : Type ?u.897856
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ ↑(s • univ) = ↑univ
rw [← coe_subset] at hs
F : Type ?u.897847
α : Type u_2
β : Type u_1
γ : Type ?u.897856
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ 0
⊢ ↑s • Set.univ = Set.univ
F : Type ?u.897847
α : Type u_2
β : Type u_1
γ : Type ?u.897856
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ
push_cast at hs⊢
no goals
F : Type ?u.897847
α : Type u_2
β : Type u_1
γ : Type ?u.897856
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s✝ t : Finset β
a : α
b : β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ 0
⊢ ↑s • Set.univ = Set.univ
exact Set.smul_univ₀ hs