awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m_1 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m_1
u : ι → Ω → β
τ : Ω → WithTop ι
hτ_1 : IsStoppingTime f τ
N : ι
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})
x : Ω
m : ι
hm : n < m
hτ : τ x = (↑m : WithTop ι)
hτbdd : τ x ≤ (↑N : WithTop ι)
h_top : τ x ≠ ⊤
⊢ m ≤ N
have h : ∀ (t : ι) (hτ : (↑t : WithTop ι) = (↑m : WithTop ι)) (hτbdd : (↑t : WithTop ι) ≤ (↑N : WithTop ι)), m ≤ N
Tactic: lift τ x to ι using h_top with t
Cleared hypotheses: hτ, hτbdd, h_top
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m_1 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrder ι
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : FirstCountableTopology ι
inst_6 : MeasurableSpace β
f : Filtration ι m_1
u : ι → Ω → β
τ : Ω → WithTop ι
hτ_1 : IsStoppingTime f τ
N : ι
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})
x : Ω
m : ι
hm : n < m
t : ι
hτ : (↑t : WithTop ι) = (↑m : WithTop ι)
hτbdd : (↑t : WithTop ι) ≤ (↑N : WithTop ι)
⊢ m ≤ N
have hτbdd₁ : (↑m : WithTop ι) ≤ (↑N : WithTop ι)
Tactic: rw [hτ] at hτbdd
Cleared hypotheses: hτbdd
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
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})
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (x : Ω) ↦ (↑(hittingBtwn u s (τ x).untopA N x) : WithTop ι)) ω ≤ (↑n : WithTop ι)}
have h₂ : Eq.{u_1 + 1} (α := Set Ω)
  (⋃ (i : ι), ⋃ (_ : i > n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n}) ∅
Tactic: have h₂ : ⋃ i > n, {x | τ x = i} ∩ {x | hittingBtwn u s i N x ≤ n} = ∅ := by
    ext x
    simp only [gt_iff_lt, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq, exists_prop,
      Set.mem_empty_iff_false, iff_false, not_exists, not_and, not_le]
    refine fun m hm hτ ↦ hm.trans_le <| le_hittingBtwn ?_ x
    specialize hτbdd x
    have h_top : τ x ≠ ⊤ := fun h => by simp [h] at hτbdd
    lift τ x to ι using h_top with t
    rw [hτ] at hτbdd
    exact mod_cast hτbdd
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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}) ∅
⊢ MeasurableSet.{u_1} (α := Ω)
    {ω : Ω | (fun (x : Ω) ↦ (↑(hittingBtwn u s (τ x).untopA N x) : WithTop ι)) ω ≤ (↑n : WithTop ι)}
have simp : MeasurableSet.{u_1} (α := Ω)
  (⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
Tactic: simp only [WithTop.coe_le_coe, h₁, h₂, Set.union_empty]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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}) ∅
⊢ MeasurableSet.{u_1} (α := Ω)
    (⋃ (i : ι), ⋃ (_ : i ≤ n), {x : Ω | τ x = (↑i : WithTop ι)} ∩ {x : Ω | hittingBtwn u s i N x ≤ n})
have refine : ∀ (i : ι) (hi : i ≤ n), MeasurableSet.{u_1} (α := Ω) {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 ?_
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
⊢ hittingBtwn u s ⊥ ⊤ ω = sInf {i : ι | u i ω ∈ s}
have simp : (∀ (x : ι), ¬(Membership.mem (γ := Set ι) Set.univ x ∧ u x ω ∈ s)) → Eq.{u_3 + 1} (α := ι) ⊤ (sInf {i : ι | u i ω ∈ s})
Tactic: simp only [hittingBtwn, Set.Icc_bot,
    Set.Iic_top, Set.univ_inter, ite_eq_left_iff, not_exists]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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)
⊢ Eq.{u_3 + 1} (α := ι) ⊤ (sInf {i : ι | u i ω ∈ s})
have symm : Eq.{u_3 + 1} (α := ι) (sInf {i : ι | u i ω ∈ s}) ⊤
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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)
⊢ Eq.{u_3 + 1} (α := ι) (sInf {i : ι | u i ω ∈ s}) ⊤
have rw : ∀ (a : ι), Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} a → a = ⊤
Tactic: rw [sInf_eq_top]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (hypothesis)
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)
⊢ ∀ (a : ι), Membership.mem (γ := Set ι) {i : ι | u i ω ∈ s} a → a = ⊤
have h_notMem_s₁ : ∀ (x : ι), u x ω ∉ s
Tactic: simp only [Set.mem_univ, true_and] at h_notMem_s
Cleared hypotheses: h_notMem_s
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
have inl : ∀ (hi : i < n), hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
Tactic: rcases lt_or_ge i n with hi | hi
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
have inr : ∀ (hi : n ≤ i), hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
Tactic: rcases lt_or_ge i n with hi | hi
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
have inl : (∃ j ∈ Set.Icc ⊥ i, u j ω ∈ s) ↔ ∃ j ≤ i, u j ω ∈ s
Tactic: rw [hittingBtwn_le_iff_of_lt _ hi]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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
⊢ hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
have inr : ∃ j ≤ i, u j ω ∈ s
Tactic: simp only [(hittingBtwn_le ω).trans hi, true_iff]
-- Lean 4 proof step from Mathlib.Probability.Process.HittingTime (goal)
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
⊢ ∃ j ≤ i, u j ω ∈ s
have inr : ∀ (j : ι) (hj₁ : j ≤ n) (hj₂ : u j ω ∈ s), ∃ j ≤ i, u j ω ∈ s
Tactic: obtain ⟨j, hj₁, hj₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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 ≤ (↑M : ℝ≥0∞) * edist s t ^ q
have h : ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P =
  ∫⁻ (ω : Ω), edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p ∂P
Tactic: convert! hX.IsKolmogorovProcess_mk.kolmogorovCondition s t using 1
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
have 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
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
have 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
Tactic: filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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 ω) ^ p = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
have h : edist (IsAEKolmogorovProcess.mk X hX s ω) (X t ω) ^ p =
  edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p
Tactic: simp_rw [hω₁, hω₂]
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
have refine : ∀ (t : T), Y t =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX t
Tactic: refine ⟨hX.mk X, hX.IsKolmogorovProcess_mk, fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
⊢ Y t =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX t
have 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
Tactic: filter_upwards [hX.ae_eq_mk t, h t] with ω hX hY using hY.symm.trans hX
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
⊢ Y t =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX t
have h₂ : ∀ (a : Ω), X t a = IsAEKolmogorovProcess.mk X hX t a → X t a = Y t a → Y t a = IsAEKolmogorovProcess.mk X hX t a
Tactic: filter_upwards [hX.ae_eq_mk t, h t] with ω hX hY using hY.symm.trans hX
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (hypothesis)
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
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (ω : Ω) ↦ edist (X s ω) (X t ω)
have this : let this : MeasurableSpace (E × E) := borel (E × E);
BorelSpace.{u_3} (E × E)
Tactic: borelize (E × E)
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
have refine : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) fun (ω : Ω) ↦
  edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)
Tactic: refine ⟨(fun ω ↦ edist (hX.mk X s ω) (hX.mk X t ω)),
    hX.IsKolmogorovProcess_mk.stronglyMeasurable_edist, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)
have 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
Tactic: filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂ using by simp [hω₁, hω₂]
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
⊢ (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω)) fun (ω : Ω) ↦
    edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)
have h₁ : ∀ (a : Ω),
  X s a = IsAEKolmogorovProcess.mk X hX s a →
    X t a = IsAEKolmogorovProcess.mk X hX t a →
      edist (X s a) (X t a) = edist (IsAEKolmogorovProcess.mk X hX s a) (IsAEKolmogorovProcess.mk X hX t a)
Tactic: filter_upwards [hX.ae_eq_mk s, hX.ae_eq_mk t] with ω hω₁ hω₂ using by simp [hω₁, hω₂]
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
have refine : X s =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX s
Tactic: refine ⟨hX.mk X s, hX.IsKolmogorovProcess_mk.measurable s, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
⊢ X s =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX s
have 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 : Ω | (fun (x : Ω) ↦ X s x = IsAEKolmogorovProcess.mk X hX s x) x} x}
    a
Tactic: filter_upwards [hX.ae_eq_mk s] with ω hω using hω
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
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 : Ω | (fun (x : Ω) ↦ X s x = IsAEKolmogorovProcess.mk X hX s x) x} x}
      a
⊢ X s =ᶠ[ae P] IsAEKolmogorovProcess.mk X hX s
have h₁ : ∀ (a : Ω), X s a = IsAEKolmogorovProcess.mk X hX s a → X s a = IsAEKolmogorovProcess.mk X hX s a
Tactic: filter_upwards [hX.ae_eq_mk s] with ω hω using hω
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
inst_4 : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
this : Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
⊢ Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
have rwa : ∀ (this : Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)),
  Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
Tactic: rwa [Prod.borelSpace.measurable_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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
inst_4 : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ (↑M : ℝ≥0∞) * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
⊢ Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
have suffices : Measurable.{u_2, u_3} (β := E × E) fun (ω : Ω) ↦ (X s ω, X t ω)
Tactic: suffices Measurable (fun ω ↦ (X s ω, X t ω)) by
      rwa [Prod.borelSpace.measurable_eq] at this
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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 s t = 0
this : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
have h₁ : ∀ (ω : Ω) (hω : edist (X s ω) (X t ω) ^ p = 0 ω), edist (X s ω) (X t ω) = 0
Tactic: filter_upwards [this] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Process.Kolmogorov (goal)
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 s t = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
have suffices : (ae P).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ edist (X s ω) (X t ω) ^ p) 0
Tactic: suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω