case h
α : Type u_1
β : Type ?u.150393
ι : Type ?u.150396
M : Type u_2
N : Type ?u.150402
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U V : Set α
h : indicator U 1 = indicator V 1
x✝ : α
⊢ x✝ ∈ U ↔ x✝ ∈ V
α : Type u_1
β : Type ?u.150393
ι : Type ?u.150396
M : Type u_2
N : Type ?u.150402
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U V : Set α
h : indicator U 1 = indicator V 1
⊢ U = V
ext
no goals
case h
α : Type u_1
β : Type ?u.150393
ι : Type ?u.150396
M : Type u_2
N : Type ?u.150402
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U V : Set α
h : indicator U 1 = indicator V 1
x✝ : α
⊢ x✝ ∈ U ↔ x✝ ∈ V
simp_rw [← indicator_eq_one_iff_mem M, h]