[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m✝ m₁ m₂ : MeasurableSpace α
m' : MeasurableSpace β
f✝¹ : α → β
g : β → α
f✝ : α → β
m : MeasurableSpace α
f : ℕ → Set β
hf : ∀ (i : ℕ), (fun s => MeasurableSet (f✝ ⁻¹' s)) (f i)
⊢ (fun s => MeasurableSet (f✝ ⁻¹' s)) (⋃ (i : ℕ), f i)
[PROOFSTEP]
simpa only [preimage_iUnion] using m.measurableSet_iUnion _ hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m✝ m₁ m₂ : MeasurableSpace α
m' : MeasurableSpace β
f✝ : α → β
g : β → α
f : α → β
m : MeasurableSpace β
s : ℕ → Set α
hs : ∀ (i : ℕ), (fun s => ∃ s', MeasurableSet s' ∧ f ⁻¹' s' = s) (s i)
s' : ℕ → Set β
hs' : ∀ (x : ℕ), MeasurableSet (s' x) ∧ f ⁻¹' s' x = s x
⊢ f ⁻¹' ⋃ (i : ℕ), s' i = ⋃ (i : ℕ), s i
[PROOFSTEP]
simp [hs']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
⊢ Measurable f
[PROOFSTEP]
nontriviality β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
⊢ Measurable f
[PROOFSTEP]
inhabit β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable f
[PROOFSTEP]
convert @measurable_const α β _ _ (f default) using 2
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f✝ g : α → β
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → α
hf : ∀ (x y : β), f x = f y
✝ : Nontrivial β
inhabited_h : Inhabited β
x✝ : β
⊢ f x✝ = f default
[PROOFSTEP]
apply hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ Measurable (piecewise s f g)
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (piecewise s f g ⁻¹' t)
[PROOFSTEP]
rw [piecewise_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (Set.ite s (f ⁻¹' t) (g ⁻¹' t))
[PROOFSTEP]
exact hs.ite (hf ht) (hg ht)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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)
[PROOFSTEP]
have : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x} := by simp [← inter_union_distrib_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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}
[PROOFSTEP]
simp [← inter_union_distrib_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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})
[PROOFSTEP]
refine (h.mono (inter_subset_right _ _)).measurableSet.union ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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})
[PROOFSTEP]
have : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x} :=
  by
  ext x
  simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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}
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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})
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : 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})
[PROOFSTEP]
exact (hf ht).inter h.measurableSet.of_compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)
[PROOFSTEP]
rw [← biUnion_preimage_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet (⋃ (y : α) (_ : y ∈ s), f ⁻¹' {y})
[PROOFSTEP]
refine' MeasurableSet.iUnion fun y => MeasurableSet.iUnion fun hy => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
⊢ MeasurableSet (f ⁻¹' {y})
[PROOFSTEP]
by_cases hyf : y ∈ range f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∈ range f
⊢ MeasurableSet (f ⁻¹' {y})
[PROOFSTEP]
rcases hyf with ⟨y, rfl⟩
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : β
hy : f y ∈ s
⊢ MeasurableSet (f ⁻¹' {f y})
[PROOFSTEP]
apply h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : ¬y ∈ range f
⊢ MeasurableSet (f ⁻¹' {y})
[PROOFSTEP]
simp only [preimage_singleton_eq_empty.2 hyf, MeasurableSet.empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ Measurable f
[PROOFSTEP]
apply measurable_to_countable'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
[PROOFSTEP]
rintro (- | -)
[GOAL]
case h.false
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {false})
[PROOFSTEP]
convert h.compl
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
[PROOFSTEP]
rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
[GOAL]
case h.true
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
⊢ Measurable fun x => Nat.findGreatest (p x) N
[PROOFSTEP]
refine' measurable_findGreatest' fun k hk => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet {x | Nat.findGreatest (p x) N = k}
[PROOFSTEP]
simp only [Nat.findGreatest_eq_iff, setOf_and, setOf_forall, ← compl_setOf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet ({a | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x | p x k}) ∩ ⋂ (i : ℕ) (_ : k < i) (_ : i ≤ N), {a | p a i}ᶜ))
[PROOFSTEP]
repeat'
  apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN] <;> try intros
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ MeasurableSet ({a | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x | p x k}) ∩ ⋂ (i : ℕ) (_ : k < i) (_ : i ≤ N), {a | p a i}ᶜ))
[PROOFSTEP]
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN]
[GOAL]
case h₂.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ k ≠ 0 → MeasurableSet {x | p x k}
[PROOFSTEP]
try intros
[GOAL]
case h₂.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ k ≠ 0 → MeasurableSet {x | p x k}
[PROOFSTEP]
intros
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : k < b) (_ : b ≤ N), {a | p a b}ᶜ)
[PROOFSTEP]
try intros
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : k < b) (_ : b ≤ N), {a | p a b}ᶜ)
[PROOFSTEP]
intros
[GOAL]
case h₂.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : k ≠ 0
⊢ MeasurableSet {x | p x k}
[PROOFSTEP]
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN]
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ MeasurableSet (⋂ (_ : k < b✝) (_ : b✝ ≤ N), {a | p a b✝}ᶜ)
[PROOFSTEP]
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN]
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ k < b✝ → MeasurableSet (⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)
[PROOFSTEP]
try intros
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ k < b✝ → MeasurableSet (⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)
[PROOFSTEP]
intros
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ MeasurableSet (⋂ (_ : b✝¹ ≤ N), {a | p a b✝¹}ᶜ)
[PROOFSTEP]
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN]
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ
[PROOFSTEP]
try intros
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ
[PROOFSTEP]
intros
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ (k : ℕ), k ≤ N → MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝² : ℕ
b✝¹ : k < b✝²
b✝ : b✝² ≤ N
⊢ MeasurableSet {a | p a b✝²}ᶜ
[PROOFSTEP]
apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter, MeasurableSet.compl, hN]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
⊢ Measurable fun x => Nat.find (_ : ∃ N, p x N)
[PROOFSTEP]
refine' measurable_to_nat fun x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet ((fun x => Nat.find (_ : ∃ N, p x N)) ⁻¹' {Nat.find (_ : ∃ N, p x N)})
[PROOFSTEP]
rw [preimage_find_eq_disjointed (fun k => {x | p x k})]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet (disjointed (fun k => {x | p x k}) (Nat.find (_ : ∃ N, p x N)))
[PROOFSTEP]
exact MeasurableSet.disjointed hm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
p : α → Prop
inst✝ : MeasurableSingletonClass α
x : Subtype p
⊢ val ⁻¹' {↑x} = {x}
[PROOFSTEP]
rw [← image_singleton, preimage_image_eq _ Subtype.val_injective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set ↑s
hs : MeasurableSet s
⊢ MeasurableSet t → MeasurableSet (Subtype.val '' t)
[PROOFSTEP]
rintro ⟨u, hu, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' (Subtype.val ⁻¹' u))
[PROOFSTEP]
rw [Subtype.image_preimage_coe]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (u ∩ s)
[PROOFSTEP]
exact hu.inter hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
p : β → Prop
f : α → β
hf : Measurable f
h : ∀ (x : α), p (f x)
t : Set (Subtype p)
x✝ : MeasurableSet t
s : Set β
hs : MeasurableSet s ∧ Subtype.val ⁻¹' s = t
⊢ MeasurableSet ((fun x => { val := f x, property := (_ : p (f x)) }) ⁻¹' (Subtype.val ⁻¹' s))
[PROOFSTEP]
simp only [← preimage_comp, (· ∘ ·), Subtype.coe_mk, hf hs.1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
u : Set ↑s
hs : MeasurableSet (Subtype.val ⁻¹' s)
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' u)
[PROOFSTEP]
rcases hu with ⟨u, hu, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' (Subtype.val ⁻¹' u))
[PROOFSTEP]
convert (measurable_subtype_coe hu).inter hs
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion h '' (Subtype.val ⁻¹' u) = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.e'_3.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ inclusion h '' (Subtype.val ⁻¹' u) ↔
    { val := x, property := hx } ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
[PROOFSTEP]
simpa [@and_comm _ (_ = x)] using and_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ MeasurableSet (f ⁻¹' u)
[PROOFSTEP]
convert (hs.subtype_image (hc hu)).union (ht.subtype_image (hd hu))
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ f ⁻¹' u = Subtype.val '' ((fun a => f ↑a) ⁻¹' u) ∪ Subtype.val '' ((fun a => f ↑a) ⁻¹' u)
[PROOFSTEP]
change f ⁻¹' u = (↑) '' ((↑) ⁻¹' (f ⁻¹' u) : Set s) ∪ (↑) '' ((↑) ⁻¹' (f ⁻¹' u) : Set t)
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : Measurable fun a => f ↑a
hd : Measurable fun a => f ↑a
u : Set β
hu : MeasurableSet u
⊢ f ⁻¹' u = Subtype.val '' (Subtype.val ⁻¹' (f ⁻¹' u)) ∪ Subtype.val '' (Subtype.val ⁻¹' (f ⁻¹' u))
[PROOFSTEP]
rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, Subtype.range_coe, Subtype.range_coe, ←
  inter_distrib_left, univ_subset_iff.1 h, inter_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : Measurable f
g : ↑sᶜ → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable (restrict s fun x => if hx : x ∈ s then f { val := x, property := hx } else g { val := x, property := hx })
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : Measurable f
g : ↑sᶜ → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable
    (restrict sᶜ fun x => if hx : x ∈ s then f { val := x, property := hx } else g { val := x, property := hx })
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ MeasurableSpace.comap Prod.fst mβ ≤ MeasurableSpace.map f m
[PROOFSTEP]
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ mβ ≤ MeasurableSpace.map (Prod.fst ∘ f) m
[PROOFSTEP]
exact hf₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ MeasurableSpace.comap Prod.snd mγ ≤ MeasurableSpace.map f m
[PROOFSTEP]
rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
hf₁ : Measurable fun a => (f a).fst
hf₂ : Measurable fun a => (f a).snd
⊢ mγ ≤ MeasurableSpace.map (Prod.snd ∘ f) m
[PROOFSTEP]
exact hf₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
[PROOFSTEP]
rcases h with ⟨⟨x, y⟩, hx, hy⟩
[GOAL]
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
[PROOFSTEP]
refine' ⟨fun hst => _, fun h => h.1.prod h.2⟩
[GOAL]
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
[PROOFSTEP]
have : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t) := measurable_prod_mk_right hst
[GOAL]
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
[PROOFSTEP]
have : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t) := measurable_prod_mk_left hst
[GOAL]
case intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
x : α
y : β
hx : (x, y).fst ∈ s
hy : (x, y).snd ∈ t
hst : MeasurableSet (s ×ˢ t)
this✝ : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
cases' (s ×ˢ t).eq_empty_or_nonempty with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp [h, prod_eq_empty_iff.mp h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set α
t : Set β
h : Set.Nonempty (s ×ˢ t)
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)
[PROOFSTEP]
have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ ({ y } : Set β) :=
  by
  ext1 ⟨x, y⟩
  simp [and_assoc, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
[PROOFSTEP]
ext1 ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
[PROOFSTEP]
simp [and_assoc, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
⊢ MeasurableSet (f ⁻¹' s)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y}
⊢ MeasurableSet (⋃ (y : β), ((fun x => f (x, y)) ⁻¹' s) ×ˢ {y})
[PROOFSTEP]
exact .iUnion fun y => (hf y hs).prod (.singleton y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)
[PROOFSTEP]
rw [preimage_iUnionLift]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
f : (i : ι) → ↑(t i) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (inclusion hT ⁻¹' ⋃ (i : ι), inclusion (_ : t i ⊆ ⋃ (i : ι), t i) '' (f i ⁻¹' s))
[PROOFSTEP]
exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
htU : ⋃ (i : ι), t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (liftCover t f hf htU ⁻¹' s)
[PROOFSTEP]
rw [preimage_liftCover]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
htU : ⋃ (i : ι), t i = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⋃ (i : ι), Subtype.val '' (f i ⁻¹' s))
[PROOFSTEP]
exact .iUnion fun i => .subtype_image (htm i) <| hfm i hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
inhabit ι
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
set g' : (i : ι) → t i → β := fun i =>
  g i ∘
    (↑)
      -- see #2184
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
have ht' : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
[GOAL]
case ht'
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
⊢ ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
[PROOFSTEP]
intro i j x hxi hxj
[GOAL]
case ht'
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
i j : ι
x : α
hxi : x ∈ t i
hxj : x ∈ t j
⊢ g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
[PROOFSTEP]
rcases eq_or_ne i j with rfl | hij
[GOAL]
case ht'.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
i : ι
x : α
hxi hxj : x ∈ t i
⊢ g' i { val := x, property := hxi } = g' i { val := x, property := hxj }
[PROOFSTEP]
rfl
[GOAL]
case ht'.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
i j : ι
x : α
hxi : x ∈ t i
hxj : x ∈ t j
hij : i ≠ j
⊢ g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
[PROOFSTEP]
exact ht hij ⟨hxi, hxj⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
set f : (⋃ i, t i) → β := iUnionLift t g' ht' _ Subset.rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
f : ↑(⋃ (i : ι), t i) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) (_ : ⋃ (i : ι), t i ⊆ ⋃ (i : ι), t i)
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
have hfm : Measurable f := measurable_iUnionLift _ _ t_meas (fun i => (hg i).comp measurable_subtype_coe)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
f : ↑(⋃ (i : ι), t i) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) (_ : ⋃ (i : ι), t i ⊆ ⋃ (i : ι), t i)
hfm : Measurable f
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
classical
refine
  ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
    hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
f : ↑(⋃ (i : ι), t i) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) (_ : ⋃ (i : ι), t i ⊆ ⋃ (i : ι), t i)
hfm : Measurable f
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
[PROOFSTEP]
refine
  ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
    hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
f : ↑(⋃ (i : ι), t i) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) (_ : ⋃ (i : ι), t i ⊆ ⋃ (i : ι), t i)
hfm : Measurable f
i : ι
x : α
hx : x ∈ t i
⊢ (fun x => if hx : x ∈ ⋃ (i : ι), t i then f { val := x, property := hx } else g default x) x = g i x
[PROOFSTEP]
simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort uι
s t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j => EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i => g i ∘ Subtype.val
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    g' i { val := x, property := hxi } = g' j { val := x, property := hxj }
f : ↑(⋃ (i : ι), t i) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) (_ : ⋃ (i : ι), t i ⊆ ⋃ (i : ι), t i)
hfm : Measurable f
i : ι
x : α
hx : x ∈ t i
⊢ iUnionLift t (fun i => g i ∘ Subtype.val) ht' (⋃ (i : ι), t i) (_ : ⋃ (i : ι), t i ⊆ ⋃ (i : ι), t i)
      { val := x, property := (_ : x ∈ ⋃ (i : ι), t i) } =
    g i x
[PROOFSTEP]
exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
m✝ : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
m : MeasurableSpace α
t : ℕ → Set β
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_disj : Pairwise (Disjoint on t)
g : ℕ → β → α
hg : ∀ (n : ℕ), Measurable (g n)
i j : ℕ
h : (Disjoint on t) i j
⊢ EqOn (g i) (g j) (t i ∩ t j)
[PROOFSTEP]
simp only [h.inter_eq, eqOn_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
g : α → (a : δ) → π a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a
[PROOFSTEP]
simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp,
  Function.comp, iSup_le_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
⊢ Measurable (update f a)
[PROOFSTEP]
refine measurable_pi_lambda _ fun x => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
x : δ
⊢ Measurable fun c => update f a c x
[PROOFSTEP]
rcases eq_or_ne x a with (rfl | hx)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
inst✝ : DecidableEq δ
x : δ
⊢ Measurable fun c => update f x c x
[PROOFSTEP]
simpa only [update_same] using measurable_id
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
f : (a : δ) → π a
a : δ
inst✝ : DecidableEq δ
x : δ
hx : x ≠ a
⊢ Measurable fun c => update f a c x
[PROOFSTEP]
simpa only [update_noteq hx] using measurable_const
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
ht : ∀ (i : δ), i ∈ s → MeasurableSet (t i)
⊢ MeasurableSet (Set.pi s t)
[PROOFSTEP]
rw [pi_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
ht : ∀ (i : δ), i ∈ s → MeasurableSet (t i)
⊢ MeasurableSet (⋂ (a : δ) (_ : a ∈ s), eval a ⁻¹' t a)
[PROOFSTEP]
exact MeasurableSet.biInter hs fun i hi => measurable_pi_apply _ (ht i hi)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
h : Set.Nonempty (Set.pi s t)
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
[PROOFSTEP]
classical
rcases h with ⟨f, hf⟩
refine' ⟨fun hst i hi => _, MeasurableSet.pi hs⟩
convert measurable_update f (a := i) hst
rw [update_preimage_pi hi]
exact fun j hj _ => hf j hj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
h : Set.Nonempty (Set.pi s t)
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
[PROOFSTEP]
rcases h with ⟨f, hf⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
⊢ MeasurableSet (Set.pi s t) ↔ ∀ (i : δ), i ∈ s → MeasurableSet (t i)
[PROOFSTEP]
refine' ⟨fun hst i hi => _, MeasurableSet.pi hs⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (t i)
[PROOFSTEP]
convert measurable_update f (a := i) hst
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ t i = update f i ⁻¹' Set.pi s t
[PROOFSTEP]
rw [update_preimage_pi hi]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
f : (i : δ) → π i
hf : f ∈ Set.pi s t
hst : MeasurableSet (Set.pi s t)
i : δ
hi : i ∈ s
⊢ ∀ (j : δ), j ∈ s → j ≠ i → f j ∈ t j
[PROOFSTEP]
exact fun j hj _ => hf j hj
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
⊢ MeasurableSet (Set.pi s t) ↔ (∀ (i : δ), i ∈ s → MeasurableSet (t i)) ∨ Set.pi s t = ∅
[PROOFSTEP]
cases' (pi s t).eq_empty_or_nonempty with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
h : Set.pi s t = ∅
⊢ MeasurableSet (Set.pi s t) ↔ (∀ (i : δ), i ∈ s → MeasurableSet (t i)) ∨ Set.pi s t = ∅
[PROOFSTEP]
simp [h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
π : δ → Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : MeasurableSpace γ
s : Set δ
t : (i : δ) → Set (π i)
hs : Set.Countable s
h : Set.Nonempty (Set.pi s t)
⊢ MeasurableSet (Set.pi s t) ↔ (∀ (i : δ), i ∈ s → MeasurableSet (t i)) ∨ Set.pi s t = ∅
[PROOFSTEP]
simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
⊢ Measurable ↑(piEquivPiSubtypeProd p π).symm
[PROOFSTEP]
refine' measurable_pi_iff.2 fun j => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
[PROOFSTEP]
by_cases hj : p j
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
[PROOFSTEP]
simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => Prod.fst x { val := j, property := (_ : p j) }
[PROOFSTEP]
have : Measurable fun (f : ∀ i : { x // p x }, π i.1) => f ⟨j, hj⟩ :=
  measurable_pi_apply (π := fun i : { x // p x } => π i.1) ⟨j, hj⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
this : Measurable fun f => f { val := j, property := hj }
⊢ Measurable fun x => Prod.fst x { val := j, property := (_ : p j) }
[PROOFSTEP]
exact Measurable.comp this measurable_fst
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
[PROOFSTEP]
simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => Prod.snd x { val := j, property := (_ : ¬p j) }
[PROOFSTEP]
have : Measurable fun (f : ∀ i : { x // ¬p x }, π i.1) => f ⟨j, hj⟩ :=
  measurable_pi_apply (π := fun i : { x // ¬p x } => π i.1) ⟨j, hj⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
this : Measurable fun f => f { val := j, property := hj }
⊢ Measurable fun x => Prod.snd x { val := j, property := (_ : ¬p j) }
[PROOFSTEP]
exact Measurable.comp this measurable_snd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
l : List δ
⊢ Measurable (TProd.mk l)
[PROOFSTEP]
induction' l with i l ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
⊢ Measurable (TProd.mk [])
[PROOFSTEP]
exact measurable_const
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
i : δ
l : List δ
ih : Measurable (TProd.mk l)
⊢ Measurable (TProd.mk (i :: l))
[PROOFSTEP]
exact (measurable_pi_apply i).prod_mk ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
⊢ Measurable fun v => TProd.elim v hj
[PROOFSTEP]
by_cases hji : j = i
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v => TProd.elim v hj
[PROOFSTEP]
subst hji
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v => TProd.elim v hj
[PROOFSTEP]
simpa using measurable_fst
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v hj
[PROOFSTEP]
simp only [TProd.elim_of_ne _ hji]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.snd (_ : j ∈ is)
[PROOFSTEP]
rw [mem_cons] at hj 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj✝ : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.snd (_ : j ∈ is)
[PROOFSTEP]
exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
l : List δ
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod l s)
[PROOFSTEP]
induction' l with i l ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod [] s)
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)
[PROOFSTEP]
exact MeasurableSet.univ
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)
[PROOFSTEP]
exact (hs i).prod ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
⊢ MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s
[PROOFSTEP]
simp [measurableSet_sum_iff, Sum.inl_injective.preimage_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
⊢ MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
[PROOFSTEP]
simp [measurableSet_sum_iff, Sum.inr_injective.preimage_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inl)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)
[PROOFSTEP]
exact MeasurableSet.univ.inl_image
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inr)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)
[PROOFSTEP]
exact MeasurableSet.univ.inr_image
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
s : Set α
h : MeasurableSet (f '' s)
⊢ MeasurableSet s
[PROOFSTEP]
simpa only [hf.injective.preimage_image] using hf.measurable h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (_root_.id '' s)
[PROOFSTEP]
rwa [image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)
[PROOFSTEP]
rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
⊢ MeasurableSet (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)
[PROOFSTEP]
exact hf.measurableSet_image' MeasurableSet.univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
[PROOFSTEP]
rw [← image_preimage_eq_inter_range, hf.measurableSet_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)
[PROOFSTEP]
rwa [preimage_rangeSplitting hf.injective, ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
  coe_comp_rangeFactorization, hf.measurableSet_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')
[PROOFSTEP]
refine' measurable_of_restrict_of_restrict_compl hf.measurableSet_range _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (restrict (range f) (extend f g g'))
[PROOFSTEP]
rw [restrict_extend_range]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x => g (Exists.choose (_ : ↑x ∈ range f))
[PROOFSTEP]
simpa only [rangeSplitting] using hg.comp hf.measurable_rangeSplitting
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (restrict (range f)ᶜ (extend f g g'))
[PROOFSTEP]
rw [restrict_extend_compl_range]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → γ
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)
[PROOFSTEP]
exact hg'.comp measurable_subtype_coe
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f
[PROOFSTEP]
refine' ⟨fun H => _, hg.measurable.comp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f
[PROOFSTEP]
suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
  rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ Measurable f
[PROOFSTEP]
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
[PROOFSTEP]
exact hg.measurable_rangeSplitting.comp H.subtype_mk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
⊢ Injective toEquiv
[PROOFSTEP]
rintro ⟨e₁, _, _⟩ ⟨e₂, _, _⟩ (rfl : e₁ = e₂)
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
e₁ : α ≃ β
measurable_toFun✝¹ : Measurable ↑e₁
measurable_invFun✝¹ : Measurable ↑e₁.symm
measurable_toFun✝ : Measurable ↑e₁
measurable_invFun✝ : Measurable ↑e₁.symm
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun✝¹, measurable_invFun := measurable_invFun✝¹ } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun✝, measurable_invFun := measurable_invFun✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
e : α ≃ᵐ β
s : Set β
h : MeasurableSet (↑e ⁻¹' s)
⊢ MeasurableSet s
[PROOFSTEP]
simpa only [symm_preimage_preimage] using e.symm.measurable h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
e : α ≃ᵐ β
s : Set α
⊢ MeasurableSet (↑e '' s) ↔ MeasurableSet s
[PROOFSTEP]
rw [image_eq_preimage, measurableSet_preimage]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝³ : MeasurableSpace α✝
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
α β : Type ?u.874921
i₁ : MeasurableSpace α
i₂ : MeasurableSpace β
h : α = β
hi : HEq i₁ i₂
⊢ Measurable ↑(Equiv.cast h)
[PROOFSTEP]
subst h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝³ : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
α : Type ?u.874921
i₁ i₂ : MeasurableSpace α
hi : HEq i₁ i₂
⊢ Measurable ↑(Equiv.cast (_ : α = α))
[PROOFSTEP]
subst hi
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝³ : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
α : Type ?u.874921
i₁ : MeasurableSpace α
⊢ Measurable ↑(Equiv.cast (_ : α = α))
[PROOFSTEP]
exact measurable_id
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝³ : MeasurableSpace α✝
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
α β : Type ?u.874921
i₁ : MeasurableSpace α
i₂ : MeasurableSpace β
h : α = β
hi : HEq i₁ i₂
⊢ Measurable ↑(Equiv.cast h).symm
[PROOFSTEP]
subst h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝³ : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
α : Type ?u.874921
i₁ i₂ : MeasurableSpace α
hi : HEq i₁ i₂
⊢ Measurable ↑(Equiv.cast (_ : α = α)).symm
[PROOFSTEP]
subst hi
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝³ : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
α : Type ?u.874921
i₁ : MeasurableSpace α
⊢ Measurable ↑(Equiv.cast (_ : α = α)).symm
[PROOFSTEP]
exact measurable_id
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ↑e)
⊢ Measurable f
[PROOFSTEP]
have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ↑e)
this : Measurable (f ∘ ↑(trans (symm e) e).toEquiv)
⊢ Measurable f
[PROOFSTEP]
rwa [coe_toEquiv, symm_trans_self] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (↑(Equiv.Set.rangeInl α β) ⁻¹' s)
[PROOFSTEP]
refine' ⟨_, hs.inl_image, Set.ext _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
s : Set α
hs : MeasurableSet s
⊢ ∀ (x : { x // x ∈ range Sum.inl }), x ∈ Subtype.val ⁻¹' (Sum.inl '' s) ↔ x ∈ ↑(Equiv.Set.rangeInl α β) ⁻¹' s
[PROOFSTEP]
rintro ⟨ab, a, rfl⟩
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
s : Set α
hs : MeasurableSet s
a : α
⊢ { val := Sum.inl a, property := (_ : ∃ y, Sum.inl y = Sum.inl a) } ∈ Subtype.val ⁻¹' (Sum.inl '' s) ↔
    { val := Sum.inl a, property := (_ : ∃ y, Sum.inl y = Sum.inl a) } ∈ ↑(Equiv.Set.rangeInl α β) ⁻¹' s
[PROOFSTEP]
simp [Set.range_inl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (↑(Equiv.Set.rangeInr α β) ⁻¹' s)
[PROOFSTEP]
refine' ⟨_, hs.inr_image, Set.ext _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
s : Set β
hs : MeasurableSet s
⊢ ∀ (x : { x // x ∈ range Sum.inr }), x ∈ Subtype.val ⁻¹' (Sum.inr '' s) ↔ x ∈ ↑(Equiv.Set.rangeInr α β) ⁻¹' s
[PROOFSTEP]
rintro ⟨ab, b, rfl⟩
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
s : Set β
hs : MeasurableSet s
b : β
⊢ { val := Sum.inr b, property := (_ : ∃ y, Sum.inr y = Sum.inr b) } ∈ Subtype.val ⁻¹' (Sum.inr '' s) ↔
    { val := Sum.inr b, property := (_ : ∃ y, Sum.inr y = Sum.inr b) } ∈ ↑(Equiv.Set.rangeInr α β) ⁻¹' s
[PROOFSTEP]
simp [Set.range_inr]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.902483
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ↑(Equiv.sumProdDistrib α β γ)
[PROOFSTEP]
refine'
  measurable_of_measurable_union_cover (range Sum.inl ×ˢ (univ : Set γ)) (range Sum.inr ×ˢ (univ : Set γ))
    (measurableSet_range_inl.prod MeasurableSet.univ) (measurableSet_range_inr.prod MeasurableSet.univ)
    (by rintro ⟨a | b, c⟩ <;> simp [Set.prod_eq]) _ _
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ univ ⊆ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ
[PROOFSTEP]
rintro ⟨a | b, c⟩
[GOAL]
case mk.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
a : α
⊢ (Sum.inl a, c) ∈ univ → (Sum.inl a, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ
[PROOFSTEP]
simp [Set.prod_eq]
[GOAL]
case mk.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
b : β
⊢ (Sum.inr b, c) ∈ univ → (Sum.inr b, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ
[PROOFSTEP]
simp [Set.prod_eq]
[GOAL]
case refine'_1
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a => ↑(Equiv.sumProdDistrib α β γ) ↑a
[PROOFSTEP]
refine' (Set.prod (range Sum.inl) univ).symm.measurable_comp_iff.1 _
[GOAL]
case refine'_1
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ((fun a => ↑(Equiv.sumProdDistrib α β γ) ↑a) ∘ ↑(symm (Set.prod (range Sum.inl) univ)))
[PROOFSTEP]
refine' (prodCongr Set.rangeInl (Set.univ _)).symm.measurable_comp_iff.1 _
[GOAL]
case refine'_1
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable
    (((fun a => ↑(Equiv.sumProdDistrib α β γ) ↑a) ∘ ↑(symm (Set.prod (range Sum.inl) univ))) ∘
      ↑(symm (prodCongr Set.rangeInl (Set.univ γ))))
[PROOFSTEP]
exact measurable_inl
[GOAL]
case refine'_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a => ↑(Equiv.sumProdDistrib α β γ) ↑a
[PROOFSTEP]
refine' (Set.prod (range Sum.inr) univ).symm.measurable_comp_iff.1 _
[GOAL]
case refine'_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ((fun a => ↑(Equiv.sumProdDistrib α β γ) ↑a) ∘ ↑(symm (Set.prod (range Sum.inr) univ)))
[PROOFSTEP]
refine' (prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 _
[GOAL]
case refine'_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
inst✝³ : MeasurableSpace δ
α : Type ?u.902477
β : Type ?u.902480
γ : Type ?u.903170
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable
    (((fun a => ↑(Equiv.sumProdDistrib α β γ) ↑a) ∘ ↑(symm (Set.prod (range Sum.inr) univ))) ∘
      ↑(symm (prodCongr Set.rangeInr (Set.univ γ))))
[PROOFSTEP]
exact measurable_inr
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
n : ℕ
α : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → MeasurableSpace (α i)
i : Fin (n + 1)
⊢ Measurable fun x => ↑(Equiv.piFinSuccAboveEquiv α i).symm x i
[PROOFSTEP]
simp only [piFinSuccAboveEquiv_symm_apply, Fin.insertNth_apply_same, measurable_fst]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
n : ℕ
α : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → MeasurableSpace (α i)
i : Fin (n + 1)
j : Fin n
⊢ Measurable fun x => ↑(Equiv.piFinSuccAboveEquiv α i).symm x (Fin.succAbove i j)
[PROOFSTEP]
simpa only [piFinSuccAboveEquiv_symm_apply, Fin.insertNth_apply_succAbove] using
  (measurable_pi_apply _).comp measurable_snd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
s : Set α
hf : MeasurableEmbedding f
⊢ Measurable ↑(Equiv.Set.image f s (_ : Injective f)).symm
[PROOFSTEP]
rintro t ⟨u, hu, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u✝ : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
s : Set α
hf : MeasurableEmbedding f
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (↑(Equiv.Set.image f s (_ : Injective f)).symm ⁻¹' (Subtype.val ⁻¹' u))
[PROOFSTEP]
simp [preimage_preimage, Set.image_symm_preimage hf.injective]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u✝ : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
s : Set α
hf : MeasurableEmbedding f
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val ⁻¹' (f '' u))
[PROOFSTEP]
exact measurable_subtype_coe (hf.measurableSet_image' hu)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
hf : MeasurableEmbedding f
⊢ ↑(f '' univ) = ↑(range f)
[PROOFSTEP]
rw [image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
hf : MeasurableEmbedding f
⊢ HEq Subtype.instMeasurableSpace Subtype.instMeasurableSpace
[PROOFSTEP]
rw [image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → α
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
⊢ MeasurableEmbedding f
[PROOFSTEP]
set e : α ≃ᵐ range f :=
  ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective surjective_onto_range⟩, hf₁.subtype_mk, hg⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → α
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : α ≃ᵐ ↑(range f) :=
  {
    toEquiv :=
      { toFun := rangeFactorization f, invFun := g, left_inv := H,
        right_inv := (_ : Function.RightInverse g (rangeFactorization f)) },
    measurable_toFun := (_ : Measurable fun x => { val := f x, property := (_ : f x ∈ range f) }),
    measurable_invFun := hg }
⊢ MeasurableEmbedding f
[PROOFSTEP]
exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
⊢ α ≃ᵐ β
[PROOFSTEP]
let F : Set α → Set α := fun A =>
  (g '' (f '' A)ᶜ)ᶜ
    -- We follow the proof of the usual SB theorem in mathlib,
      -- the crux of which is finding a fixed point of this F.
      -- However, we must find this fixed point manually instead of invoking Knaster-Tarski
      -- in order to make sure it is measurable.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
⊢ α ≃ᵐ β
[PROOFSTEP]
suffices Σ' A : Set α, MeasurableSet A ∧ F A = A
  by
  rcases this with ⟨A, Ameas, Afp⟩
  let B := f '' A
  have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
  refine' (MeasurableEquiv.sumCompl Ameas).symm.trans (MeasurableEquiv.trans _ (MeasurableEquiv.sumCompl Bmeas))
  apply MeasurableEquiv.sumCongr (hf.equivImage _)
  have : Aᶜ = g '' Bᶜ := by
    apply compl_injective
    rw [← Afp]
    simp
  rw [this]
  exact (hg.equivImage _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
this : (A : Set α) ×' MeasurableSet A ∧ F A = A
⊢ α ≃ᵐ β
[PROOFSTEP]
rcases this with ⟨A, Ameas, Afp⟩
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
⊢ α ≃ᵐ β
[PROOFSTEP]
let B := f '' A
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
⊢ α ≃ᵐ β
[PROOFSTEP]
have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ α ≃ᵐ β
[PROOFSTEP]
refine' (MeasurableEquiv.sumCompl Ameas).symm.trans (MeasurableEquiv.trans _ (MeasurableEquiv.sumCompl Bmeas))
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ ↑A ⊕ ↑Aᶜ ≃ᵐ ↑B ⊕ ↑Bᶜ
[PROOFSTEP]
apply MeasurableEquiv.sumCongr (hf.equivImage _)
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ ↑Aᶜ ≃ᵐ ↑Bᶜ
[PROOFSTEP]
have : Aᶜ = g '' Bᶜ := by
  apply compl_injective
  rw [← Afp]
  simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ Aᶜ = g '' Bᶜ
[PROOFSTEP]
apply compl_injective
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ Aᶜᶜ = (g '' Bᶜ)ᶜ
[PROOFSTEP]
rw [← Afp]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ (F A)ᶜᶜ = (g '' Bᶜ)ᶜ
[PROOFSTEP]
simp
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ ↑Aᶜ ≃ᵐ ↑Bᶜ
[PROOFSTEP]
rw [this]
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ ↑(g '' Bᶜ) ≃ᵐ ↑Bᶜ
[PROOFSTEP]
exact (hg.equivImage _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
[PROOFSTEP]
have Fmono : ∀ {A B}, A ⊆ B → F A ⊆ F B := fun h =>
  compl_subset_compl.mpr <| Set.image_subset _ <| compl_subset_compl.mpr <| Set.image_subset _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
[PROOFSTEP]
let X : ℕ → Set α := fun n => F^[n] univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
[PROOFSTEP]
refine' ⟨iInter X, _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ MeasurableSet (iInter X)
[PROOFSTEP]
apply MeasurableSet.iInter
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ ∀ (b : ℕ), MeasurableSet (F^[b] univ)
[PROOFSTEP]
intro n
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
n : ℕ
⊢ MeasurableSet (F^[n] univ)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case refine'_1.h.zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ MeasurableSet (F^[Nat.zero] univ)
[PROOFSTEP]
exact MeasurableSet.univ
[GOAL]
case refine'_1.h.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F^[Nat.succ n] univ)
[PROOFSTEP]
rw [Function.iterate_succ', Function.comp_apply]
[GOAL]
case refine'_1.h.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F (F^[n] univ))
[PROOFSTEP]
exact (hg.measurableSet_image' (hf.measurableSet_image' ih).compl).compl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ F (iInter X) = iInter X
[PROOFSTEP]
apply subset_antisymm
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ F (iInter X) ⊆ iInter X
[PROOFSTEP]
apply subset_iInter
[GOAL]
case refine'_2.a.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ ∀ (i : ℕ), F (iInter X) ⊆ F^[i] univ
[PROOFSTEP]
intro n
[GOAL]
case refine'_2.a.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
n : ℕ
⊢ F (iInter X) ⊆ F^[n] univ
[PROOFSTEP]
cases n
[GOAL]
case refine'_2.a.h.zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ F (iInter X) ⊆ F^[Nat.zero] univ
[PROOFSTEP]
exact subset_univ _
[GOAL]
case refine'_2.a.h.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F^[Nat.succ n✝] univ
[PROOFSTEP]
rw [Function.iterate_succ', Function.comp_apply]
[GOAL]
case refine'_2.a.h.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F (F^[n✝] univ)
[PROOFSTEP]
exact Fmono (iInter_subset _ _)
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
⊢ iInter X ⊆ F (iInter X)
[PROOFSTEP]
rintro x hx ⟨y, hy, rfl⟩
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : g y ∈ iInter X
⊢ False
[PROOFSTEP]
rw [mem_iInter] at hx 
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ False
[PROOFSTEP]
apply hy
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ f '' iInter X
[PROOFSTEP]
rw [(injOn_of_injective hf.injective _).image_iInter_eq]
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ ⋂ (i : ℕ), f '' F^[i] univ
[PROOFSTEP]
rw [mem_iInter]
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ ∀ (i : ℕ), y ∈ f '' F^[i] univ
[PROOFSTEP]
intro n
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
n : ℕ
⊢ y ∈ f '' F^[n] univ
[PROOFSTEP]
specialize hx n.succ
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F^[Nat.succ n] univ
⊢ y ∈ f '' F^[n] univ
[PROOFSTEP]
rw [Function.iterate_succ', Function.comp_apply] at hx 
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
⊢ y ∈ f '' F^[n] univ
[PROOFSTEP]
by_contra h
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
h : ¬y ∈ f '' F^[n] univ
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
case refine'_2.a.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A => (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n => F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
h : ¬y ∈ f '' F^[n] univ
⊢ g y ∈ g '' (f '' F^[n] univ)ᶜ
[PROOFSTEP]
exact ⟨y, h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m : MeasurableSpace β
h : CountablyGenerated β
f : α → β
⊢ CountablyGenerated α
[PROOFSTEP]
rcases h with ⟨⟨b, hbc, rfl⟩⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f : α → β
b : Set (Set β)
hbc : Set.Countable b
⊢ CountablyGenerated α
[PROOFSTEP]
rw [comap_generateFrom]
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f : α → β
b : Set (Set β)
hbc : Set.Countable b
⊢ CountablyGenerated α
[PROOFSTEP]
letI := generateFrom (preimage f '' b)
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
f : α → β
b : Set (Set β)
hbc : Set.Countable b
this : MeasurableSpace α := generateFrom (preimage f '' b)
⊢ CountablyGenerated α
[PROOFSTEP]
exact ⟨_, hbc.image _, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m₁ m₂ : MeasurableSpace β
h₁ : CountablyGenerated β
h₂ : CountablyGenerated β
⊢ CountablyGenerated β
[PROOFSTEP]
rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
m₂ : MeasurableSpace β
h₂ : CountablyGenerated β
b₁ : Set (Set β)
hb₁c : Set.Countable b₁
⊢ CountablyGenerated β
[PROOFSTEP]
rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
[GOAL]
case mk.intro.intro.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
b₁ : Set (Set β)
hb₁c : Set.Countable b₁
b₂ : Set (Set β)
hb₂c : Set.Countable b₂
⊢ CountablyGenerated β
[PROOFSTEP]
exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
s : Set α
h : CountablyGenerated ↑s
inst✝ : MeasurableSingletonClass ↑s
⊢ HasCountableSeparatingOn α MeasurableSet s
[PROOFSTEP]
suffices HasCountableSeparatingOn s MeasurableSet univ from this.of_subtype fun _ ↦ id
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
s : Set α
h : CountablyGenerated ↑s
inst✝ : MeasurableSingletonClass ↑s
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ
[PROOFSTEP]
rcases h.1 with ⟨b, hbc, hb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
s : Set α
h : CountablyGenerated ↑s
inst✝ : MeasurableSingletonClass ↑s
b : Set (Set ↑s)
hbc : Set.Countable b
hb : Subtype.instMeasurableSpace = generateFrom b
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ
[PROOFSTEP]
refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, fun x _ y _ h ↦ ?_⟩⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
s : Set α
h✝ : CountablyGenerated ↑s
inst✝ : MeasurableSingletonClass ↑s
b : Set (Set ↑s)
hbc : Set.Countable b
hb : Subtype.instMeasurableSpace = generateFrom b
x : ↑s
x✝¹ : x ∈ univ
y : ↑s
x✝ : y ∈ univ
h : ∀ (s_1 : Set ↑s), s_1 ∈ b → (x ∈ s_1 ↔ y ∈ s_1)
⊢ x = y
[PROOFSTEP]
rw [← forall_generateFrom_mem_iff_mem_iff, ← hb] at h 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
s : Set α
h✝ : CountablyGenerated ↑s
inst✝ : MeasurableSingletonClass ↑s
b : Set (Set ↑s)
hbc : Set.Countable b
hb : Subtype.instMeasurableSpace = generateFrom b
x : ↑s
x✝¹ : x ∈ univ
y : ↑s
x✝ : y ∈ univ
h : ∀ (s_1 : Set ↑s), MeasurableSet s_1 → (x ∈ s_1 ↔ y ∈ s_1)
⊢ x = y
[PROOFSTEP]
simpa using h { y }
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : HasCountableSeparatingOn α MeasurableSet univ
⊢ ∃ f, Measurable f ∧ Injective f
[PROOFSTEP]
rcases exists_seq_separating α MeasurableSet.empty univ with ⟨e, hem, he⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : HasCountableSeparatingOn α MeasurableSet univ
e : ℕ → Set α
hem : ∀ (n : ℕ), MeasurableSet (e n)
he : ∀ (x : α), x ∈ univ → ∀ (y : α), y ∈ univ → (∀ (n : ℕ), x ∈ e n ↔ y ∈ e n) → x = y
⊢ ∃ f, Measurable f ∧ Injective f
[PROOFSTEP]
refine ⟨(· ∈ e ·), ?_, ?_⟩
[GOAL]
case intro.intro.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : HasCountableSeparatingOn α MeasurableSet univ
e : ℕ → Set α
hem : ∀ (n : ℕ), MeasurableSet (e n)
he : ∀ (x : α), x ∈ univ → ∀ (y : α), y ∈ univ → (∀ (n : ℕ), x ∈ e n ↔ y ∈ e n) → x = y
⊢ Measurable fun x x_1 => decide (x ∈ e x_1)
[PROOFSTEP]
rw [measurable_pi_iff]
[GOAL]
case intro.intro.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : HasCountableSeparatingOn α MeasurableSet univ
e : ℕ → Set α
hem : ∀ (n : ℕ), MeasurableSet (e n)
he : ∀ (x : α), x ∈ univ → ∀ (y : α), y ∈ univ → (∀ (n : ℕ), x ∈ e n ↔ y ∈ e n) → x = y
⊢ ∀ (a : ℕ), Measurable fun x => decide (x ∈ e a)
[PROOFSTEP]
refine fun n ↦ measurable_to_bool ?_
[GOAL]
case intro.intro.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : HasCountableSeparatingOn α MeasurableSet univ
e : ℕ → Set α
hem : ∀ (n : ℕ), MeasurableSet (e n)
he : ∀ (x : α), x ∈ univ → ∀ (y : α), y ∈ univ → (∀ (n : ℕ), x ∈ e n ↔ y ∈ e n) → x = y
n : ℕ
⊢ MeasurableSet ((fun x => decide (x ∈ e n)) ⁻¹' {true})
[PROOFSTEP]
simpa only [preimage, mem_singleton_iff, Bool.decide_iff, setOf_mem_eq] using hem n
[GOAL]
case intro.intro.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : HasCountableSeparatingOn α MeasurableSet univ
e : ℕ → Set α
hem : ∀ (n : ℕ), MeasurableSet (e n)
he : ∀ (x : α), x ∈ univ → ∀ (y : α), y ∈ univ → (∀ (n : ℕ), x ∈ e n ↔ y ∈ e n) → x = y
⊢ Injective fun x x_1 => decide (x ∈ e x_1)
[PROOFSTEP]
exact fun x y h ↦ he x trivial y trivial fun n ↦ decide_eq_decide.1 <| congr_fun h _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : IsMeasurablyGenerated f
inst✝ : IsMeasurablyGenerated g
⊢ IsMeasurablyGenerated (f ⊓ g)
[PROOFSTEP]
constructor
[GOAL]
case exists_measurable_subset
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : IsMeasurablyGenerated f
inst✝ : IsMeasurablyGenerated g
⊢ ∀ ⦃s : Set α⦄, s ∈ f ⊓ g → ∃ t, t ∈ f ⊓ g ∧ MeasurableSet t ∧ t ⊆ s
[PROOFSTEP]
rintro t ⟨sf, hsf, sg, hsg, rfl⟩
[GOAL]
case exists_measurable_subset.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : IsMeasurablyGenerated f
inst✝ : IsMeasurablyGenerated g
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
⊢ ∃ t, t ∈ f ⊓ g ∧ MeasurableSet t ∧ t ⊆ sf ∩ sg
[PROOFSTEP]
rcases IsMeasurablyGenerated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩
[GOAL]
case exists_measurable_subset.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : IsMeasurablyGenerated f
inst✝ : IsMeasurablyGenerated g
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
⊢ ∃ t, t ∈ f ⊓ g ∧ MeasurableSet t ∧ t ⊆ sf ∩ sg
[PROOFSTEP]
rcases IsMeasurablyGenerated.exists_measurable_subset hsg with ⟨s'g, hs'g, hmg, hs'sg⟩
[GOAL]
case exists_measurable_subset.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : IsMeasurablyGenerated f
inst✝ : IsMeasurablyGenerated g
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ ∃ t, t ∈ f ⊓ g ∧ MeasurableSet t ∧ t ⊆ sf ∩ sg
[PROOFSTEP]
refine' ⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, _⟩
[GOAL]
case exists_measurable_subset.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : IsMeasurablyGenerated f
inst✝ : IsMeasurablyGenerated g
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ s'f ∩ s'g ⊆ sf ∩ sg
[PROOFSTEP]
exact inter_subset_inter hs'sf hs'sg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
⊢ IsMeasurablyGenerated (𝓟 s) ↔ MeasurableSet s
[PROOFSTEP]
refine' ⟨_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
⊢ IsMeasurablyGenerated (𝓟 s) → MeasurableSet s
[PROOFSTEP]
rintro ⟨hs⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s
[PROOFSTEP]
rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩
[GOAL]
case mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s
[PROOFSTEP]
have : t = s := hts.antisymm ht
[GOAL]
case mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
⊢ MeasurableSet s
[PROOFSTEP]
rwa [← this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
⊢ IsMeasurablyGenerated (⨅ (i : ι), f i)
[PROOFSTEP]
refine' ⟨fun s hs => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
s : Set α
hs : s ∈ ⨅ (i : ι), f i
⊢ ∃ t, t ∈ ⨅ (i : ι), f i ∧ MeasurableSet t ∧ t ⊆ s
[PROOFSTEP]
rw [← Equiv.plift.surjective.iInf_comp, mem_iInf] at hs 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
s : Set α
hs : ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ f (↑Equiv.plift ↑i)) ∧ s = ⋂ (i : ↑I), V i
⊢ ∃ t, t ∈ ⨅ (i : ι), f i ∧ MeasurableSet t ∧ t ⊆ s
[PROOFSTEP]
rcases hs with ⟨t, ht, ⟨V, hVf, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
⊢ ∃ t_1, t_1 ∈ ⨅ (i : ι), f i ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : ↑t), V i
[PROOFSTEP]
choose U hUf hU using fun i => IsMeasurablyGenerated.exists_measurable_subset (hVf i)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (↑Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ∃ t_1, t_1 ∈ ⨅ (i : ι), f i ∧ MeasurableSet t_1 ∧ t_1 ⊆ ⋂ (i : ↑t), V i
[PROOFSTEP]
refine' ⟨⋂ i : t, U i, _, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (↑Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ (i : ↑t), U i ∈ ⨅ (i : ι), f i
[PROOFSTEP]
rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (↑Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ∃ I, Set.Finite I ∧ ∃ V, (∀ (i : ↑I), V i ∈ f (↑Equiv.plift ↑i)) ∧ ⋂ (i : ↑t), U i = ⋂ (i : ↑I), V i
[PROOFSTEP]
refine' ⟨t, ht, U, hUf, rfl⟩
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (↑Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ (i : ↑t), U i)
[PROOFSTEP]
haveI := ht.countable.toEncodable.countable
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (↑Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
this : Countable ↑t
⊢ MeasurableSet (⋂ (i : ↑t), U i)
[PROOFSTEP]
exact MeasurableSet.iInter fun i => (hU i).1
[GOAL]
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t✝ u : Set α
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), IsMeasurablyGenerated (f i)
t : Set (PLift ι)
ht : Set.Finite t
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (↑Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (↑Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ (i : ↑t), U i ⊆ ⋂ (i : ↑t), V i
[PROOFSTEP]
exact iInter_mono fun i => (hU i).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (blimsup s atTop p)
[PROOFSTEP]
simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋂ (i : ℕ), ⋃ (j : ℕ) (_ : p j ∧ i ≤ j), s j)
[PROOFSTEP]
exact .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (bliminf s atTop p)
[PROOFSTEP]
simp only [Filter.bliminf_eq_iSup_biInf_of_nat, iInf_eq_iInter, iSup_eq_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋃ (i : ℕ), ⋂ (j : ℕ) (_ : p j ∧ i ≤ j), s j)
[PROOFSTEP]
exact .iUnion fun n => .iInter fun m => .iInter fun hm => h m hm.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (limsup s atTop)
[PROOFSTEP]
simpa only [← blimsup_true] using measurableSet_blimsup fun n _ => hs n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
⊢ MeasurableSet (liminf s atTop)
[PROOFSTEP]
simpa only [← bliminf_true] using measurableSet_bliminf fun n _ => hs n
