case intro.intro.intro
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0
rcases exists_measurable_superset_of_null hs with ⟨t, hst, _, hμt⟩
case intro.intro.intro
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
this : ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0

case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
case intro.intro.intro
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0
suffices : Measure.pi μ (eval i ⁻¹' t) = 0
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
case intro.intro.intro
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
this : ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0

case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
exact measure_mono_null (preimage_mono hst) this
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
clear! s
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ∏ i_1 : ι, ↑↑(μ i_1) (update (fun j => univ) i t i_1) = 0
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
rw [← univ_pi_update_univ, pi_pi]
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(μ i) (update (fun j => univ) i t i) = 0
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ∏ i_1 : ι, ↑↑(μ i_1) (update (fun j => univ) i t i_1) = 0
apply Finset.prod_eq_zero (Finset.mem_univ i)
no goals
case this
ι : Type u_2
ι' : Type ?u.3165675
α : ι → Type u_1
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(μ i) (update (fun j => univ) i t i) = 0
simp [hμt]