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

State before:
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Tactic:
obtain _ | _ := isEmpty_or_nonempty ι
State after:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i

case inr
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : Nonempty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i

State before:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Tactic:
refine' Eq.trans _ (Set.iInter_of_empty _).symm
State after:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = Set.univ

State before:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • ⋂ i, s i = Set.univ
Tactic:
rw [Set.iInter_of_empty]
State after:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • Set.univ = Set.univ

State before:
case inl
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : IsEmpty ι
⊢ a • Set.univ = Set.univ
Tactic:
exact Set.smul_set_univ
State after:
no goals

State before:
case inr
α✝ : Type u_1
α : Type u_3
β : Type u_2
G : Type ?u.17549
X : Type ?u.17552
ι : Sort u_4
κ : ι → Sort ?u.17560
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
s : ι → Set β
h✝ : Nonempty ι
⊢ a • ⋂ i, s i = ⋂ i, a • s i
Tactic:
exact (MulAction.injective _).image_iInter_eq _
State after:
no goals