awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ : ℝ≥0∞)
have 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∞)
Tactic: rw [← pi_univ, pi_pi μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : Set ι
Tactic: rw [← pi_univ, pi_pi μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 ι
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) univ)
Tactic: rw [← pi_univ, pi_pi μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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∞)
have 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∞)
Tactic: rw [ball_pi _ hr, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ 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∞)
have 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))
Tactic: rw [ball_pi _ hr, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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∞)
have 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∞)
Tactic: rw [closedBall_pi _ hr, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ 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∞)
have 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))
Tactic: rw [closedBall_pi _ hr, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
⊢ Measure.pi (α := β) μ = dirac x
have this : ∀ (a : α), SigmaFinite (μ a)
Tactic: haveI : ∀ a, SigmaFinite (μ a) := isEmptyElim
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
have 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∞)
Tactic: refine pi_eq fun s _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ Eq (α := ℝ≥0∞) ((dirac x : (a : Set ((i : α) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)
    (∏ i : α, (μ i : (a : Set (β i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : x ∈ Set.pi (α := β) univ s
Tactic: rw [Fintype.prod_empty, dirac_apply_of_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
α : Type u_4
inst : Fintype α
inst_1 : IsEmpty α
β : α → Type u_5
m : (α : α) → MeasurableSpace (β α)
μ : (a : α) → Measure (β a)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := β) μ : (a : Set ((i : α) → β i)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((dirac fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β x) a : (a : Set ((i : α) → β i)) → ℝ≥0∞) univ : ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [pi_of_empty, measure_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := β) μ : (a : Set ((i : α) → β i)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [pi_of_empty, measure_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rcases exists_measurable_superset_of_null hs with ⟨t, hst, _, hμt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have suffices : Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices Measure.pi μ (eval i ⁻¹' t) = 0 from measure_mono_null (preimage_mono hst) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' t) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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
Tactic: rw [← univ_pi_update_univ, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i_1))
    0
have apply : Eq (α := ℝ≥0∞)
  ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i t i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply Finset.prod_eq_zero (Finset.mem_univ i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ QuasiMeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)
have 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∞)
Tactic: refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((x : ι) → α x)) → ℝ≥0∞) (eval (β := α) i ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ QuasiMeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)
have 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∞)
Tactic: classical
  refine ⟨by fun_prop, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply (by fun_prop) hs, pi_eval_preimage_null μ h2s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 : ι
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) =
    HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i)
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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∞)
have 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∞)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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∞)
have h : Eq (α := ℝ≥0∞)
  (∏ x ∈ Finset.erase Finset.univ i,
    (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x))
  (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
Tactic: congrm ?_ * ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ i,
      (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x))
    (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
⊢ 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∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i) : ℝ≥0∞)
  ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: congrm ?_ * ?_