awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
this : Encodable ι
rw :
  Eq (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [← pi'_eq_pi, pi'_pi]

Premises used: MeasureTheory.Measure.pi'_pi, MeasureTheory.Measure.pi'_eq_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ fun (i : ι) ↦ univ) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ : Set ι
rw₂ rw₃ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← pi_univ, pi_pi μ]

Premises used: MeasureTheory.Measure.pi_univ, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
f : (i : ι) → α i
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) {f})
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) {f i})

Tactic:
simpa [Set.univ_pi_singleton, -pi_pi] using pi_pi μ fun i ↦ {f i}

Premises used: Singleton.singleton, Set.univ_pi_singleton, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
⊢ IsFiniteMeasure (Measure.pi (α := α) μ)

Tactic:
⟨Measure.pi_univ μ ▸ ENNReal.prod_lt_top (fun i _ ↦ measure_lt_top (μ i) _)⟩

Premises used: ENNReal.prod_lt_top, MeasureTheory.measure_lt_top, Set.univ, Eq.rec, MeasureTheory.Measure.pi_univ, MeasureTheory.IsFiniteMeasure.mk, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α_1 : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α_1 i)
inst_1 : (i : ι) → MeasurableSpace (α_1 i)
μ : (i : ι) → Measure (α_1 i)
α : ι → Type u_4
inst_2 : (i : ι) → MeasureSpace (α i)
inst_3 : ∀ (i : ι), IsFiniteMeasure.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsFiniteMeasure (α := (i : ι) → α i) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
pi.instIsFiniteMeasure _

Premises used: MeasureTheory.Measure.pi.instIsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp only [Measure.pi_univ, measure_univ, Finset.prod_const_one]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.Measure.pi_univ, Finset.prod_const_one
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : (i : ι) → Set (α i)
s : Finset ι
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := α) f) : ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (α i)) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp [← Set.univ_pi_ite, pi_pi, apply_ite]

Premises used: apply_ite, Set.univ_pi_ite, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : (i : ι) → Set (α i)
s : Finset ι
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := α) f) : ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (α i)) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
classical simp [← Set.univ_pi_ite, pi_pi, apply_ite]

Premises used: apply_ite, Set.univ_pi_ite, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α_1 : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α_1 i)
inst_1 : (i : ι) → MeasurableSpace (α_1 i)
μ : (i : ι) → Measure (α_1 i)
α : ι → Type u_4
inst_2 : (i : ι) → MeasureSpace (α i)
inst_3 : ∀ (i : ι), IsProbabilityMeasure.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsProbabilityMeasure (α := (i : ι) → α i) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
pi.instIsProbabilityMeasure _

Premises used: MeasureTheory.Measure.pi.instIsProbabilityMeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (b : ι) ↦ Metric.ball (x b) r) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.ball (x i) r) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.ball (x i) r))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.ball (x i) r))
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.ball (x i) r) : ℝ≥0∞)

Tactic:
rw [ball_pi _ hr, pi_pi]

Premises used: ball_pi, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (b : ι) ↦ Metric.closedBall (x b) r) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.closedBall (x i) r) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.closedBall (x i) r))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.closedBall (x i) r))
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Metric.closedBall (x i) r) : ℝ≥0∞)

Tactic:
rw [closedBall_pi _ hr, pi_pi]

Premises used: closedBall_pi, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.pi (α := α) μ)

Tactic:
(FiniteSpanningSetsIn.pi fun i => (μ i).toFiniteSpanningSetsIn).sigmaFinite

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite, MeasureTheory.Measure.toFiniteSpanningSetsIn
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α_1 : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α_1 i)
inst_1 : (i : ι) → MeasurableSpace (α_1 i)
μ : (i : ι) → Measure (α_1 i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
α : ι → Type u_4
inst_3 : (i : ι) → MeasureSpace (α i)
inst_4 : ∀ (i : ι), SigmaFinite.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ SigmaFinite (α := (i : ι) → α i) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
pi.sigmaFinite _

Premises used: MeasureTheory.Measure.pi.sigmaFinite
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
⊢ ∀ (a : α), SigmaFinite (μ a)

Tactic:
haveI : ∀ a, SigmaFinite (μ a) := isEmptyElim
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
⊢ Measure.pi (α := β) μ = dirac x

Tactic:
pi_eq fun s _ => ?_

Premises used: MeasureTheory.Measure.pi_eq
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
refine :
  ∀ (s : (i : α) → Set (β i)),
    (∀ (i : α), MeasurableSet (s i)) →
      Eq (α := ℝ≥0∞) ((dirac x : (a : Set ((i : α) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)
        (∏ i : α, (μ i : (a : Set (β i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Measure.pi (α := β) μ = dirac x

Tactic:
refine pi_eq fun s _ => ?_

Premises used: MeasureTheory.Measure.pi_eq
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
h : ∀ (i : α), MeasurableSet (s i)
rw : x ∈ Set.pi (α := β) univ s
⊢ Eq (α := ℝ≥0∞) ((dirac x : (a : Set ((i : α) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)
    (∏ i : α, (μ i : (a : Set (β i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [Fintype.prod_empty, dirac_apply_of_mem]

Premises used: MeasureTheory.Measure.dirac_apply_of_mem, Fintype.prod_empty
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
h : ∀ (i : α), MeasurableSet (s i)
⊢ x ∈ Set.pi (α := β) univ s

Tactic:
isEmptyElim (α := α)

Premises used: Set.Mem, isEmptyElim, setOf, Set.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
h : ∀ (i : α), MeasurableSet (s i)
⊢ x ∈ Set.pi (α := β) univ s

Tactic:
exact isEmptyElim (α := α)
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : IsEmpty ι
α : ι → Type u_5
inst_2 : (i : ι) → MeasureSpace (α i)
x : (a : ι) → α a
⊢ Eq (α := Measure ((i : ι) → α i)) volume (dirac x)

Tactic:
Measure.pi_of_empty _ _

Premises used: MeasureTheory.Measure.pi_of_empty
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (α : α) → MeasurableSpace (β α)
μ : (a : α) → Measure (β a)
rw :
  Eq (α := ℝ≥0∞)
    ((dirac fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β x) a : (a : Set ((i : α) → β i)) → ℝ≥0∞) univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := β) μ : (a : Set ((i : α) → β i)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [pi_of_empty, measure_univ]

Premises used: MeasureTheory.Measure.pi_of_empty, isEmptyElim, MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rcases :
  ∀ (t : Set (α i)) (hst : s ⊆ t),
    MeasurableSet t →
      ∀ (hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞)
          (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α i)
hst : s ⊆ t
left : MeasurableSet t
hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
suffices :
  Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
suffices Measure.pi μ (eval i ⁻¹' t) = 0 from measure_mono_null (preimage_mono hst) this
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α i)
hst : s ⊆ t
left : MeasurableSet t
hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞)
    (∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i_1))
    0
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← univ_pi_update_univ, pi_pi]

Premises used: Set.univ_pi_update_univ, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α i)
hst : s ⊆ t
left : MeasurableSet t
hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
apply :
  Eq (α := ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i_1))
    0

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

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α i)
hst : s ⊆ t
left : MeasurableSet t
hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [hμt]
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
is :
  ∀ (t : Set (α i)) (hst : s ⊆ t),
    MeasurableSet t →
      ∀ (hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞)
          (0 : ℝ≥0∞)
is₁ :
  ∀ (t : Set (α i)) (hst : s ⊆ t),
    MeasurableSet t →
      ∀ (hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' t) : ℝ≥0∞)
          (0 : ℝ≥0∞)
is₂ :
  ∀ (t : Set (α i)) (hst : s ⊆ t),
    MeasurableSet t →
      ∀ (hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞)
          (∏ i_1 : ι,
            (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i_1))
          0
is₃ :
  ∀ (t : Set (α i)) (hst : s ⊆ t),
    MeasurableSet t →
      ∀ (hμt : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞)
          ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i) : ℝ≥0∞)
          (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
classical
  -- WLOG, `s` is measurable
  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
  -- Now rewrite it as `Set.pi`, and apply `pi_pi`
  rw [← univ_pi_update_univ, pi_pi]
  apply Finset.prod_eq_zero (Finset.mem_univ i)
  simp [hμt]

Premises used: Finset.mem_univ, Finset.prod_eq_zero, Set.univ_pi_update_univ, MeasureTheory.exists_measurable_superset_of_null, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ Measurable (α := (x : ι) → α x) (eval (β := α) i)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
refine :
  ∀ (s : Set (α i)) (hs : MeasurableSet s) (h2s : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ QuasiMeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)

Tactic:
refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable (α := (x : ι) → α x) (eval (β := α) i)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((x : ι) → α x)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]

Premises used: MeasureTheory.Measure.pi_eval_preimage_null, MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
refine :
  ∀ (s : Set (α i)) (hs : MeasurableSet s) (h2s : Eq (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ QuasiMeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)

Tactic:
classical
  refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
h :
  ∀ (s : Set (α i)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
            (a : Set (α i)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) =
    HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ Membership.mem (γ := Finset ι) Finset.univ i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (∏ x ∈ Finset.erase Finset.univ i,
          (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x) :
        ℝ≥0∞)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]

Premises used: Finset.prod_erase_mul, MeasureTheory.Measure.map_apply, measurable_pi_apply, MeasureTheory.Measure.smul_apply, Set.univ_pi_update_univ, smul_eq_mul, MeasureTheory.Measure.pi_pi