awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
h₂ :
  Eq.{u_1 + 1} (α := Set Ω)
    (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅
refine : ∀ (i : ι) (hi : i ≤ n), MeasurableSet.{u_1} (α := Ω) {x : Ω | hittingBtwn u s i N x ≤ n}
⊢ MeasurableSet.{u_1} (α := Ω)
    (⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})

Tactic:
refine MeasurableSet.iUnion fun i => MeasurableSet.iUnion fun hi =>
    (f.mono hi _ (hτ.measurableSet_eq i)).inter ?_

Premises used: setOf, MeasureTheory.IsStoppingTime.measurableSet_eq, WithTop.some, MeasureTheory.Filtration.mono, MeasurableSet.iUnion, Eq, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
N : ι
hτbdd : ∀ (x : Ω), τ x ≤ (↑N : WithTop ι)
s : Set β
hs : MeasurableSet s
hf : Adapted (β := fun (i : ι) ↦ β) f u
n : ι
h₁ :
  Eq.{u_1 + 1} (α := Set Ω) {x : Ω | hittingBtwn u s (τ x).untopA N x ≤ n}
    ((⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∪
      ⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
h₂ :
  Eq.{u_1 + 1} (α := Set Ω)
    (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅
i : ι
hi : i ≤ n
⊢ MeasurableSet.{u_1} (α := Ω) {x : Ω | hittingBtwn u s i N x ≤ n}

Tactic:
simpa using hf.isStoppingTime_hittingBtwn hs n

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
simp :
  (∀ (x : ι), ¬(Membership.mem (γ := Set ι) Set.univ x ∧ u x ω ∈ s)) →
    Eq.{u_3 + 1} (α := ι) ⊤ (sInf {i : ι | u i ω ∈ s})
⊢ hittingBtwn u s ⊥ ⊤ ω = sInf {i : ι | u i ω ∈ s}

Tactic:
simp only [hittingBtwn, Set.Icc_bot,
    Set.Iic_top, Set.univ_inter, ite_eq_left_iff, not_exists]

Premises used: ite_eq_left_iff, not_exists, MeasureTheory.hittingBtwn, Set.univ_inter, Set.Iic_top, Set.Icc_bot
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(Membership.mem (γ := Set ι) Set.univ x ∧ u x ω ∈ s)
symm : Eq.{u_3 + 1} (α := ι) (sInf {i : ι | u i ω ∈ s}) ⊤
⊢ Eq.{u_3 + 1} (α := ι) ⊤ (sInf {i : ι | u i ω ∈ s})

Tactic:
symm
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(Membership.mem (γ := Set ι) Set.univ x ∧ u x ω ∈ s)
rw : ∀ (a : ι), Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} a → a = ⊤
⊢ Eq.{u_3 + 1} (α := ι) (sInf {i : ι | u i ω ∈ s}) ⊤

Tactic:
rw [sInf_eq_top]

Premises used: sInf_eq_top
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(Membership.mem (γ := Set ι) Set.univ x ∧ u x ω ∈ s)
⊢ ∀ (x : ι), u x ω ∉ s

Tactic:
simp only [Set.mem_univ, true_and] at h_notMem_s

Premises used: Set.mem_univ, true_and
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), u x ω ∉ s
⊢ ∀ (a : ι), Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} a → a = ⊤

Tactic:
fun i hi_mem_s => absurd hi_mem_s (h_notMem_s i)

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), u x ω ∉ s
⊢ ∀ (a : ι), Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} a → a = ⊤

Tactic:
exact fun i hi_mem_s => absurd hi_mem_s (h_notMem_s i)

Premises used: absurd
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
inst_1 : (ω : Ω) → Decidable (∃ (j : ι), u j ω ∈ s)
ω : Ω
⊢ hittingAfter u s ⊥ ω = if ∃ (j : ι), u j ω ∈ s then (↑(sInf {i : ι | u i ω ∈ s}) : WithTop ι) else ⊤

Tactic:
simp [hittingAfter]

Premises used: MeasureTheory.hittingAfter
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
inl : ∀ (hi : i < n), hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
inr : ∀ (hi : n ≤ i), hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
rcases lt_or_ge i n with hi | hi

Premises used: lt_or_ge
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : i < n
inl : (∃ j ∈ Set.Icc ⊥ i, u j ω ∈ s) ↔ ∃ j ≤ i, u j ω ∈ s
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
rw [hittingBtwn_le_iff_of_lt _ hi]

Premises used: MeasureTheory.hittingBtwn_le_iff_of_lt
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : i < n
⊢ (∃ j ∈ Set.Icc ⊥ i, u j ω ∈ s) ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
simp
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : n ≤ i
inr : ∃ j ≤ i, u j ω ∈ s
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
simp only [(hittingBtwn_le ω).trans hi, true_iff]

Premises used: true_iff, MeasureTheory.hittingBtwn_le, LE.le.trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hx : ∃ j ≤ n, u j ω ∈ s
hi : n ≤ i
inr : ∀ (j : ι) (hj₁ : j ≤ n) (hj₂ : u j ω ∈ s), ∃ j ≤ i, u j ω ∈ s
⊢ ∃ j ≤ i, u j ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hx
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hi : n ≤ i
j : ι
hj₁ : j ≤ n
hj₂ : u j ω ∈ s
⊢ ∃ j ≤ i, u j ω ∈ s

Tactic:
⟨j, hj₁.trans hi, hj₂⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i n : ι
ω : Ω
hi : n ≤ i
j : ι
hj₁ : j ≤ n
hj₂ : u j ω ∈ s
⊢ ∃ j ≤ i, u j ω ∈ s

Tactic:
exact ⟨j, hj₁.trans hi, hj₂⟩
-- Module: Mathlib.Probability.Process.HittingTime
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrderBot ι
inst_1 : WellFoundedLT ι
u : ι → Ω → β
s : Set β
i : ι
ω : Ω
⊢ hittingAfter u s ⊥ ω ≤ (↑i : WithTop ι) ↔ ∃ j ≤ i, u j ω ∈ s

Tactic:
simp [hittingAfter_le_iff]

Premises used: MeasureTheory.hittingAfter_le_iff
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
⊢ ∀ (t : T), X t =ᶠ[ae P] X t

Tactic:
simp
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
h : IsAEKolmogorovProcess X P p q M
⊢ IsKolmogorovProcess (IsAEKolmogorovProcess.mk X h) P p q M

Tactic:
(Classical.choose_spec h).1

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.mk, Classical.choose_spec, And.left
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
h : IsAEKolmogorovProcess X P p q M
⊢ ∀ (t : T), X t =ᶠ[ae P] IsAEKolmogorovProcess.mk X h t

Tactic:
(Classical.choose_spec h).2

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.mk, Classical.choose_spec, And.right
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ ∫⁻ (ω : Ω), edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p ∂P ≤
    (↑M : ℝ≥0∞) * edist s t ^ q

Tactic:
hX.IsKolmogorovProcess_mk.kolmogorovCondition s t

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h :
  ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P =
    ∫⁻ (ω : Ω), edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p ∂P
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q

Tactic:
convert! hX.IsKolmogorovProcess_mk.kolmogorovCondition s t using 1

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P =
    ∫⁻ (ω : Ω), edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p ∂P

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h :
  (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P =
    ∫⁻ (ω : Ω), edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p ∂P

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h :
  ∀ (ω : Ω) (hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω) (hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω),
    edist (X s ω) (X t ω) ^ p = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p

Tactic:
filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
ω : Ω
hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω
hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω
h :
  edist (IsAEKolmogorovProcess.mk X hX s ω) (X t ω) ^ p =
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
⊢ edist (X s ω) (X t ω) ^ p = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p

Tactic:
simp_rw [hω₁, hω₂]
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
⊢ 0 < p

Tactic:
hX.IsKolmogorovProcess_mk.p_pos

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, ProbabilityTheory.IsKolmogorovProcess.p_pos
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
⊢ 0 < q

Tactic:
hX.IsKolmogorovProcess_mk.q_pos

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, ProbabilityTheory.IsKolmogorovProcess.q_pos
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X Y : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᶠ[ae P] Y t
⊢ IsAEKolmogorovProcess Y P p q M

Tactic:
⟨hX.mk X, hX.IsKolmogorovProcess_mk, fun t ↦ ?_⟩

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.mk, ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, And.intro, Exists.intro, ProbabilityTheory.IsAEKolmogorovProcess
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X Y : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᶠ[ae P] Y t
refine : ∀ (t : T), Y t =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX t
⊢ IsAEKolmogorovProcess Y P p q M

Tactic:
refine ⟨hX.mk X, hX.IsKolmogorovProcess_mk, fun t ↦ ?_⟩
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X Y : T → Ω → E
hX_1 : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᶠ[ae P] Y t
t : T
ω : Ω
hX : X t ω = IsAEKolmogorovProcess.mk X hX_1 t ω
hY : X t ω = Y t ω
⊢ Y t ω = IsAEKolmogorovProcess.mk X hX_1 t ω

Tactic:
hY.symm.trans hX

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X Y : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᶠ[ae P] Y t
t : T
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X t x = IsAEKolmogorovProcess.mk X hX t x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X t x = Y t x) x} x →
                Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ Y t x = IsAEKolmogorovProcess.mk X hX t x) x} x}
            x}
      a
h₂ h₃ :
  ∀ (ω : Ω) (hX_1 : X t ω = IsAEKolmogorovProcess.mk X hX t ω) (hY : X t ω = Y t ω),
    Y t ω = IsAEKolmogorovProcess.mk X hX t ω
⊢ Y t =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX t

Tactic:
filter_upwards [hX.ae_eq_mk t, h t] with ω hX hY using hY.symm.trans hX

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
⊢ let this : MeasurableSpace (E × E) := borel (E × E);
  BorelSpace.{u_3} (E × E)

Tactic:
borelize (E × E)

Premises used: Prod
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
this : MeasurableSpace (E × E) := borel (E × E)
this_1 : BorelSpace.{u_3} (E × E)
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (ω : Ω) ↦ edist (X s ω) (X t ω)

Tactic:
continuous_edist.stronglyMeasurable.comp_measurable (hX.measurablePair s t)

Premises used: continuous_edist, Continuous.stronglyMeasurable, MeasureTheory.StronglyMeasurable.comp_measurable, ProbabilityTheory.IsKolmogorovProcess.measurablePair
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
this : MeasurableSpace (E × E) := borel (E × E)
this_1 : BorelSpace.{u_3} (E × E)
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (ω : Ω) ↦ edist (X s ω) (X t ω)

Tactic:
exact continuous_edist.stronglyMeasurable.comp_measurable (hX.measurablePair s t)

Premises used: continuous_edist, Continuous.stronglyMeasurable, MeasureTheory.StronglyMeasurable.comp_measurable, ProbabilityTheory.IsKolmogorovProcess.measurablePair
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ AEStronglyMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) P

Tactic:
⟨(fun ω ↦ edist (hX.mk X s ω) (hX.mk X t ω)),
    hX.IsKolmogorovProcess_mk.stronglyMeasurable_edist, ?_⟩

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.mk, ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist, And.intro, Exists.intro, EDist.edist, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
refine :
  (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)
⊢ AEStronglyMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) P

Tactic:
refine ⟨(fun ω ↦ edist (hX.mk X s ω) (hX.mk X t ω)),
    hX.IsKolmogorovProcess_mk.stronglyMeasurable_edist, ?_⟩
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
ω : Ω
hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω
hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω
⊢ edist (X s ω) (X t ω) = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)

Tactic:
simp [hω₁, hω₂]
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X s x = IsAEKolmogorovProcess.mk X hX s x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X t x = IsAEKolmogorovProcess.mk X hX t x) x} x →
                Membership.mem (γ := Set Ω)
                  {x : Ω |
                    (fun (x : Ω) ↦
                        Eq (α := ℝ≥0∞) ((fun (ω : Ω) ↦ edist (X s ω) (X t ω)) x)
                          ((fun (ω : Ω) ↦ edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω))
                            x))
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (ω : Ω) (hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω) (hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω),
    edist (X s ω) (X t ω) = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)

Tactic:
filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂ using by simp [hω₁, hω₂]

Premises used: ProbabilityTheory.IsAEKolmogorovProcess.ae_eq_mk
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
⊢ Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ edist (X s ω) (X t ω)

Tactic:
hX.stronglyMeasurable_edist.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ AEMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) P

Tactic:
hX.aestronglyMeasurable_edist.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.IsAEKolmogorovProcess.aestronglyMeasurable_edist
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
hX : IsKolmogorovProcess X P p q M
s : T
⊢ Measurable (X s)

Tactic:
(measurable_fst.mono prod_le_borel_prod le_rfl).comp (hX.measurablePair s s)

Premises used: le_rfl, Measurable.comp, ProbabilityTheory.IsKolmogorovProcess.measurablePair, prod_le_borel_prod, Measurable.mono, measurable_fst
-- Module: Mathlib.Probability.Process.Kolmogorov
Goal:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
hX : IsAEKolmogorovProcess X P p q M
s : T
⊢ AEMeasurable (X s) P

Tactic:
⟨hX.mk X s, hX.IsKolmogorovProcess_mk.measurable s, ?_⟩

Premises used: ProbabilityTheory.IsKolmogorovProcess.measurable, AEMeasurable, ProbabilityTheory.IsAEKolmogorovProcess.mk, ProbabilityTheory.IsAEKolmogorovProcess.IsKolmogorovProcess_mk, And.intro, Exists.intro