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)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
h : 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∞)
have hs₁ : t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s ⊆ t
Tactic: gcongr
-- 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)
j : ι
h : 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∞)
have hs₁ : t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s ⊆ t
Tactic: gcongr
-- 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)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (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∞)
have refine_1 : LE.le (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine le_antisymm ?_ ?_
-- 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)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
refine_1 :
  LE.le (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
Tactic: refine le_antisymm ?_ ?_
-- 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)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ LE.le (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞)
  ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      (Set.pi (α := α) univ s) :
    ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs 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)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
have refine_2 : ∀ (this : Encodable ι),
  LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
Tactic: haveI : Encodable ι := Fintype.toEncodable ι
-- 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)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
  ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      (Set.pi (α := α) univ s) :
    ℝ≥0∞)
Tactic: simp_rw [← pi'_pi μ s, Measure.pi,
      toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs 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)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ LE.le (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
have refine_2 : (pi' (α := α) μ).toOuterMeasure ≤ OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure
Tactic: suffices (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i => (μ i).toOuterMeasure by exact 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)
this : Encodable ι
⊢ (pi' (α := α) μ).toOuterMeasure ≤ OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure
have refine_2 : ∀ (s : (i : ι) → Set (α i)),
  (Set.pi (α := α) univ s).Nonempty →
    LE.le (α := ℝ≥0∞)
      (((pi' (α := α) μ).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
      (∏ i : ι, ((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [OuterMeasure.le_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
⊢ (Measure.pi (α := α) μ).FiniteSpanningSetsIn (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have this : ∀ (i : ι), SigmaFinite (μ i)
Tactic: haveI := fun i => (hμ i).sigmaFinite
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ (Measure.pi (α := α) μ).FiniteSpanningSetsIn (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have haveI : (this : Encodable ι) →
  (Measure.pi (α := α) μ).FiniteSpanningSetsIn (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
Tactic: haveI := Fintype.toEncodable ι
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ (Measure.pi (α := α) μ).FiniteSpanningSetsIn (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have refine_1 : ∀ (n : ℕ),
  (fun (n : ℕ) ↦
        (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
          Set ((i : ι) → α i)))
      n ∈
    Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
Tactic: refine ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).getD default i),
    fun n => ?_, fun n => ?_, ?_⟩
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
refine_1 :
  ∀ (n : ℕ),
    (fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        n ∈
      Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
⊢ (Measure.pi (α := α) μ).FiniteSpanningSetsIn (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have refine_2 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      ((fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        n))
    ∞
Tactic: refine ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).getD default i),
    fun n => ?_, fun n => ?_, ?_⟩
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
refine_1 :
  ∀ (n : ℕ),
    (fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        n ∈
      Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
refine_2 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        ((fun (n : ℕ) ↦
            (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
              Set ((i : ι) → α i)))
          n))
      ∞
⊢ (Measure.pi (α := α) μ).FiniteSpanningSetsIn (Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
have refine_3 : Eq (α := Set ((i : ι) → α i))
  (⋃ (i : ℕ),
    (fun (n : ℕ) ↦
        (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
          Set ((i : ι) → α i)))
      i)
  univ
Tactic: refine ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).getD default i),
    fun n => ?_, fun n => ?_, ?_⟩
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
⊢ LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
      ((fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        n))
    ∞
have μ₁ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (toMeasurable (μ i) ((hμ i).set (C := C i) (e n i))))
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) ((hμ i).set (C := C i) (e n i)))
Tactic: calc
      Measure.pi μ (Set.pi univ fun i => (hμ i).set (e n i)) ≤
          Measure.pi μ (Set.pi univ fun i => toMeasurable (μ i) ((hμ i).set (e n i))) :=
        measure_mono (pi_mono fun i _ => subset_toMeasurable _ _)
      _ = ∏ i, μ i (toMeasurable (μ i) ((hμ i).set (e n i))) :=
        (pi_pi_aux μ _ fun i => measurableSet_toMeasurable _ _)
      _ = ∏ i, μ i ((hμ i).set (e n i)) := by simp only [measure_toMeasurable]
      _ < ∞ := ENNReal.prod_lt_top fun i _ => (hμ i).finite _
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
refine_3 refine_3₁ :
  Eq (α := Set ((i : ι) → α i))
    (⋃ (i : ℕ), Set.pi (α := α) univ fun (i_1 : ι) ↦ (hμ i_1).set (C := C i_1) (Option.getD (decode i) default i_1))
    univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (i : ℕ),
      (fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        i)
    univ
have refine_3₂ : Eq (α := Set ((i : ι) → α i)) (⋃ (y : ι → ℕ), Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (y i)) univ
Tactic: simp_rw [(surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x =>
        Set.pi univ fun i => (hμ i).set (x i),
      iUnion_univ_pi fun i => (hμ i).set, (hμ _).spanning, Set.pi_univ]
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
refine_3 refine_3₁ :
  Eq (α := Set ((i : ι) → α i))
    (⋃ (i : ℕ), Set.pi (α := α) univ fun (i_1 : ι) ↦ (hμ i_1).set (C := C i_1) (Option.getD (decode i) default i_1))
    univ
refine_3₂ :
  Eq (α := Set ((i : ι) → α i)) (⋃ (y : ι → ℕ), Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (y i)) univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (i : ℕ),
      (fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        i)
    univ
have refine_3₃ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ ⋃ (j : ℕ), (hμ a).set (C := C a) j) univ
Tactic: simp_rw [(surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x =>
        Set.pi univ fun i => (hμ i).set (x i),
      iUnion_univ_pi fun i => (hμ i).set, (hμ _).spanning, Set.pi_univ]
-- 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)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun (n : ℕ) ↦ Option.getD (decode n) default
refine_3 refine_3₁ :
  Eq (α := Set ((i : ι) → α i))
    (⋃ (i : ℕ), Set.pi (α := α) univ fun (i_1 : ι) ↦ (hμ i_1).set (C := C i_1) (Option.getD (decode i) default i_1))
    univ
refine_3₂ :
  Eq (α := Set ((i : ι) → α i)) (⋃ (y : ι → ℕ), Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (y i)) univ
refine_3₃ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ ⋃ (j : ℕ), (hμ a).set (C := C a) j) univ
⊢ Eq (α := Set ((i : ι) → α i))
    (⋃ (i : ℕ),
      (fun (n : ℕ) ↦
          (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (Option.getD (decode n) default i) :
            Set ((i : ι) → α i)))
        i)
    univ
have refine_3₄ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ univ) univ
Tactic: simp_rw [(surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x =>
        Set.pi univ fun i => (hμ i).set (x i),
      iUnion_univ_pi fun i => (hμ i).set, (hμ _).spanning, Set.pi_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)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst_1 i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), s i ∈ C i) →
      Eq (α := ℝ≥0∞) ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
s : Set (α i)
hs : s ∈ C i
⊢ MeasurableSet s
have rw : MeasurableSet s
Tactic: rw [← hC]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst_1 i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), s i ∈ C i) →
      Eq (α := ℝ≥0∞) ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Measure.pi (α := α) μ = μν
have h4C : ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s
Tactic: have h4C : ∀ (i) (s : Set (α i)), s ∈ C i → MeasurableSet s := by
    intro i s hs; rw [← hC]; exact measurableSet_generateFrom 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)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst_1 i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), s i ∈ C i) →
      Eq (α := ℝ≥0∞) ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
h4C : ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s
⊢ Measure.pi (α := α) μ = μν
have hC₁ : ∀ s ∈ Set.pi (α := α) univ '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C,
  Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine
    (FiniteSpanningSetsIn.pi h3C).ext
      (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm (IsPiSystem.pi h2C) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst_1 i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), s i ∈ C i) →
      Eq (α := ℝ≥0∞) ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
h4C : ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
have hs₁ : ∀ (i : ι), s i ∈ C i
Tactic: rw [mem_univ_pi] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst_1 i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), s i ∈ C i) →
      Eq (α := ℝ≥0∞) ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
h4C : ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), s i ∈ C i
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
have this : ∀ (i : ι), SigmaFinite (μ i)
Tactic: haveI := fun i => (h3C i).sigmaFinite
-- 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)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst_1 i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), s i ∈ C i) →
      Eq (α := ℝ≥0∞) ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
h4C : ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), s i ∈ C i
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs 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)
s : (i : ι) → Set (α i)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have haveI : ∀ (this : Encodable ι),
  Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: haveI : Encodable ι := Fintype.toEncodable ι
-- 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)
s : (i : ι) → Set (α i)
this : Encodable ι
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((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]
-- 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)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
Tactic: rw [← pi'_eq_pi, pi'_pi]