Theorem: MulAction.smul_set_iInter₂ (Jordan/Mathlib/Set.lean)

State before:
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.20290
X : Type ?u.20293
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : (i : ι) → κ i → Set β
⊢ a • ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, a • s i j
Tactic:
simp_rw [smul_set_iInter]
State after:
no goals