-- Mathlib/MeasureTheory/Group/Arithmetic.lean
@[measurability]
lemma measurableSet_eq_fun' {β : Type*} [AddCommMonoid β] [PartialOrder β]
    [CanonicallyOrderedAdd β] [Sub β] [OrderedSub β]
    {_ : MeasurableSpace β} [MeasurableSub₂ β] [MeasurableSingletonClass β]
    {f g : α → β} (hf : Measurable f) (hg : Measurable g) :
    MeasurableSet {x | f x = g x}

Proof state:
case h
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝¹ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ f x✝ = g x✝ ↔ f x✝ ≤ g x✝ ∧ g x✝ ≤ f x✝

Tactic:
exact ⟨fun h ↦ ⟨h.le, h.symm.le⟩, fun h ↦ le_antisymm h.1 h.2⟩

Result:
no goals

Proof state:
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
this : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}
⊢ MeasurableSet {x | f x = g x}

Tactic:
rw [this]

Result:
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
this : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}
⊢ MeasurableSet ({a | (f - g) a = 0} ∩ {a | (g - f) a = 0})

Proof state:
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
this : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}
⊢ MeasurableSet ({a | (f - g) a = 0} ∩ {a | (g - f) a = 0})

Tactic:
exact ((hf.sub hg) (measurableSet_singleton 0)).inter ((hg.sub hf) (measurableSet_singleton 0))

Result:
no goals

Proof state:
case h
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝¹ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ x✝ ∈ {a | f a = g a} ↔ x✝ ∈ {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}

Tactic:
simp only [Set.mem_setOf_eq, Pi.sub_apply, tsub_eq_zero_iff_le, Set.mem_inter_iff]

Result:
case h
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝¹ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ f x✝ = g x✝ ↔ f x✝ ≤ g x✝ ∧ g x✝ ≤ f x✝

Proof state:
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
⊢ {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}

Tactic:
ext

Result:
case h
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝¹ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ x✝ ∈ {a | f a = g a} ↔ x✝ ∈ {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}

Proof state:
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet {x | f x = g x}

Tactic:
have : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0} := by
  ext
  simp only [Set.mem_setOf_eq, Pi.sub_apply, tsub_eq_zero_iff_le, Set.mem_inter_iff]
  exact ⟨fun h ↦ ⟨h.le, h.symm.le⟩, fun h ↦ le_antisymm h.1 h.2⟩

Result:
α : Type u_3
m : MeasurableSpace α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
f g : α → β
hf : Measurable f
hg : Measurable g
this : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0}
⊢ MeasurableSet {x | f x = g x}