awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
⊢ Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ) ⊗ₘ κ a =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) (trajMeasure (X := X) μ₀ κ)
have rw : Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
  (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
    (Measure.map
      (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
            X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
        (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
      μ₀)
    (⇑(Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a) :
      (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
  (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
    (Measure.map
      (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
            X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
        (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
      μ₀)
    (⇑(map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) :
      (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
Tactic: rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp _ _ (by fun_prop),
    traj_map_frestrictLe, Measure.comp_assoc, Measure.map_comp _ _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
have e_f : ∀ (x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)),
  Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
Tactic: congr with x₀ : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
have e_f : Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
  (Measure.bind (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)))
    ((partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀)
    (⇑(Kernel.id ×ₖ κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
  ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
      (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    x₀)
Tactic: rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le']
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)
e_f :
  Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀)
      (⇑(Kernel.id ×ₖ κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀)
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
have e_f₁ : (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
  (map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
      (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    x₀
Tactic: rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le']
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)
e_f :
  Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀)
      (⇑(Kernel.id ×ₖ κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀)
e_f₁ :
  (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
    (map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
have e_f₂ : (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
  Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
    ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀)
Tactic: rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le']
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)
e_f :
  Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀)
      (⇑(Kernel.id ×ₖ κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀)
e_f₁ :
  (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
    (map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀
e_f₂ :
  (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
      ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀)
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
have e_f₃ : Eq.{u_1 + 1} (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
  (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
    ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
  (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
    ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀))
Tactic: rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le']
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
inst_3 : StandardBorelSpace.{u_1} (X (a + 1))
inst_4 : Nonempty.{u_1 + 1} (X (a + 1))
⊢ (ae (F := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
        (Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ))).EventuallyEq
    (β := Measure (X (a + 1)))
    (⇑(condDistrib (fun (x : (i : ℕ) → X i) ↦ x (a + 1)) (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ)) :
      (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1)))
    (⇑(κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1)))
have apply : Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) (trajMeasure (X := X) μ₀ κ) =
  Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ) ⊗ₘ κ a
Tactic: apply condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (by fun_prop) (by fun_prop)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Irreducible (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
⊢ ∃ (n : ℕ),
    GT.gt (α := ℝ≥0∞)
      ((((HPow.hPow (α := Kernel α α) Kernel.id n : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h : GT.gt (α := ℝ≥0∞)
  ((((HPow.hPow (α := Kernel α α) (β := ℕ) Kernel.id 1 : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: use 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Irreducible (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
⊢ GT.gt (α := ℝ≥0∞)
    ((((HPow.hPow (α := Kernel α α) (β := ℕ) Kernel.id 1 : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have ha : a ∈ s
Tactic: have ha : a ∈ s :=
      Subsingleton.mem_iff_nonempty.mpr
        <| MeasureTheory.nonempty_of_measure_ne_zero (μ := φ) (ne_of_lt hsp).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet.{u_1} (α := α) {a : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) a)}
have simp_rw : MeasurableSet.{u_1} (α := α) {a : α | @HasFiniteIntegral _ _ _ mβ f ((κ : (a : α) → Measure β) a)}
Tactic: simp_rw [Integrable, hf.aestronglyMeasurable, true_and]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet.{u_1} (α := α) {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)}
have simp_rw : MeasurableSet.{u_1} (α := α) {x : α | @HasFiniteIntegral _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)}
Tactic: simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos : ∀ (hE : CompleteSpace E),
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have neg : ∀ (hE : ¬CompleteSpace E),
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
Tactic: have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos : ∀ (n : ℕ), StronglyMeasurable (f' n)
Tactic: refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
pos : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos₁ : Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y)
Tactic: refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
⊢ StronglyMeasurable (f' n)
have pos : StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
Tactic: refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
have pos : StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
  ∑ x_1 ∈ (s n).range,
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
        (preimage (β := E) (⇑(s n) : (a : β) → E) {x_1}) •
      x_1
Tactic: simp_rw [SimpleFunc.integral_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s n) : (a : β) → E) {x_1}) •
        x_1
have pos : ∀ x ∈ (s n).range,
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x_2 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_2)
        (preimage (β := E) (⇑(s n) : (a : β) → E) {x}) •
      x
Tactic: refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_