ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
⊢ AEMeasurable f
nontriviality β
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
⊢ AEMeasurable f
inhabit β
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ AEMeasurable f
set s : ι → Set α := fun i => toMeasurable (μ i) { x | f x ≠ (h i).mk f x }
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ AEMeasurable f
have hsμ : ∀ i, μ i (s i) = 0 := by
  intro i
  rw [measure_toMeasurable]
  exact (h i).ae_eq_mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
⊢ AEMeasurable f
have hsm : MeasurableSet (⋂ i, s i) :=
  MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
⊢ AEMeasurable f
have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
  intro i x hx
  contrapose! hx
  exact subset_toMeasurable _ _ hx
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ AEMeasurable f
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
⊢ AEMeasurable f
set g : α → β := (⋂ i, s i).piecewise (const α default) f
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i) g)

case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict ((⋂ (i : ι), s i)ᶜ) g)

case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ AEMeasurable f
refine' ⟨g, measurable_of_restrict_of_restrict_compl hsm _ _, ae_sum_iff.mpr fun i => _⟩
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
⊢ ↑↑(μ i) (s i) = 0
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ ∀ (i : ι), ↑↑(μ i) (s i) = 0
intro i
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
⊢ ↑↑(μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x} = 0
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
⊢ ↑↑(μ i) (s i) = 0
rw [measure_toMeasurable]
no goals
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
⊢ ↑↑(μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x} = 0
exact (h i).ae_eq_mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
i : ι
x : α
hx : ¬x ∈ s i
⊢ f x = mk f (_ : AEMeasurable f) x
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
⊢ ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
intro i x hx
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
i : ι
x : α
hx : f x ≠ mk f (_ : AEMeasurable f) x
⊢ x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
i : ι
x : α
hx : ¬x ∈ s i
⊢ f x = mk f (_ : AEMeasurable f) x
contrapose! hx
no goals
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
i : ι
x : α
hx : f x ≠ mk f (_ : AEMeasurable f) x
⊢ x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
exact subset_toMeasurable _ _ hx
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i) (const α default))
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i) g)
rw [restrict_piecewise]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable fun x => default
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i) (const α default))
simp only [Set.restrict, const]
no goals
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable fun x => default
exact measurable_const
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋃ (i : ι), s iᶜ) f)
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict ((⋂ (i : ι), s i)ᶜ) g)
rw [restrict_piecewise_compl, compl_iInter]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (Set.restrict (⋃ (i : ι), s iᶜ) f ⁻¹' t)
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋃ (i : ι), s iᶜ) f)
intro t ht
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ (Subtype.val ⁻¹' ⋃ (i : ι), mk f (_ : AEMeasurable f) ⁻¹' t ∩ s iᶜ) = Set.restrict (⋃ (i : ι), s iᶜ) f ⁻¹' t
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (Set.restrict (⋃ (i : ι), s iᶜ) f ⁻¹' t)
refine'
  ⟨⋃ i, (h i).mk f ⁻¹' t ∩ s iᶜ,
    MeasurableSet.iUnion fun i =>
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl,
    _⟩
case refine'_2.h.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : x ∈ ⋃ (i : ι), s iᶜ
⊢ ({ val := x, property := hx } ∈ Subtype.val ⁻¹' ⋃ (i : ι), mk f (_ : AEMeasurable f) ⁻¹' t ∩ s iᶜ) ↔
    { val := x, property := hx } ∈ Set.restrict (⋃ (i : ι), s iᶜ) f ⁻¹' t
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ (Subtype.val ⁻¹' ⋃ (i : ι), mk f (_ : AEMeasurable f) ⁻¹' t ∩ s iᶜ) = Set.restrict (⋃ (i : ι), s iᶜ) f ⁻¹' t
ext ⟨x, hx⟩
case refine'_2.h.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ (∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) ↔ f x ∈ t
case refine'_2.h.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : x ∈ ⋃ (i : ι), s iᶜ
⊢ ({ val := x, property := hx } ∈ Subtype.val ⁻¹' ⋃ (i : ι), mk f (_ : AEMeasurable f) ⁻¹' t ∩ s iᶜ) ↔
    { val := x, property := hx } ∈ Set.restrict (⋃ (i : ι), s iᶜ) f ⁻¹' t
simp only [mem_preimage, mem_iUnion, Subtype.coe_mk, Set.restrict, mem_inter_iff,
  mem_compl_iff] at hx⊢
case refine'_2.h.mk.mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ (∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) → f x ∈ t

case refine'_2.h.mk.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t → ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
case refine'_2.h.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ (∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) ↔ f x ∈ t
constructor
case refine'_2.h.mk.mp.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
hxt : mk f (_ : AEMeasurable f) x ∈ t
hxs : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t
case refine'_2.h.mk.mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ (∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) → f x ∈ t
rintro ⟨i, hxt, hxs⟩
no goals
case refine'_2.h.mk.mp.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
hxt : mk f (_ : AEMeasurable f) x ∈ t
hxs : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t
rwa [hs _ _ hxs]
case refine'_2.h.mk.mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t → ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
case refine'_2.h.mk.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t → ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
rcases hx with ⟨i, hi⟩
case refine'_2.h.mk.mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ mk f (_ : AEMeasurable f) x ∈ t →
    ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
case refine'_2.h.mk.mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t → ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
rw [hs _ _ hi]
no goals
case refine'_2.h.mk.mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ mk f (_ : AEMeasurable f) x ∈ t →
    ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
exact fun h => ⟨i, h, hi⟩
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : f x ≠ g x
⊢ x ∈ s i
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x
refine' measure_mono_null (fun x (hx : f x ≠ g x) => _) (hsμ i)
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : ¬x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
⊢ f x = piecewise (⋂ (i : ι), s i) (const α default) f x
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : f x ≠ g x
⊢ x ∈ s i
contrapose! hx
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : ¬x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
⊢ ¬x ∈ ⋂ (i : ι), s i
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : ¬x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
⊢ f x = piecewise (⋂ (i : ι), s i) (const α default) f x
refine' (piecewise_eq_of_not_mem _ _ _ _).symm
no goals
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.987471
δ : Type ?u.987474
R : Type ?u.987477
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
inst✝ : Countable ι
μ : ι → MeasureTheory.Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : ¬x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
⊢ ¬x ∈ ⋂ (i : ι), s i
exact fun h => hx (mem_iInter.1 h i)