no goals
α : Type u_2
β : Type ?u.24420
ι : Type ?u.24423
M : Type u_1
N : Type ?u.24429
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}
classical
  rw [mulIndicator_one', preimage_one]
  split_ifs <;> simp
α : Type u_2
β : Type ?u.24420
ι : Type ?u.24423
M : Type u_1
N : Type ?u.24429
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ (if 1 ∈ s then univ else ∅) ∈ {univ, ∅}
α : Type u_2
β : Type ?u.24420
ι : Type ?u.24423
M : Type u_1
N : Type ?u.24429
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}
rw [mulIndicator_one', preimage_one]
no goals
α : Type u_2
β : Type ?u.24420
ι : Type ?u.24423
M : Type u_1
N : Type ?u.24429
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ (if 1 ∈ s then univ else ∅) ∈ {univ, ∅}
split_ifs <;> simp