F : Type ?u.901234
α : Type u_2
β : Type u_1
γ : Type ?u.901243
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ
F : Type ?u.901234
α : Type u_2
β : Type u_1
γ : Type ?u.901243
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ ↑(a • univ) = ↑univ
push_cast
no goals
F : Type ?u.901234
α : Type u_2
β : Type u_1
γ : Type ?u.901243
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s t : Finset β
a : α
b : β
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ
exact Set.smul_set_univ₀ ha