awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
I : Finset S
s : S → Set Ω
hs :
  ∀ i ∈ I,
    ∃ (s_1 : Finset (T i)) (t : (i_1 : T i) → Set (𝓧 i i_1)),
      (∀ (i_1 : T i), MeasurableSet (t i_1)) ∧
        (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑s_1 : Set (T i)).pi (α := 𝓧 i) t = s i
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ I, s i) : ENNReal)
      (∏ i ∈ I, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)
have inr : ∀ (J : (i : S) → Finset (T i)) (t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1))
  (ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1))
  (hs : ∀ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i) = s i),
  ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ I, s i) : ENNReal)
      (∏ i ∈ I, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)
Tactic: choose! J t ht hs using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i) = s i
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (⋂ i ∈ I, s i) : ENNReal)
      (∏ i ∈ I, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (s i) : ENNReal)
have inr : ∀ᵐ (a : α) ∂P,
  Eq (α := ENNReal)
    ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
        (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
      ENNReal)
    (∏ i ∈ I,
        (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
      ENNReal)
Tactic: simp_rw [Set.iInter₂_congr (fun i hi ↦ (hs i hi).symm),
    I.prod_congr rfl (fun i hi ↦ congrArg _ (hs i hi).symm)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i) = s i
⊢ Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
    (⋂ (i : ↥I),
      ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
        preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
          (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
          ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
            fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))
have h₁ : ∀ (x : Ω),
  Membership.mem (γ := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
      x ↔
    Membership.mem (γ := Set Ω)
      (⋂ (i : ↥I),
        ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
          preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
            (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
            ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
              fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i) = s i
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
        ENNReal)
      (∏ i ∈ I,
          (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
        ENNReal)
have this : Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
  (⋂ (i : ↥I),
    ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
      preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
        (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
        ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
          fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))
Tactic: have : (⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' .pi (J i) (t i)) =
      (⋂ i ∈ (.univ : Finset I), (fun ω (j : J i) ↦ X i j ω) ⁻¹'
        .pi (SetLike.coe Finset.univ) (fun j ↦ t i j)) := by
    ext; simp
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (hypothesis)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_4, u_3} (β := Measure Ω) (ae P) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
π : (i : S) → Set (Set Ω) :=
  fun (i : S) ↦
    {s : Set Ω |
      ∃ (t : Set ((i_1 : T i) → 𝓧 i i_1)),
        Membership.mem (γ := Set (Set ((i_1 : T i) → 𝓧 i i_1)))
            (squareCylinders (α := 𝓧 i) fun (j : T i) ↦ {s : Set (𝓧 i j) | MeasurableSet s}) t ∧
          (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen :
  ∀ (i : S),
    MeasurableSpace.comap (β := (j : T i) → 𝓧 i j) (fun (ω : Ω) (j : T i) ↦ X i j ω) (MeasurableSpace.pi (X := 𝓧 i)) =
      generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i) = s i
this :
  Eq.{u_3 + 1} (α := Set Ω) (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i))
    (⋂ (i : ↥I),
      ⋂ (_ : Membership.mem (γ := Finset ↥I) Finset.univ i),
        preimage (β := (j : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
          (fun (ω : Ω) (j : ↥(J (↑i : S))) ↦ X (↑i : S) (↑j : T (↑i : S)) ω)
          ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
            fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S))))
⊢ ∀ᵐ (a : α) ∂P,
    Eq (α := ENNReal)
      ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ I, (fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
        ENNReal)
      (∏ i ∈ I,
          (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (ω : Ω) (j : T i) ↦ X i j ω) ⁻¹' (↑(J i) : Set (T i)).pi (α := 𝓧 i) (t i)) :
        ENNReal)
have h' : ∀ (i : ↥I) (hi : Membership.mem (γ := Finset ↥I) Finset.univ i),
  MeasurableSet (α := (i_1 : ↥(J (↑i : S))) → 𝓧 (↑i : S) (↑i_1 : T (↑i : S)))
    ((↑Finset.univ : Set ↥(J (↑i : S))).pi (α := fun (j : ↥(J (↑i : S))) ↦ 𝓧 (↑i : S) (↑j : T (↑i : S)))
      fun (j : ↥(J (↑i : S))) ↦ t (↑i : S) (↑j : T (↑i : S)))
Tactic: have h' (i : I) (hi : i ∈ Finset.univ) :
      MeasurableSet <| (SetLike.coe Finset.univ).pi fun (j : J i) ↦ t i j :=
    .pi (Finset.countable_toSet _) (fun _ _ ↦ ht _ i.2 _)
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) κ P
have refine : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ AEMeasurable.mk (X i j) sorry ω) κ P
Tactic: refine process_congr ?_ (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk.symm)
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.Basic (goal)
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → (j : T i) → Type u_6
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (_m := mΩ) (X i j) ((⇑κ : (a : α) → Measure Ω) ∘ₘ P)
h :
  ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
    iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
      (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ X (↑i : S) (↑j : T (↑i : S)) ω) κ P
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ AEMeasurable.mk (X i j) ⋯ ω) κ P
have refine : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T (↑i : S))),
  iIndepFun (β := fun (i : ↥I) ↦ (j : ↥(J i)) → 𝓧 (↑i : S) (↑j : T (↑i : S)))
    (fun (i : ↥I) (ω : Ω) (j : ↥(J i)) ↦ AEMeasurable.mk (X (↑i : S) (↑j : T (↑i : S))) sorry ω) κ P
Tactic: refine iIndepFun_process (fun i j ↦ (hX i j).measurable_mk) fun I J ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
⊢ iIndepFun (β := fun (i : ℕ) ↦ E) (fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
have refine : ∀ (s : Finset ℕ),
  iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
Tactic: refine iIndepFun_iff_finset.2 fun s ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
s : Finset ℕ
⊢ iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
have inl : iIndepFun (β := fun (x : ↥∅) ↦ E)
  (Finset.restrict (π := fun (i : ℕ) ↦ Ω → E) ∅ fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
s : Finset ℕ
inl :
  iIndepFun (β := fun (x : ↥∅) ↦ E)
    (Finset.restrict (π := fun (i : ℕ) ↦ Ω → E) ∅ fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
⊢ iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
have inr : ∀ (hs : s.Nonempty),
  iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (hypothesis)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
⊢ iIndepFun (β := fun (x : ↥∅) ↦ E)
    (Finset.restrict (π := fun (i : ℕ) ↦ Ω → E) ∅ fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
have this : IsProbabilityMeasure P
Tactic: have := (hX 0 (fun _ ↦ t 0) (fun _ ↦ by grind)).isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
s : Finset ℕ
hs : s.Nonempty
g : (x : ↥s) → Fin (s.max' hs + 1) := fun (x : ↥s) ↦ ⟨(↑x : ℕ), ⋯⟩
⊢ iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
have inr : Function.Injective g
Tactic: refine iIndepFun.precomp (g := g) ?_ (hX (s.max' hs + 1) (fun m ↦ t m) ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
s : Finset ℕ
hs : s.Nonempty
g : (x : ↥s) → Fin (s.max' hs + 1) := fun (x : ↥s) ↦ ⟨(↑x : ℕ), ⋯⟩
inr : Function.Injective g
⊢ iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
have inr₁ : Monotone.{0, u_1} (β := T) fun (m : Fin (s.max' hs + 1 + 1)) ↦ t (↑m : ℕ)
Tactic: refine iIndepFun.precomp (g := g) ?_ (hX (s.max' hs + 1) (fun m ↦ t m) ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
h :
  ∀ (t : ℕ → T),
    Monotone t →
      EventuallyConst t atTop → iIndepFun (β := fun (i : ℕ) ↦ E) (fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : (k : ℕ) → T := fun (k : ℕ) ↦ t ⟨min n k, ⋯⟩
⊢ iIndepFun (β := fun (i : Fin n) ↦ E) (fun (i : Fin n) (ω : Ω) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P
have h₁ : ∀ (i : Fin n) (ω : Ω), (↑i.succ : ℕ) = min n ((↑i : ℕ) + 1)
Tactic: convert! (h t' ?_ ?_).precomp Fin.val_injective with i ω
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
h :
  ∀ (t : ℕ → T),
    Monotone t →
      EventuallyConst t atTop → iIndepFun (β := fun (i : ℕ) ↦ E) (fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : (k : ℕ) → T := fun (k : ℕ) ↦ t ⟨min n k, ⋯⟩
h₁ : ∀ (i : Fin n) (ω : Ω), (↑i.succ : ℕ) = min n ((↑i : ℕ) + 1)
⊢ iIndepFun (β := fun (i : Fin n) ↦ E) (fun (i : Fin n) (ω : Ω) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P
have h₂ : ∀ (i : Fin n) (ω : Ω), (↑i.castSucc : ℕ) = min n (↑i : ℕ)
Tactic: convert! (h t' ?_ ?_).precomp Fin.val_injective with i ω
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
h :
  ∀ (t : ℕ → T),
    Monotone t →
      EventuallyConst t atTop → iIndepFun (β := fun (i : ℕ) ↦ E) (fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : (k : ℕ) → T := fun (k : ℕ) ↦ t ⟨min n k, ⋯⟩
h₁ : ∀ (i : Fin n) (ω : Ω), (↑i.succ : ℕ) = min n ((↑i : ℕ) + 1)
h₂ : ∀ (i : Fin n) (ω : Ω), (↑i.castSucc : ℕ) = min n (↑i : ℕ)
⊢ iIndepFun (β := fun (i : Fin n) ↦ E) (fun (i : Fin n) (ω : Ω) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P
have convert_1 : Monotone t'
Tactic: convert! (h t' ?_ ?_).precomp Fin.val_injective with i ω
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : Sub E
h :
  ∀ (t : ℕ → T),
    Monotone t →
      EventuallyConst t atTop → iIndepFun (β := fun (i : ℕ) ↦ E) (fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : (k : ℕ) → T := fun (k : ℕ) ↦ t ⟨min n k, ⋯⟩
h₁ : ∀ (i : Fin n) (ω : Ω), (↑i.succ : ℕ) = min n ((↑i : ℕ) + 1)
h₂ : ∀ (i : Fin n) (ω : Ω), (↑i.castSucc : ℕ) = min n (↑i : ℕ)
convert_1 : Monotone t'
⊢ iIndepFun (β := fun (i : Fin n) ↦ E) (fun (i : Fin n) (ω : Ω) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P
have convert_2 : EventuallyConst t' atTop
Tactic: convert! (h t' ?_ ?_).precomp Fin.val_injective with i ω
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s ⟂ᵢ[P] X t - X s
have refine : X s - X r =ᶠ[ae P] X s
Tactic: refine (hX.indepFun_sub_sub hrs hst).congr ?_ .rfl
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s - X r =ᶠ[ae P] X s
have h₁ : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X r ω = 0) x} x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ (X s - X r) x = X s x) x} x}
    a
Tactic: filter_upwards [h] with ω hω using by simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic (goal)
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : Preorder T
inst_1 : MeasurableSpace E
inst_2 : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X r ω = 0) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ (X s - X r) x = X s x) x} x}
      a
⊢ X s - X r =ᶠ[ae P] X s
have h₂ : ∀ (a : Ω), X r a = 0 → (X s - X r) a = X s a
Tactic: filter_upwards [h] with ω hω using by simp [hω]