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 ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : Set.pi (α := α) univ s = ∅
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
have inr : ∀ (i : ι) (hi : s i = ∅),
  piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
Tactic: rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : Set.pi (α := α) univ s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
have this : ∃ (i : ι), Eq (α := ℝ≥0∞) ((m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ fun (i : ι) ↦ eval (β := α) i '' s) = piPremeasure (α := α) m s
have simp : ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) ((fun (a : (x : ι) → α x) ↦ a i) '' s) = piPremeasure (α := α) m s
Tactic: simp only [eval, piPremeasure_pi']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have inl : ∀ (h : Set.pi (α := α) univ s = ∅),
  LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rcases (pi univ s).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
inl :
  ∀ (h : Set.pi (α := α) univ s = ∅),
    LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
      (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have inr : ∀ (h : (Set.pi (α := α) univ s).Nonempty),
  LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rcases (pi univ s).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ n ≤ OuterMeasure.pi (α := α) m ↔
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) ↔
  ∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [OuterMeasure.pi, le_boundedBy']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) ↔
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have mp : (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) →
  ∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
mp :
  (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) →
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) ↔
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have mpr : (∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)) →
  ∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h :
  ∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s
have mpr : Set.Nonempty (α := (i : ι) → α i) (Set.pi (α := α) univ fun (i : ι) ↦ eval (β := α) i '' s)
Tactic: refine le_trans (n.mono <| subset_pi_eval_image univ s) (h _ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
⊢ Measure (TProd X l)
have nil : Measure (TProd X [])
Tactic: induction l with
  | nil => exact dirac PUnit.unit
  | cons i l ih => exact (μ i).prod (α := X i) ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
nil : Measure (TProd X [])
⊢ Measure (TProd X l)
have cons : (i : δ) → (l : List δ) → (ih : Measure (TProd X l)) → Measure (TProd X (i :: l))
Tactic: induction l with
  | nil => exact dirac PUnit.unit
  | cons i l ih => exact (μ i).prod (α := X i) ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod (X := X) l μ)
⊢ SigmaFinite (Measure.tprod (X := X) (i :: l) μ)
have cons : SigmaFinite ((μ i).prod (Measure.tprod (X := X) l μ))
Tactic: rw [tprod_cons]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod (X := X) l μ)
have nil : SigmaFinite (α := TProd X []) (Measure.tprod (X := X) [] μ)
Tactic: induction l with
  | nil => rw [tprod_nil]; infer_instance
  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
nil : SigmaFinite (α := TProd X []) (Measure.tprod (X := X) [] μ)
⊢ SigmaFinite (Measure.tprod (X := X) l μ)
have cons : ∀ (i : δ) (l : List δ) (ih : SigmaFinite (Measure.tprod (X := X) l μ)), SigmaFinite (Measure.tprod (X := X) (i :: l) μ)
Tactic: induction l with
  | nil => rw [tprod_nil]; infer_instance
  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih :
  Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.tprod (X := X) (a :: l) μ : (a : Set (TProd X (a :: l))) → ℝ≥0∞) (Set.tprod (α := X) (a :: l) s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) (a :: l)) : ℝ≥0∞)
have cons : Eq (α := ℝ≥0∞)
  (((μ a).prod (Measure.tprod (X := X) l μ) : (a : Set (TProd X (a :: l))) → ℝ≥0∞) (s a ×ˢ Set.tprod (α := X) l s) :
    ℝ≥0∞)
  (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) (a :: l)) : ℝ≥0∞)
Tactic: rw [tprod_cons, Set.tprod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih :
  Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
⊢ ((μ a).prod (Measure.tprod (X := X) l μ) :
        (a : Set (X a × foldr (fun (i : δ) (β : Type u_5) ↦ X i × β) PUnit.{u_5 + 1} l)) → ℝ≥0∞)
      (s a ×ˢ Set.tprod (α := X) l s) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
have cons : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
    ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
Tactic: rw [prod_prod, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih :
  Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
cons :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
⊢ ((μ a).prod (Measure.tprod (X := X) l μ) :
        (a : Set (X a × foldr (fun (i : δ) (β : Type u_5) ↦ X i × β) PUnit.{u_5 + 1} l)) → ℝ≥0∞)
      (s a ×ˢ Set.tprod (α := X) l s) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
have cons₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
Tactic: rw [prod_prod, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
⊢ Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
have nil : Eq (α := ℝ≥0∞)
  (((Measure.tprod (X := X) [] μ : Measure (TProd X [])) : (a : Set (TProd X [])) → ℝ≥0∞) (Set.tprod (α := X) [] s) :
    ℝ≥0∞)
  (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) []) : ℝ≥0∞)
Tactic: induction l with
  | nil => simp
  | cons a l ih =>
    rw [tprod_cons, Set.tprod]
    dsimp only [foldr_cons, map_cons, prod_cons]
    rw [prod_prod, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
nil :
  Eq (α := ℝ≥0∞)
    (((Measure.tprod (X := X) [] μ : Measure (TProd X [])) : (a : Set (TProd X [])) → ℝ≥0∞) (Set.tprod (α := X) [] s) :
      ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) []) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
have cons : ∀ (a : δ) (l : List δ)
  (ih :
    Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((Measure.tprod (X := X) (a :: l) μ : (a : Set (TProd X (a :: l))) → ℝ≥0∞) (Set.tprod (α := X) (a :: l) s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) (a :: l)) : ℝ≥0∞)
Tactic: induction l with
  | nil => simp
  | cons a l ih =>
    rw [tprod_cons, Set.tprod]
    dsimp only [foldr_cons, map_cons, prod_cons]
    rw [prod_prod, ih]
Cleared hypotheses: l
-- 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 : Encodable ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ Eq (α := ℝ≥0∞)
    ((map (TProd.elim' (α := α) ⋯) (Measure.tprod (X := α) (sortedUniv ι) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have _hl : (sortedUniv ι).Nodup
Tactic: rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
    MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
    List.prod_toFinset, sortedUniv_toFinset]
-- 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 : Encodable ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ Eq (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((map (TProd.elim' (α := α) sorry) (Measure.tprod (X := α) (sortedUniv ι) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      (Set.pi (α := α) univ s) :
    ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: classical
  rw [pi']
  rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
    MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
    List.prod_toFinset, sortedUniv_toFinset] <;>
  exact sortedUniv_nodup ι
-- 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)
⊢ LE.le (α := MeasurableSpace ((a : ι) → α a)) (MeasurableSpace.pi (X := α))
    (OuterMeasure.caratheodory (OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure))
have refine : ∀ (i : ι),
  LE.le (α := MeasurableSpace ((a : ι) → α a)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst_1 i))
    (OuterMeasure.caratheodory (OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure))
Tactic: refine iSup_le ?_
-- 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)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ MeasurableSet (α := (a : ι) → α a) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)
have hs₁ : ∀ (t : Set ((a : ι) → α a)),
  piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) +
      piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) ≤
    piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) t
Tactic: apply boundedBy_caratheodory
-- 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)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) +
      piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) ≤
    piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) t
have hs₁ : HAdd.hAdd (α := ℝ≥0∞)
    (∏ x : ι,
      ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
    (∏ x : ι,
      ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
        (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
  ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)
Tactic: simp_rw [piPremeasure]
-- 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)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
    ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)
have hs₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
      ℝ≥0∞)
    (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
      ℝ≥0∞) ≤
  ((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' t)
Tactic: refine Finset.prod_add_prod_le' (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)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
hs₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞) ≤
    ((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' t)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
    ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)
have hs₂ : ∀ (j : ι),
  Membership.mem (γ := Finset ι) Finset.univ j →
    j ≠ i →
      LE.le (α := ℝ≥0∞)
        (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞)
            (eval (β := α) j '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
          ℝ≥0∞)
        (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)
Tactic: refine Finset.prod_add_prod_le' (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)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
hs₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞) ≤
    ((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' t)
hs₂ :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      j ≠ i →
        LE.le (α := ℝ≥0∞)
          (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞)
              (eval (β := α) j '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
            ℝ≥0∞)
          (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
    ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)
have hs₃ : ∀ (j : ι),
  Membership.mem (γ := Finset ι) Finset.univ j →
    j ≠ i →
      LE.le (α := ℝ≥0∞)
        (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞)
            (eval (β := α) j '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
          ℝ≥0∞)
        (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)
Tactic: refine Finset.prod_add_prod_le' (Finset.mem_univ i) ?_ ?_ ?_