-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem measurableSet_eq_fun_of_countable {m : MeasurableSpace α} {E} [MeasurableSpace E]
    [MeasurableSingletonClass E] [Countable E] {f g : α → E} (hf : Measurable f)
    (hg : Measurable g) : MeasurableSet { x | f x = g x }

Proof state:
case refine_1
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
j : E
⊢ MeasurableSet {x | f x = j}

Tactic:
exact hf (measurableSet_singleton j)

Result:
no goals

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
⊢ MeasurableSet (⋃ j, {x | f x = j} ∩ {x | g x = j})

Tactic:
refine MeasurableSet.iUnion fun j => MeasurableSet.inter ?_ ?_

Result:
case refine_1
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
j : E
⊢ MeasurableSet {x | f x = j}

case refine_2
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
j : E
⊢ MeasurableSet {x | g x = j}

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet {x | f x = g x}

Tactic:
have : { x | f x = g x } = ⋃ j, { x | f x = j } ∩ { x | g x = j } := by
  ext1 x
  simp only [Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_eq_right']

Result:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
⊢ MeasurableSet {x | f x = g x}

Proof state:
case h
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
x : α
⊢ x ∈ {x | f x = g x} ↔ x ∈ ⋃ j, {x | f x = j} ∩ {x | g x = j}

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_eq_right']

Result:
no goals

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}

Tactic:
ext1 x

Result:
case h
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
x : α
⊢ x ∈ {x | f x = g x} ↔ x ∈ ⋃ j, {x | f x = j} ∩ {x | g x = j}

Proof state:
case refine_2
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
j : E
⊢ MeasurableSet {x | g x = j}

Tactic:
exact hg (measurableSet_singleton j)

Result:
no goals

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
⊢ MeasurableSet {x | f x = g x}

Tactic:
rw [this]

Result:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}
⊢ MeasurableSet (⋃ j, {x | f x = j} ∩ {x | g x = j})