awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
⊢ iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (j : κ i) → Ω i j)) (β := fun (p : (i : ι) × κ i) ↦
    𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (fun (p : (i : ι) × κ i) (ω : (i : ι) → (j : κ i) → Ω i j) ↦
      X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))
        (ω (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (infinitePi (X := fun (i : ι) ↦ (j : κ i) → Ω i j) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
have refine_1 : iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x)
  (fun (i : ι) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (x : κ i) ↦
    (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i x ω)
  (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
Tactic: refine iIndepFun_uncurry (P := infinitePi (fun i ↦ infinitePi (μ i)))
    (X := fun i j ω ↦ X i j (ω i j)) (by fun_prop) ?_ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
refine_1 :
  iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := fun (i : ι) ↦
    (x : κ i) → 𝓧 i x)
    (fun (i : ι) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (x : κ i) ↦
      (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i x ω)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
⊢ iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (j : κ i) → Ω i j)) (β := fun (p : (i : ι) × κ i) ↦
    𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (fun (p : (i : ι) × κ i) (ω : (i : ι) → (j : κ i) → Ω i j) ↦
      X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))
        (ω (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (infinitePi (X := fun (i : ι) ↦ (j : κ i) → Ω i j) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
have refine_2 : ∀ (i : ι),
  iIndepFun (Ω := (i : ι) → (i_1 : κ i) → Ω i i_1) (_mΩ :=
    MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := 𝓧 i)
    ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
Tactic: refine iIndepFun_uncurry (P := infinitePi (fun i ↦ infinitePi (μ i)))
    (X := fun i j ω ↦ X i j (ω i j)) (by fun_prop) ?_ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ iIndepFun (Ω := (i : ι) → (i_1 : κ i) → Ω i i_1) (_mΩ :=
    MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := 𝓧 i)
    ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
have refine_2 : Eq (α := Measure ((i_1 : κ i) → 𝓧 i i_1))
  (map
    (fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i_1 : κ i) ↦
      (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1 ω)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
  (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
    map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
      (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
Tactic: rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ Eq (α := Measure ((i_1 : κ i) → 𝓧 i i_1))
    (map
      (fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i_1 : κ i) ↦
        (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1 ω)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2 : Eq (α := Measure ((j : κ i) → 𝓧 i j))
  (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
    ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
      X i j (ω i j))
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
  (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
    map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
      (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
Tactic: change map ((fun f ↦ f i) ∘ (fun ω i j ↦ X i j (ω i j)))
    (infinitePi fun i ↦ infinitePi (μ i)) = _
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ Eq (α := Measure ((j : κ i) → 𝓧 i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
        X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2 : Eq (α := Measure ((j : κ i) → 𝓧 i j)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) (μ i i_1))
  (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
    map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
      (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
Tactic: rw [← map_map (by fun_prop) (by fun_prop),
    infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i))
      (f := fun i f j ↦ X i j (f j)), @infinitePi_map_eval .., infinitePi_map_pi]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
refine_2 :
  Eq (α := Measure ((j : κ i) → 𝓧 i j)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) (μ i i_1))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
⊢ Eq (α := Measure ((j : κ i) → 𝓧 i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
        X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2₁ : ∀ (i_1 : κ i), Measurable (X i i_1)
Tactic: rw [← map_map (by fun_prop) (by fun_prop),
    infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i))
      (f := fun i f j ↦ X i j (f j)), @infinitePi_map_eval .., infinitePi_map_pi]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
refine_2 :
  Eq (α := Measure ((j : κ i) → 𝓧 i j)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) (μ i i_1))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
refine_2₁ : ∀ (i_1 : κ i), Measurable (X i i_1)
⊢ Eq (α := Measure ((j : κ i) → 𝓧 i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
        X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have rw : ∀ (i : ι),
  IsProbabilityMeasure (α := (j : κ i) → 𝓧 i j) (m0 := MeasurableSpace.pi (X := 𝓧 i))
    (map (fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)) (infinitePi (X := Ω i) (μ i)))
Tactic: rw [← map_map (by fun_prop) (by fun_prop),
    infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i))
      (f := fun i f j ↦ X i j (f j)), @infinitePi_map_eval .., infinitePi_map_pi]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
refine_2 :
  Eq (α := Measure ((j : κ i) → 𝓧 i j)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) (μ i i_1))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
refine_2₁ : ∀ (i_1 : κ i), Measurable (X i i_1)
rw :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (j : κ i) → 𝓧 i j) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)) (infinitePi (X := Ω i) (μ i)))
⊢ Eq (α := Measure ((j : κ i) → 𝓧 i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
        X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2₂ : ∀ (i : ι), Measurable (β := (j : κ i) → 𝓧 i j) fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)
Tactic: rw [← map_map (by fun_prop) (by fun_prop),
    infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i))
      (f := fun i f j ↦ X i j (f j)), @infinitePi_map_eval .., infinitePi_map_pi]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ Eq (α := Measure ((j : κ i) → 𝓧 i j)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) (μ i i_1))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2 : ∀ (j : κ i),
  Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i j)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
Tactic: congrm infinitePi fun j ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i j)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2 : Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
  (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
    (Function.comp (β := (i : ι) → (j : κ i) → 𝓧 i j)
      ((fun (f : (j : κ i) → 𝓧 i j) ↦ f j) ∘ fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i)
      fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦ X i j (ω i j))
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
Tactic: change _ = map (((fun f ↦ f j) ∘ (fun f ↦ f i)) ∘ (fun ω i j ↦ X i j (ω i j)))
      (infinitePi fun i ↦ infinitePi (μ i))
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      (Function.comp (β := (i : ι) → (j : κ i) → 𝓧 i j)
        ((fun (f : (j : κ i) → 𝓧 i j) ↦ f j) ∘ fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i)
        fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦ X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have rw : ∀ (i_1 : κ i), IsProbabilityMeasure (m0 := m𝓧 i i_1) (map (X i i_1) (μ i i_1))
Tactic: rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j)
        (μ := fun i ↦ infinitePi (μ i)) (f := fun i f j ↦ X i j (f j)),
        ← map_map (by fun_prop) (by fun_prop),
        @infinitePi_map_eval .., infinitePi_map_pi, @infinitePi_map_eval ..]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
rw : ∀ (i_1 : κ i), IsProbabilityMeasure (m0 := m𝓧 i i_1) (map (X i i_1) (μ i i_1))
⊢ Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      (Function.comp (β := (i : ι) → (j : κ i) → 𝓧 i j)
        ((fun (f : (j : κ i) → 𝓧 i j) ↦ f j) ∘ fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i)
        fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦ X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2 : ∀ (i_1 : κ i), Measurable (X i i_1)
Tactic: rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j)
        (μ := fun i ↦ infinitePi (μ i)) (f := fun i f j ↦ X i j (f j)),
        ← map_map (by fun_prop) (by fun_prop),
        @infinitePi_map_eval .., infinitePi_map_pi, @infinitePi_map_eval ..]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
rw : ∀ (i_1 : κ i), IsProbabilityMeasure (m0 := m𝓧 i i_1) (map (X i i_1) (μ i i_1))
refine_2 : ∀ (i_1 : κ i), Measurable (X i i_1)
⊢ Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      (Function.comp (β := (i : ι) → (j : κ i) → 𝓧 i j)
        ((fun (f : (j : κ i) → 𝓧 i j) ↦ f j) ∘ fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i)
        fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦ X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have rw₁ : ∀ (i : ι),
  IsProbabilityMeasure (α := (j : κ i) → 𝓧 i j) (m0 := MeasurableSpace.pi (X := 𝓧 i))
    (map (fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)) (infinitePi (X := Ω i) (μ i)))
Tactic: rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j)
        (μ := fun i ↦ infinitePi (μ i)) (f := fun i f j ↦ X i j (f j)),
        ← map_map (by fun_prop) (by fun_prop),
        @infinitePi_map_eval .., infinitePi_map_pi, @infinitePi_map_eval ..]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
rw : ∀ (i_1 : κ i), IsProbabilityMeasure (m0 := m𝓧 i i_1) (map (X i i_1) (μ i i_1))
refine_2 : ∀ (i_1 : κ i), Measurable (X i i_1)
rw₁ :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (j : κ i) → 𝓧 i j) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)) (infinitePi (X := Ω i) (μ i)))
⊢ Eq (α := Measure (𝓧 i j)) (map (X i j) (μ i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      (Function.comp (β := (i : ι) → (j : κ i) → 𝓧 i j)
        ((fun (f : (j : κ i) → 𝓧 i j) ↦ f j) ∘ fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i)
        fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦ X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
have refine_2₁ : ∀ (i : ι), Measurable (β := (j : κ i) → 𝓧 i j) fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)
Tactic: rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j)
        (μ := fun i ↦ infinitePi (μ i)) (f := fun i f j ↦ X i j (f j)),
        ← map_map (by fun_prop) (by fun_prop),
        @infinitePi_map_eval .., infinitePi_map_pi, @infinitePi_map_eval ..]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_meas_f : Measurable f
⊢ ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have revert : ∀ {f : Ω → ℝ≥0∞} (h_meas_f : Measurable f),
  ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
Tactic: revert f
Cleared hypotheses: f, h_meas_f
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
⊢ ∀ {f : Ω → ℝ≥0∞} (h_meas_f : Measurable f),
    ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
Tactic: have h_mul_indicator : ∀ g, Measurable g → Measurable fun a => g a * T.indicator (fun _ => c) a :=
    fun g h_mg => h_mg.mul (measurable_const.indicator h_meas_T)