no goals
α : Type u_1
β : Type ?u.29472
ι : Type ?u.29475
M : Type u_2
N : Type ?u.29481
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ (mulIndicator U fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}
classical
  rw [mulIndicator_const_preimage_eq_union]
  split_ifs <;> simp
α : Type u_1
β : Type ?u.29472
ι : Type ?u.29475
M : Type u_2
N : Type ?u.29481
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅) ∈ {univ, U, Uᶜ, ∅}
α : Type u_1
β : Type ?u.29472
ι : Type ?u.29475
M : Type u_2
N : Type ?u.29481
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ (mulIndicator U fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}
rw [mulIndicator_const_preimage_eq_union]
no goals
α : Type u_1
β : Type ?u.29472
ι : Type ?u.29475
M : Type u_2
N : Type ?u.29481
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅) ∈ {univ, U, Uᶜ, ∅}
split_ifs <;> simp