awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i))
    (Measure.pi (α := E) μ)
have succ : @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
  ((fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i)) ∘
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j))
  (Measure.prod (μ 0)
    (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
Tactic: rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
    ((fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i)) ∘
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
        (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j))
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
have succ : @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
  ((fun (x : (i : Fin (n + 1)) → E i) ↦ f 0 (x 0) * ∏ i : Fin n, f i.succ (x i.succ)) ∘
    (⇑{
          toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦
            Fin.cons (α := E) f.1 fun (j : Fin n) ↦ cast sorry (f.2 j),
          invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := sorry,
          right_inv := sorry } :
      (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i))
  (Measure.prod (μ 0)
    (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
Tactic: simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
        Fin.prod_univ_succ, Fin.insertNth_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
    ((fun (x : (i : Fin (n + 1)) → E i) ↦ f 0 (x 0) * ∏ i : Fin n, f i.succ (x i.succ)) ∘
      (⇑{
            toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦
              Fin.cons (α := E) f.1 fun (j : Fin n) ↦ cast ⋯ (f.2 j),
            invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
            right_inv := ⋯ } :
        (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i))
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
have succ : @Integrable.{u_1, u_3} 𝕜 _ _ _ Prod.instMeasurableSpace
  (fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
    f 0
        (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
              invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := sorry,
              right_inv := sorry : E 0 × ((i : Fin n) → E i.succ) ≃ ((i : Fin (n + 1)) → E i) } :
            (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
          x 0) *
      ∏ i : Fin n,
        f i.succ
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := sorry,
                right_inv := sorry } :
              (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
            x i.succ))
  (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))
Tactic: simp only [Fin.zero_succAbove, cast_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ _ Prod.instMeasurableSpace
    (fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
      f 0
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                right_inv := ⋯ : E 0 × ((i : Fin n) → E i.succ) ≃ ((i : Fin (n + 1)) → E i) } :
              (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
            x 0) *
        ∏ i : Fin n,
          f i.succ
            (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                  invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                  right_inv := ⋯ } :
                (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
              x i.succ))
    (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))
have this₁ : @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (j : Fin n) ↦ E j.succ))
  (fun (x : (j : Fin n) → E j.succ) ↦ ∏ j : Fin n, f j.succ (x j))
  (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (i : Fin n) ↦ μ i.succ)
Tactic: have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j))
          (Measure.pi (fun i ↦ μ i.succ)) :=
        n_ih (fun i ↦ hf _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
E : Fin n → Type u_3
mE : (i : Fin n) → MeasurableSpace (E i)
μ : (i : Fin n) → Measure (E i)
inst_1 : ∀ (i : Fin n), SigmaFinite (μ i)
f : (i : Fin n) → E i → 𝕜
hf : ∀ (i : Fin n), Integrable (f i) (μ i)
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
have zero : ∀ {E : Fin 0 → Type u_3} {mE : (i : Fin 0) → MeasurableSpace (E i)} {μ : (i : Fin 0) → Measure (E i)}
  [∀ (i : Fin 0), SigmaFinite (μ i)] {f : (i : Fin 0) → E i → 𝕜} (hf : ∀ (i : Fin 0), Integrable (f i) (μ i)),
  Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin 0) → E i) ↦ ∏ i : Fin 0, f i (x i)) (Measure.pi (α := E) μ)
Tactic: induction n with
  | zero => simp only [Finset.univ_eq_empty, Finset.prod_empty, isFiniteMeasure_iff,
      integrable_const_iff, pi_empty_univ, ENNReal.one_lt_top, or_true]
  | succ n n_ih =>
      have := ((measurePreserving_piFinSuccAbove μ 0).symm)
      rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
      simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
        Fin.prod_univ_succ, Fin.insertNth_zero]
      simp only [Fin.zero_succAbove, cast_eq, Function.comp_def]
      have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j))
          (Measure.pi (fun i ↦ μ i.succ)) :=
        n_ih (fun i ↦ hf _)
      exact Integrable.mul_prod (hf 0) this
Cleared hypotheses: n, E, mE, μ, inst_1, f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
E : Fin n → Type u_3
mE : (i : Fin n) → MeasurableSpace (E i)
μ : (i : Fin n) → Measure (E i)
inst_1 : ∀ (i : Fin n), SigmaFinite (μ i)
f : (i : Fin n) → E i → 𝕜
hf : ∀ (i : Fin n), Integrable (f i) (μ i)
zero :
  ∀ {E : Fin 0 → Type u_3} {mE : (i : Fin 0) → MeasurableSpace (E i)} {μ : (i : Fin 0) → Measure (E i)}
    [∀ (i : Fin 0), SigmaFinite (μ i)] {f : (i : Fin 0) → E i → 𝕜} (hf : ∀ (i : Fin 0), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin 0) → E i) ↦ ∏ i : Fin 0, f i (x i)) (Measure.pi (α := E) μ)
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
have succ : ∀ (n : ℕ)
  (n_ih :
    ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
      [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
      Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ))
  {E : Fin (n + 1) → Type u_3} {mE : (i : Fin (n + 1)) → MeasurableSpace (E i)} {μ : (i : Fin (n + 1)) → Measure (E i)}
  [∀ (i : Fin (n + 1)), SigmaFinite (μ i)] {f : (i : Fin (n + 1)) → E i → 𝕜}
  (hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)),
  Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i))
    (Measure.pi (α := E) μ)
Tactic: induction n with
  | zero => simp only [Finset.univ_eq_empty, Finset.prod_empty, isFiniteMeasure_iff,
      integrable_const_iff, pi_empty_univ, ENNReal.one_lt_top, or_true]
  | succ n n_ih =>
      have := ((measurePreserving_piFinSuccAbove μ 0).symm)
      rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
      simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
        Fin.prod_univ_succ, Fin.insertNth_zero]
      simp only [Fin.zero_succAbove, cast_eq, Function.comp_def]
      have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j))
          (Measure.pi (fun i ↦ μ i.succ)) :=
        n_ih (fun i ↦ hf _)
      exact Integrable.mul_prod (hf 0) this
Cleared hypotheses: n, E, mE, μ, inst_1, f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
⊢ Integrable (ε := 𝕜) (fun (x : (i : ι) → E i) ↦ ∏ i : ι, f i (x i)) (Measure.pi (α := E) μ)
have simp_rw : @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
  (fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
    ∏ x_1 : Fin (card ι), f ((e : (a : Fin (card ι)) → ι) x_1) (x x_1))
  (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
    μ ((e : (a : Fin (card ι)) → ι) i'))
Tactic: simp_rw [← (measurePreserving_piCongrLeft _ e).integrable_comp_emb
    (MeasurableEquiv.measurableEmbedding _),
    ← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def,
    Equiv.piCongrLeft_apply_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
    ∏ i : Fin (n + 1),
      f i
        ((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0) :
            (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
          x i))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
Tactic: rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0)
        (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
      fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
      ∏ i : Fin (n + 1),
        f i
          ((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0) :
              (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
            x i))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
have simp_rw : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
    ∏ x_1 : Fin (n + 1),
      f x_1
        ((Fin.insertNthEquiv E 0 : (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i) x x_1))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
Tactic: simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
simp_rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0)
        (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
      fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
      ∏ x_1 : Fin (n + 1),
        f x_1
          ((Fin.insertNthEquiv E 0 : (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i) x
            x_1))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0)
        (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
      fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
      ∏ i : Fin (n + 1),
        f i
          ((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0) :
              (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
            x i))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
have simp_rw₁ : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
    ∏ x_1 : Fin (n + 1),
      f x_1
        (({ toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦ Fin.insertNth (α := E) 0 f.1 f.2,
              invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := sorry,
              right_inv := sorry } :
            (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i)
          x x_1))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
Tactic: simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)) =
    HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ)
have rw : (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)) =
  HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : Fin n) ↦ E i.succ))
      (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ) fun (x : (i : Fin n) → E i.succ) ↦
      ∏ i : Fin n, f i.succ (x i))
Tactic: rw [← n_ih, ← integral_prod_mul]