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)
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)
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∞)
⊢ 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:
congrm ?_ * ?_
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ 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:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ 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:
Finset.prod_congr rfl fun j hj ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  ∀ (j : ι) (hj : j ∈ Finset.erase Finset.univ i),
    Eq (α := ℝ≥0∞)
      ((μ j : (a : Set (α j)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s j) : ℝ≥0∞)
      ((μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ 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:
refine Finset.prod_congr rfl fun j hj ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
j : ι
hj : j ∈ Finset.erase Finset.univ i
⊢ Eq (α := ℝ≥0∞)
    ((μ j : (a : Set (α j)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s j) : ℝ≥0∞)
    ((μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp [Function.update, Finset.ne_of_mem_erase hj]

Premises used: Function.update, Finset.ne_of_mem_erase
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
⊢ ∀ (i : ι), SigmaFinite (μ i)

Tactic:
have (i : ι) := (hμ i).of_map _ (hf i)
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ))
    (Measure.pi (α := Y) fun (i : ι) ↦ map (f i) (μ i))

Tactic:
(pi_eq fun s hs ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
refine :
  ∀ (s : (i : ι) → Set (Y i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
    Eq (α := ℝ≥0∞)
      ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
          (Set.pi (α := Y) univ s) :
        ℝ≥0∞)
      (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ))
    (Measure.pi (α := Y) fun (i : ι) ↦ map (f i) (μ i))

Tactic:
refine (pi_eq fun s hs ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ : AEMeasurable (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ)
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        (Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [map_apply_of_aemeasurable _ (.univ_pi hs)]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, MeasurableSet.univ_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ AEMeasurable (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ)

Tactic:
aemeasurable_pi_lambda _
      fun i ↦ (hf i).comp_quasiMeasurePreserving (quasiMeasurePreserving_eval _ i)

Premises used: aemeasurable_pi_lambda, AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_eval
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ AEMeasurable (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ)

Tactic:
exact aemeasurable_pi_lambda _
      fun i ↦ (hf i).comp_quasiMeasurePreserving (quasiMeasurePreserving_eval _ i)

Premises used: aemeasurable_pi_lambda, AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_eval
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
h :
  ∀ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
        x ↔
      Membership.mem (γ := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i) x
⊢ Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
x : (i : ι) → X i
⊢ Membership.mem (γ := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
      x ↔
    Membership.mem (γ := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)

Tactic:
have : (fun (x : Π i, X i) i ↦ f i (x i)) ⁻¹' (Set.univ.pi s) =
      Set.univ.pi (fun i ↦ (f i) ⁻¹' (s i)) := by ext x; simp
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
rw :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [this, pi_pi]

Premises used: MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
e_f :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
      (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i))

Tactic:
congr with i
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
i : ι
e_f e_f₁ :
  Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
    (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [map_apply_of_aemeasurable (hf i) (hs i)]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ MeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)

Tactic:
⟨measurable_pi_apply i, ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
refine : map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
⊢ MeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)

Tactic:
refine ⟨measurable_pi_apply i, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
rw : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i

Tactic:
rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]

Premises used: Finset.prod_eq_one, MeasureTheory.Measure.pi_map_eval, one_smul
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
fun _ _ ↦ measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact fun _ _ ↦ measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
rw : HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) = μ i
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 (μ i) = μ i
rw₂ : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw₃ : μ i = μ i
rw₄ : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw₅ : μ i = μ i
rw₆ rw₇ : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i

Tactic:
classical
  rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
  exact fun _ _ ↦ measure_univ

Premises used: Finset.prod_eq_one, MeasureTheory.Measure.pi_map_eval, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
inst_3 : NoAtoms (μ i)
x : α i
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) {f : (i : ι) → α i | f i = x} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
show Measure.pi μ (eval i ⁻¹' {x}) = 0 from pi_eval_preimage_null _ (measure_singleton x)

Premises used: MeasureTheory.Measure.pi_eval_preimage_null, Set.Mem, setOf, MeasureTheory.NoAtoms.measure_singleton, Set.preimage, Set.singleton
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
inst_3 : NoAtoms (μ i)
x : α i
⊢ ∀ᵐ (y : (i : ι) → α i) ∂Measure.pi (α := α) μ, y i ≠ x

Tactic:
compl_mem_ae_iff.2 (pi_hyperplane μ i x)

Premises used: Iff.mpr, MeasureTheory.Measure.pi_hyperplane, Set.Mem, Filter.Eventually, setOf, MeasureTheory.compl_mem_ae_iff
-- 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)
⊢ (Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) =
    Measure.pi (α := α) fun (i : ι) ↦ (μ i).restrict (s i)

Tactic:
(pi_eq fun _ h ↦ ?_).symm

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

Tactic:
refine (pi_eq fun _ h ↦ ?_).symm

Premises used: 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 x : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (x i)
simp_rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x ∩ Set.pi (α := α) univ fun (i : ι) ↦ s i) :
      ℝ≥0∞)
    (∏ x_1 : ι, (μ x_1 : (a : Set (α x_1)) → ℝ≥0∞) (x x_1 ∩ s x_1) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ fun (i : ι) ↦ x i ∩ s i) : ℝ≥0∞)
    (∏ x_1 : ι, (μ x_1 : (a : Set (α x_1)) → ℝ≥0∞) (x x_1 ∩ s x_1) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := α) μ).restrict (Set.pi (α := α) univ fun (i : ι) ↦ s i) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ x) :
      ℝ≥0∞)
    (∏ i : ι, ((μ i).restrict (s i) : (a : Set (α i)) → ℝ≥0∞) (x i) : ℝ≥0∞)

Tactic:
simp_rw [restrict_apply (MeasurableSet.univ_pi h), restrict_apply (h _),
    ← Set.pi_inter_distrib, pi_pi]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.pi_pi, Set.pi_inter_distrib, MeasurableSet.univ_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ Tendsto (eval (β := α) i) (ae (Measure.pi (α := α) μ)) (ae (μ i))

Tactic:
fun _ hs =>
  pi_eval_preimage_null μ hs

Premises used: MeasureTheory.Measure.pi_eval_preimage_null, Set.Mem, setOf, Set.preimage, Filter.Tendsto, Not
-- 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)
⊢ ae (Measure.pi (α := α) μ) ≤ Filter.pi (α := α) fun (i : ι) ↦ ae (μ i)

Tactic:
le_iInf fun _ => tendsto_eval_ae_ae.le_comap

Premises used: Filter.Tendsto.le_comap, Set.Mem, le_iInf, MeasureTheory.Measure.tendsto_eval_ae_ae
-- 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)
β : ι → Type u_4
f f' : (i : ι) → α i → β i
h : ∀ (i : ι), f i =ᶠ[ae (μ i)] f' i
⊢ (ae (Measure.pi (α := α) μ)).EventuallyEq (β := (i : ι) → β i) (fun (x : (i : ι) → α i) (i : ι) ↦ f i (x i))
    fun (x : (i : ι) → α i) (i : ι) ↦ f' i (x i)

Tactic:
(eventually_all.2 fun i => tendsto_eval_ae_ae.eventually (h i)).mono fun _ hx => funext hx

Premises used: Iff.mpr, Filter.EventuallyEq, Filter.eventually_all, Filter.Eventually.mono, funext, Filter.Tendsto.eventually, MeasureTheory.Measure.tendsto_eval_ae_ae
-- 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)
β : ι → Type u_4
inst_3 : (i : ι) → Preorder (β i)
f f' : (i : ι) → α i → β i
h : ∀ (i : ι), f i ≤ᶠ[ae (μ i)] f' i
⊢ (ae (Measure.pi (α := α) μ)).EventuallyLE (β := (i : ι) → β i) (fun (x : (i : ι) → α i) (i : ι) ↦ f i (x i))
    fun (x : (i : ι) → α i) (i : ι) ↦ f' i (x i)

Tactic:
(eventually_all.2 fun i => tendsto_eval_ae_ae.eventually (h i)).mono fun _ hx => hx

Premises used: Iff.mpr, Filter.eventually_all, Filter.Eventually.mono, Filter.Tendsto.eventually, MeasureTheory.Measure.tendsto_eval_ae_ae, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
I : Set ι
s t : (i : ι) → Set (α i)
h : ∀ i ∈ I, s i ≤ᶠ[ae (μ i)] t i
⊢ I.pi (α := α) s ≤ᶠ[ae (Measure.pi (α := α) μ)] I.pi (α := α) t

Tactic:
((eventually_all_finite I.toFinite).2 fun i hi => tendsto_eval_ae_ae.eventually (h i hi)).mono
    fun _ hst hx i hi => hst i hi <| hx i hi

Premises used: Iff.mpr, Filter.Eventually.mono, Set.toFinite, Filter.eventually_all_finite, Filter.Tendsto.eventually, MeasureTheory.Measure.tendsto_eval_ae_ae, Filter.EventuallyLE