awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), Measurable (X i)
hY : ∀ (j : T), Measurable (Y j)
h : ∀ (I : Finset S) (J : Finset T), (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) ⟂ᵢ[P] fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω
inst_2 : IsZeroOrProbabilityMeasure P
⊢ (fun (ω : Ω) (i : S) ↦ X i ω) ⟂ᵢ[P] fun (ω : Ω) (j : T) ↦ Y j ω

Tactic:
Kernel.IndepFun.process_indepFun_process hX hY h

Premises used: ProbabilityTheory.IndepFun, ProbabilityTheory.Kernel.IndepFun.process_indepFun_process
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) ⟂ᵢ[P] fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω
inst_2 : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S),
    AEMeasurable (_m := mΩ) (X i)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst : (i : S) → MeasurableSpace (𝓧 i)
inst_1 : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun (ω : Ω) (i : ↥I) ↦ X (↑i : S) ω) ⟂ᵢ[P] fun (ω : Ω) (j : ↥J) ↦ Y (↑j : T) ω
inst_2 : IsZeroOrProbabilityMeasure P
⊢ ∀ (j : T),
    AEMeasurable (_m := mΩ) (Y j)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → (j : T i) → Type u_5
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) P
h2 : ∀ (i : S) (j : T i), X i j =ᶠ[ae P] X' i j
⊢ ∀ (i : S) (j : T i),
    ∀ᵐ (a : Unit) ∂Measure.dirac (),
      X i j =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit P : (a : Unit) → Measure Ω) a : Measure Ω)] X' i j

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → (j : T i) → Type u_5
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
⊢ iIndepFun (β := fun (i : S) ↦ (j : T i) → 𝓧 i j) (fun (i : S) (ω : Ω) (j : T i) ↦ X i j ω) P

Tactic:
Kernel.iIndepFun.iIndepFun_process hX h

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process
-- Module: Mathlib.Probability.Independence.Process.Basic
Goal:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → (j : T i) → Type u_5
inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) 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
⊢ ∀ (i : S) (j : T i),
    AEMeasurable (_m := mΩ) (X i j)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit P) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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

Tactic:
iIndepFun_iff_finset.2 fun s ↦ ?_

Premises used: Iff.mpr, ProbabilityTheory.iIndepFun_iff_finset
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
refine :
  ∀ (s : Finset ℕ),
    iIndepFun (β := fun (x : ↥s) ↦ E)
      (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P
⊢ iIndepFun (β := fun (i : ℕ) ↦ E) (fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P

Tactic:
refine iIndepFun_iff_finset.2 fun s ↦ ?_

Premises used: Iff.mpr, ProbabilityTheory.iIndepFun_iff_finset
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
inr :
  ∀ (hs : s.Nonempty),
    iIndepFun (β := fun (x : ↥s) ↦ E)
      (s.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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
x : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ ∀ ⦃b : Fin (HAdd.hAdd (α := ℕ) 0 1)⦄,
    x ≤ b →
      LE.le.{u_1} (α := T) ((fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ t 0) x)
        ((fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ t 0) b)

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
⊢ IsProbabilityMeasure P

Tactic:
have := (hX 0 (fun _ ↦ t 0) (fun _ ↦ by grind)).isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
this : IsProbabilityMeasure P
⊢ iIndepFun (β := fun (x : ↥∅) ↦ E)
    (Finset.restrict (π := fun (i : ℕ) ↦ Ω → E) ∅ fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P

Tactic:
iIndepFun.of_subsingleton

Premises used: ProbabilityTheory.iIndepFun.of_subsingleton
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
this : IsProbabilityMeasure P
⊢ iIndepFun (β := fun (x : ↥∅) ↦ E)
    (Finset.restrict (π := fun (i : ℕ) ↦ Ω → E) ∅ fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P

Tactic:
exact iIndepFun.of_subsingleton

Premises used: ProbabilityTheory.iIndepFun.of_subsingleton
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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

Tactic:
iIndepFun.precomp (g := g) ?_ (hX (s.max' hs + 1) (fun m ↦ t m) ?_)

Premises used: Finset.max', Finset.restrict, Fin.val, ProbabilityTheory.iIndepFun.precomp, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
inr₁ : Monotone.{0, u_1} (β := T) fun (m : Fin (s.max' hs + 1 + 1)) ↦ t (↑m : ℕ)
⊢ iIndepFun (β := fun (x : ↥s) ↦ E)
    (s.restrict (π := fun (i : ℕ) ↦ Ω → E) fun (i : ℕ) (ω : Ω) ↦ X (t (i + 1)) ω - X (t i) ω) P

Tactic:
refine iIndepFun.precomp (g := g) ?_ (hX (s.max' hs + 1) (fun m ↦ t m) ?_)

Premises used: Finset.max', Fin.val, ProbabilityTheory.iIndepFun.precomp, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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 : ℕ), ⋯⟩
⊢ Function.Injective g

Tactic:
simp [g, Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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 : ℕ), ⋯⟩
⊢ Monotone.{0, u_1} (β := T) fun (m : Fin (s.max' hs + 1 + 1)) ↦ t (↑m : ℕ)

Tactic:
ht.comp Fin.val_strictMono.monotone

Premises used: StrictMono.monotone, Monotone.comp, Fin.val_strictMono
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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 : ℕ), ⋯⟩
⊢ Monotone.{0, u_1} (β := T) fun (m : Fin (s.max' hs + 1 + 1)) ↦ t (↑m : ℕ)

Tactic:
exact ht.comp Fin.val_strictMono.monotone

Premises used: StrictMono.monotone, Monotone.comp, Fin.val_strictMono
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
k : ℕ
⊢ min n k < n + 1

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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 : ℕ) + 1)) ω - X (t' (↑i : ℕ)) ω) P

Tactic:
(h t' ?_ ?_).precomp Fin.val_injective

Premises used: ProbabilityTheory.iIndepFun.precomp, Fin.val_injective
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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'
convert_2 : EventuallyConst t' atTop
⊢ iIndepFun (β := fun (i : Fin n) ↦ E) (fun (i : Fin n) (ω : Ω) ↦ X (t i.succ) ω - X (t i.castSucc) ω) P

Tactic:
convert! (h t' ?_ ?_).precomp Fin.val_injective with i ω

Premises used: ProbabilityTheory.iIndepFun.precomp, Fin.val_injective
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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, ⋯⟩
i : Fin n
ω : Ω
⊢ (↑i.succ : ℕ) = min n ((↑i : ℕ) + 1)

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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, ⋯⟩
i : Fin n
ω : Ω
⊢ (↑i.castSucc : ℕ) = min n (↑i : ℕ)

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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, ⋯⟩
a b : ℕ
hab : a ≤ b
⊢ (⟨min n a, ⋯⟩ : Fin (n + 1)) ≤ ⟨min n b, ⋯⟩

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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, ⋯⟩
⊢ Monotone t'

Tactic:
exact fun a b hab ↦ ht (by grind)
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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, ⋯⟩
⊢ ∀ (j : ℕ), n ≤ j → t' j = t' n

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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, ⋯⟩
⊢ EventuallyConst t' atTop

Tactic:
exact eventuallyConst_atTop.2 ⟨n, by grind⟩

Premises used: Iff.mpr, Filter.eventuallyConst_atTop, Exists.intro
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
r s t : T
hrs : r ≤ s
hst : s ≤ t
τ : ℕ → T :=
  fun (x : ℕ) ↦
    match (motive := ℕ → T) x with
    | 0 => r
    | 1 => s
    | x => t
x : ℕ
⊢ ∀ ⦃b : ℕ⦄, x ≤ b → τ x ≤ τ b

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
r s t : T
hrs : r ≤ s
hst : s ≤ t
τ : ℕ → T :=
  fun (x : ℕ) ↦
    match (motive := ℕ → T) x with
    | 0 => r
    | 1 => s
    | x => t
⊢ Ne (α := ℕ) 0 1

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
r s t : T
hrs : r ≤ s
hst : s ≤ t
τ : ℕ → T :=
  fun (x : ℕ) ↦
    match (motive := ℕ → T) x with
    | 0 => r
    | 1 => s
    | x => t
⊢ (X s - X r) ⟂ᵢ[P] X t - X s

Tactic:
exact hX.nat (t := τ) (fun _ ↦ by grind) |>.indepFun (by grind : 0 ≠ 1)

Premises used: ProbabilityTheory.HasIndepIncrements.nat, ProbabilityTheory.iIndepFun.indepFun
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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

Tactic:
(hX.indepFun_sub_sub hrs hst).congr ?_ .rfl

Premises used: ProbabilityTheory.IndepFun.congr, Filter.EventuallyEq.rfl, ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
refine : X s - X r =ᶠ[ae P] X s
⊢ X s ⟂ᵢ[P] X t - X s

Tactic:
refine (hX.indepFun_sub_sub hrs hst).congr ?_ .rfl

Premises used: ProbabilityTheory.IndepFun.congr, Filter.EventuallyEq.rfl, ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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ω : X r ω = 0
⊢ (X s - X r) ω = X s ω

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
h₂ h₃ : ∀ (ω : Ω) (hω : X r ω = 0), (X s - X r) ω = X s ω
⊢ X s - X r =ᶠ[ae P] X s

Tactic:
filter_upwards [h] with ω hω using by simp [hω]
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
F : Type u_4
G : Type u_5
inst_2 : MeasurableSpace G
inst_3 : FunLike F E G
inst_4 : AddGroup E
inst_5 : SubtractionMonoid G
inst_6 : AddMonoidHomClass F E G
f : F
hf : Measurable.{u_3, u_5} (α := E) (β := G) (⇑f : (a : E) → G)
hX : HasIndepIncrements X P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
simp_rw :
  iIndepFun (β := fun (i : Fin n) ↦ G)
    (fun (i : Fin n) (ω : Ω) ↦ (f : (a : E) → G) (X (t i.succ) ω - X (t i.castSucc) ω)) P
⊢ iIndepFun (β := fun (i : Fin n) ↦ G)
    (fun (i : Fin n) (ω : Ω) ↦
      HSub.hSub (α := G) ((fun (t : T) (ω : Ω) ↦ ((f : (a : E) → G) (X t ω) : G)) (t i.succ) ω)
        ((fun (t : T) (ω : Ω) ↦ ((f : (a : E) → G) (X t ω) : G)) (t i.castSucc) ω))
    P

Tactic:
simp_rw [← map_sub]

Premises used: map_sub
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
F : Type u_4
G : Type u_5
inst_2 : MeasurableSpace G
inst_3 : FunLike F E G
inst_4 : AddGroup E
inst_5 : SubtractionMonoid G
inst_6 : AddMonoidHomClass F E G
f : F
hf : Measurable.{u_3, u_5} (α := E) (β := G) (⇑f : (a : E) → G)
hX : HasIndepIncrements X P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
⊢ iIndepFun (β := fun (i : Fin n) ↦ G)
    (fun (i : Fin n) (ω : Ω) ↦ (f : (a : E) → G) (X (t i.succ) ω - X (t i.castSucc) ω)) P

Tactic:
(hX n t ht).comp (fun _ ↦ f) (fun _ ↦ hf)

Premises used: ProbabilityTheory.iIndepFun.comp, DFunLike.coe
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
F : Type u_4
G : Type u_5
inst_2 : MeasurableSpace G
inst_3 : FunLike F E G
inst_4 : AddGroup E
inst_5 : SubtractionMonoid G
inst_6 : AddMonoidHomClass F E G
f : F
hf : Measurable.{u_3, u_5} (α := E) (β := G) (⇑f : (a : E) → G)
hX : HasIndepIncrements X P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
⊢ iIndepFun (β := fun (i : Fin n) ↦ G)
    (fun (i : Fin n) (ω : Ω) ↦ (f : (a : E) → G) (X (t i.succ) ω - X (t i.castSucc) ω)) P

Tactic:
exact (hX n t ht).comp (fun _ ↦ f) (fun _ ↦ hf)

Premises used: ProbabilityTheory.iIndepFun.comp, DFunLike.coe
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
R : Type u_4
F : Type u_5
inst_2 : Semiring R
inst_3 : SeminormedAddCommGroup E
inst_4 : Module R E
inst_5 : OpensMeasurableSpace E
inst_6 : SeminormedAddCommGroup F
inst_7 : Module R F
inst_8 : MeasurableSpace F
inst_9 : BorelSpace F
L : E →L[R] F
hX : HasIndepIncrements X P
⊢ HasIndepIncrements.{u_1, u_2, u_5} (E := F) (fun (t : T) (ω : Ω) ↦ (L : (a : E) → F) (X t ω)) P

Tactic:
hX.map' L.measurable

Premises used: ContinuousLinearMap.measurable, ProbabilityTheory.HasIndepIncrements.map'
-- Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
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
R : Type u_4
inst_2 : AddGroup E
inst_3 : DistribSMul R E
inst_4 : MeasurableConstSMul R E
hX : HasIndepIncrements X P
c : R
⊢ HasIndepIncrements.{u_1, u_2, u_3} (E := E) (fun (t : T) (ω : Ω) ↦ c • X t ω) P

Tactic:
hX.map' (f := DistribSMul.toAddMonoidHom E c) (MeasurableConstSMul.measurable_const_smul c)

Premises used: MeasurableConstSMul.measurable_const_smul, ProbabilityTheory.HasIndepIncrements.map'