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)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
refine_2 : (pi' (α := α) μ).toOuterMeasure ≤ OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure
⊢ 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:
suffices (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i => (μ i).toOuterMeasure by exact 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)
this : Encodable ι
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∞)
⊢ (pi' (α := α) μ).toOuterMeasure ≤ OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure

Tactic:
rw [OuterMeasure.le_pi]

Premises used: MeasureTheory.OuterMeasure.le_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)
this : Encodable ι
s : (i : ι) → Set (α i)
refine_2 :
  (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∞)
⊢ (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:
_
-- 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)
this : Encodable ι
s : (i : ι) → Set (α i)
h : (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:
(pi'_pi μ s).le

Premises used: MeasureTheory.Measure.pi'_pi, Eq.le
-- 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)
this : Encodable ι
s : (i : ι) → Set (α i)
h : (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:
exact (pi'_pi μ s).le

Premises used: MeasureTheory.Measure.pi'_pi, Eq.le
-- 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)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
⊢ ∀ (i : ι), SigmaFinite (μ i)

Tactic:
haveI := fun i => (hμ i).sigmaFinite
-- 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)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this : ∀ (i : ι), SigmaFinite (μ i)
haveI :
  (this : Encodable ι) →
    (Measure.pi (α := α) μ).FiniteSpanningSetsIn (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)

Tactic:
haveI := Fintype.toEncodable ι
-- 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)
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))
      ∞
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
⊢ (Measure.pi (α := α) μ).FiniteSpanningSetsIn (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 => ?_, ?_⟩
-- 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)
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
⊢ (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:
mem_image_of_mem _ fun i _ => (hμ i).set_mem _

Premises used: Inhabited.default, Set.Mem, Option.getD, Set.mem_image_of_mem, Encodable.decode, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- 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)
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
⊢ (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 mem_image_of_mem _ fun i _ => (hμ i).set_mem _
-- 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)
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
⊢ LE.le (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (i : ι) ↦ (hμ i).set (C := C i) (e n i)) :
      ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (i : ι) ↦ toMeasurable (μ i) ((hμ i).set (C := C i) (e n i))) :
      ℝ≥0∞)

Tactic:
measure_mono (pi_mono fun i _ => subset_toMeasurable _ _)

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.set, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_mono, Set.pi_mono
-- 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)
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
⊢ Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (i : ι) ↦ toMeasurable (μ i) ((hμ i).set (C := C i) (e n i))) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (toMeasurable (μ i) ((hμ i).set (C := C i) (e n i))) : ℝ≥0∞)

Tactic:
(pi_pi_aux μ _ fun i => measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.Measure.pi_pi_aux, MeasureTheory.Measure.FiniteSpanningSetsIn.set, MeasureTheory.measurableSet_toMeasurable
-- 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)
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
⊢ 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:
simp only [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- 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)
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∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) ((hμ i).set (C := C i) (e n i))) ∞

Tactic:
ENNReal.prod_lt_top fun i _ => (hμ i).finite _

Premises used: ENNReal.prod_lt_top, MeasureTheory.Measure.FiniteSpanningSetsIn.finite
-- 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)
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
μ₁ :
  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)))
⊢ 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:
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 _

Premises used: ENNReal.prod_lt_top, MeasureTheory.Measure.pi_pi_aux, Set.univ, MeasureTheory.Measure.FiniteSpanningSetsIn.set, MeasureTheory.subset_toMeasurable, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.measure_mono, MeasureTheory.Measure.pi, Set.pi, MeasureTheory.toMeasurable, Set.pi_mono, DFunLike.coe
-- 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)
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
refine_3₄ : Eq (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (a : ι) ↦ univ) 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

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]

Premises used: Inhabited.default, Set.univ, MeasureTheory.Measure.FiniteSpanningSetsIn.set, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, Function.Surjective.iUnion_comp, Set.pi, Set.iUnion_univ_pi, Set.pi_univ, Encodable.surjective_decode_getD
-- 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)
C : (i : ι) → Set (Set (α i))
i : ι
⊢ MeasurableSpace (α i)

Tactic:
apply_assumption
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
rw : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [← hC]
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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

Tactic:
measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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

Tactic:
exact measurableSet_generateFrom hs

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 ∈ 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
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ = μν

Tactic:
(FiniteSpanningSetsIn.pi h3C).ext
      (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm (IsPiSystem.pi h2C) ?_

Premises used: generateFrom_eq_pi, IsPiSystem.pi, MeasureTheory.Measure.FiniteSpanningSetsIn.pi, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning, MeasureTheory.Measure.FiniteSpanningSetsIn.ext
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
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∞)
⊢ Measure.pi (α := α) μ = μν

Tactic:
refine
    (FiniteSpanningSetsIn.pi h3C).ext
      (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm (IsPiSystem.pi h2C) ?_

Premises used: generateFrom_eq_pi, IsPiSystem.pi, MeasureTheory.Measure.FiniteSpanningSetsIn.pi, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning, MeasureTheory.Measure.FiniteSpanningSetsIn.ext
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
⊢ ∀ (i : ι), s i ∈ C i

Tactic:
rw [mem_univ_pi] at hs

Premises used: Set.mem_univ_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
⊢ ∀ (i : ι), SigmaFinite (μ i)

Tactic:
haveI := fun i => (h3C i).sigmaFinite
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((μν : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)

Tactic:
simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs i)]

Premises used: MeasureTheory.Measure.pi_pi_aux
-- 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)
μ' : Measure ((i : ι) → α i)
h :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), MeasurableSet (s i)) →
      Eq (α := ℝ≥0∞) ((μ' : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Measure.pi (α := α) μ = μ'

Tactic:
pi_eq_generateFrom (fun _ => generateFrom_measurableSet) (fun _ => isPiSystem_measurableSet)
    (fun i => (μ i).toFiniteSpanningSetsIn) h

Premises used: MeasurableSpace.isPiSystem_measurableSet, MeasurableSpace.generateFrom_measurableSet, MeasureTheory.Measure.pi_eq_generateFrom, MeasureTheory.Measure.toFiniteSpanningSetsIn
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
⊢ pi' (α := α) μ = Measure.pi (α := α) μ

Tactic:
Eq.symm <| pi_eq fun s _ => pi'_pi μ s

Premises used: MeasureTheory.Measure.pi'_pi, MeasureTheory.Measure.pi_eq, Eq.symm
-- 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)
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∞)
⊢ 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 ι