α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (g ⁻¹' t)
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
⊢ Measurable g
intro t ht
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t)
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (g ⁻¹' t)
have : g ⁻¹' t = g ⁻¹' t ∩ { x | f x = g x }ᶜ ∪ g ⁻¹' t ∩ { x | f x = g x } := by
  simp [← inter_union_distrib_left]
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x})
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t)
rw [this]
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x})
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x})
refine (h.mono (inter_subset_right _ _)).measurableSet.union ?_
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x})
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x})
have : g ⁻¹' t ∩ { x : α | f x = g x } = f ⁻¹' t ∩ { x : α | f x = g x } := by
  ext x
  simp (config := { contextual := true })
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x | f x = g x})
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x})
rw [this]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x | f x = g x})
exact (hf ht).inter h.measurableSet.of_compl
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
⊢ g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
simp [← inter_union_distrib_left]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
x : α
⊢ x ∈ g ⁻¹' t ∩ {x | f x = g x} ↔ x ∈ f ⁻¹' t ∩ {x | f x = g x}
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
ext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.44496
δ : Type ?u.44499
δ' : Type ?u.44502
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : Set.Countable {x | f x ≠ g x}
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
x : α
⊢ x ∈ g ⁻¹' t ∩ {x | f x = g x} ↔ x ∈ f ⁻¹' t ∩ {x | f x = g x}
simp (config := { contextual := true })