-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_eval_preimage_null {i : ι} {s : Set (α i)} (hs : μ i s = 0) :
    Measure.pi μ (eval i ⁻¹' s) = 0

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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

Tactic:
suffices Measure.pi μ (eval i ⁻¹' t) = 0 from measure_mono_null (preimage_mono hst) this

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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
⊢ ∏ i_1 : ι, (μ i_1) (update (fun j => univ) i t i_1) = 0

Tactic:
apply Finset.prod_eq_zero (Finset.mem_univ i)

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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
⊢ (μ i) (update (fun j => univ) i t i) = 0

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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

Tactic:
classical
rcases exists_measurable_superset_of_null hs with ⟨t, hst, _, hμt⟩
suffices Measure.pi μ (eval i ⁻¹' t) = 0 from measure_mono_null (preimage_mono hst) this
rw [← univ_pi_update_univ, pi_pi]
apply Finset.prod_eq_zero (Finset.mem_univ i)
simp [hμt]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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

Tactic:
rcases exists_measurable_superset_of_null hs with ⟨t, hst, _, hμt⟩

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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
⊢ (μ i) (update (fun j => univ) i t i) = 0

Tactic:
simp [hμt]

Result:
no goals

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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

Tactic:
rw [← univ_pi_update_univ, pi_pi]

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
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
⊢ ∏ i_1 : ι, (μ i_1) (update (fun j => univ) i t i_1) = 0