awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
have refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | π ω ≤ τ ω}
Tactic: refine MeasurableSet.inter (measurableSet_stopping_time_le_min hτ hπ) ?_
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | π ω ≤ τ ω}
have h : ∀ (x : Ω), min (τ x) (π x) = min (π x) (τ x)
Tactic: convert! (measurableSet_stopping_time_le_min hπ hτ) using 3
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
x : Ω
⊢ min (τ x) (π x) = min (π x) (τ x)
have h : min (π x) (τ x) = min (π x) (τ x)
Tactic: rw [min_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
have h : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
Tactic: have h := measurableSet_eq_stopping_time_min hτ hπ
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : SecondCountableTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
h : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
have h₁ : MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω} ∧ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}
Tactic: rw [measurableSet_min_iff hτ hπ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
⊢ stoppedValue (stoppedProcess u τ) σ = fun (ω : Ω) ↦
    if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
    else stoppedValue u (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)) ω
have h : ∀ (ω : Ω),
  stoppedValue (stoppedProcess u τ) σ ω =
    if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
    else stoppedValue u (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
⊢ stoppedValue (stoppedProcess u τ) σ ω =
    if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
    else stoppedValue u (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)) ω
have h : u (min (↑(σ ω).untopA : WithTop ι) (τ ω)).untopA ω =
  if σ ω = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω else u (min (σ ω) (τ ω)).untopA ω
Tactic: simp only [stoppedValue, stoppedProcess, ne_eq, ite_not]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
⊢ u (min (↑(σ ω).untopA : WithTop ι) (τ ω)).untopA ω =
    if σ ω = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω else u (min (σ ω) (τ ω)).untopA ω
have h : u (min (↑(untopA ⊤) : WithTop ι) (τ ω)).untopA ω =
  if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
  else u (min ⊤ (τ ω)).untopA ω
Tactic: cases σ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
h :
  u (min (↑(untopA ⊤) : WithTop ι) (τ ω)).untopA ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min ⊤ (τ ω)).untopA ω
⊢ u (min (↑(σ ω).untopA : WithTop ι) (τ ω)).untopA ω =
    if σ ω = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω else u (min (σ ω) (τ ω)).untopA ω
have h₁ : ∀ (a : ι),
  u (min (↑(↑a : WithTop ι).untopA : WithTop ι) (τ ω)).untopA ω =
    if (↑a : WithTop ι) = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min (↑a : WithTop ι) (τ ω)).untopA ω
Tactic: cases σ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
⊢ u (min (↑(untopA ⊤) : WithTop ι) (τ ω)).untopA ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min ⊤ (τ ω)).untopA ω
have h : u (untopA (min (↑(untopA ⊤) : WithTop ι) ⊤)) ω =
  if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) ⊤).untopA ω
  else u (untopA (min ⊤ ⊤)) ω
Tactic: cases τ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
h :
  u (untopA (min (↑(untopA ⊤) : WithTop ι) ⊤)) ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) ⊤).untopA ω
    else u (untopA (min ⊤ ⊤)) ω
⊢ u (min (↑(untopA ⊤) : WithTop ι) (τ ω)).untopA ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min ⊤ (τ ω)).untopA ω
have h₁ : ∀ (a : ι),
  u (min (↑(untopA ⊤) : WithTop ι) (↑a : WithTop ι)).untopA ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (↑a : WithTop ι)).untopA ω
    else u (min ⊤ (↑a : WithTop ι)).untopA ω
Tactic: cases τ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
a : ι
⊢ u (min (↑(↑a : WithTop ι).untopA : WithTop ι) (τ ω)).untopA ω =
    if (↑a : WithTop ι) = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min (↑a : WithTop ι) (τ ω)).untopA ω
have h : u (min (↑(↑a : WithTop ι).untopA : WithTop ι) ⊤).untopA ω =
  if (↑a : WithTop ι) = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) ⊤).untopA ω
  else u (min (↑a : WithTop ι) ⊤).untopA ω
Tactic: cases τ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
a : ι
h :
  u (min (↑(↑a : WithTop ι).untopA : WithTop ι) ⊤).untopA ω =
    if (↑a : WithTop ι) = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) ⊤).untopA ω
    else u (min (↑a : WithTop ι) ⊤).untopA ω
⊢ u (min (↑(↑a : WithTop ι).untopA : WithTop ι) (τ ω)).untopA ω =
    if (↑a : WithTop ι) = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min (↑a : WithTop ι) (τ ω)).untopA ω
have h₁ : ∀ (a_1 : ι),
  u (min (↑(↑a : WithTop ι).untopA : WithTop ι) (↑a_1 : WithTop ι)).untopA ω =
    if (↑a : WithTop ι) = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (↑a_1 : WithTop ι)).untopA ω
    else u (min (↑a : WithTop ι) (↑a_1 : WithTop ι)).untopA ω
Tactic: cases τ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
μ : Measure Ω
hσ : ∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤
⊢ stoppedValue (stoppedProcess u τ) σ =ᶠ[ae μ] stoppedValue u fun (ω : Ω) ↦ min (σ ω) (τ ω)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ σ ω ≠ ⊤) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦ stoppedValue (stoppedProcess u τ) σ x = stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x) x}
          x}
    a
Tactic: filter_upwards [hσ] with ω hσ using by simp [stoppedValue_stoppedProcess, hσ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
μ : Measure Ω
hσ : ∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ σ ω ≠ ⊤) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ stoppedValue (stoppedProcess u τ) σ x = stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x)
                x}
            x}
      a
⊢ stoppedValue (stoppedProcess u τ) σ =ᶠ[ae μ] stoppedValue u fun (ω : Ω) ↦ min (σ ω) (τ ω)
have h₁ : ∀ (a : Ω), σ a ≠ ⊤ → stoppedValue (stoppedProcess u τ) σ a = stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) a
Tactic: filter_upwards [hσ] with ω hσ using by simp [stoppedValue_stoppedProcess, hσ]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i = s.indicator (stoppedProcess u τ i)
have h : ∀ (ω : Ω), stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
ω : Ω
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
have pos : ∀ (hω : ω ∈ s), stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
Tactic: by_cases hω : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
ω : Ω
pos : ∀ (hω : ω ∈ s), stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
have neg : ∀ (hω : ω ∉ s), stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
Tactic: by_cases hω : ω ∈ s
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
⊢ Eq (α := ι → Ω → β) (stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ) fun (i : ι) ↦
    s.indicator (stoppedProcess u τ i)
have h : ∀ (i : ι) (ω : Ω), stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
Tactic: ext i ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
ω : Ω
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
have h : s.indicator (stoppedProcess u τ i) ω = s.indicator (stoppedProcess u τ i) ω
Tactic: rw [stoppedProcess_indicator_comm]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u (σ ⊓ τ)
have h : ∀ (i : ι) (ω : Ω), stoppedProcess (stoppedProcess u τ) σ i ω = stoppedProcess u (σ ⊓ τ) i ω
Tactic: ext i ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
⊢ stoppedProcess (stoppedProcess u τ) σ i ω = stoppedProcess u (σ ⊓ τ) i ω
have h : u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
  u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: simp_rw [stoppedProcess]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have pos : ∀ (hτ : τ ω = ⊤),
  u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: by_cases hτ : τ ω = ⊤
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
pos :
  ∀ (hτ : τ ω = ⊤),
    u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
      u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg : ∀ (hτ : ¬τ ω = ⊤),
  u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: by_cases hτ : τ ω = ⊤
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have pos : ∀ (hσ : σ ω = ⊤),
  u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: by_cases hσ : σ ω = ⊤
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
pos :
  ∀ (hσ : σ ω = ⊤),
    u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
      u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg : ∀ (hσ : ¬σ ω = ⊤),
  u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: by_cases hσ : σ ω = ⊤
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have pos : ∀ (hστ : σ ω ≤ τ ω),
  u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: by_cases hστ : σ ω ≤ τ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
pos :
  ∀ (hστ : σ ω ≤ τ ω),
    u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
      u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg : ∀ (hστ : ¬σ ω ≤ τ ω),
  u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: by_cases hστ : σ ω ≤ τ ω
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have pos : u ((↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι).untop sorry) ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: rw [min_eq_left, untopA_eq_untop coe_ne_top]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
pos : u ((↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι).untop ⋯) ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have pos₁ : (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) ≤ τ ω
Tactic: rw [min_eq_left, untopA_eq_untop coe_ne_top]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) ≤ τ ω
have pos : (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) ≤ σ ω
Tactic: refine le_trans ?_ hστ
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg : u (min (↑((min (↑i : WithTop ι) (σ ω)).untop sorry) : WithTop ι) (τ ω)).untopA ω =
  u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: nth_rewrite 2 [untopA_eq_untop]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
neg :
  u (min (↑((min (↑i : WithTop ι) (σ ω)).untop ⋯) : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg₁ : min (↑i : WithTop ι) (σ ω) ≠ ⊤
Tactic: nth_rewrite 2 [untopA_eq_untop]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑((min (↑i : WithTop ι) (σ ω)).untop ⋯) : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg : u (min (min (↑i : WithTop ι) (σ ω)) (τ ω)).untopA ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: rw [coe_untop, min_assoc, Pi.inf_apply]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
neg : u (min (min (↑i : WithTop ι) (σ ω)) (τ ω)).untopA ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑((min (↑i : WithTop ι) (σ ω)).untop ⋯) : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg₁ : u (min (↑i : WithTop ι) (min (σ ω) (τ ω))).untopA ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
Tactic: rw [coe_untop, min_assoc, Pi.inf_apply]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
neg : u (min (min (↑i : WithTop ι) (σ ω)) (τ ω)).untopA ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
neg₁ : u (min (↑i : WithTop ι) (min (σ ω) (τ ω))).untopA ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
⊢ u (min (↑((min (↑i : WithTop ι) (σ ω)).untop ⋯) : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω
have neg₂ : u (min (↑i : WithTop ι) (min (σ ω) (τ ω))).untopA ω = u (min (↑i : WithTop ι) (min (σ ω) (τ ω))).untopA ω
Tactic: rw [coe_untop, min_assoc, Pi.inf_apply]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u fun (ω : Ω) ↦ min (σ ω) (τ ω)
have rw : stoppedProcess u (σ ⊓ τ) = stoppedProcess u fun (ω : Ω) ↦ min (σ ω) (τ ω)
Tactic: rw [stoppedProcess_stoppedProcess]
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (goal)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
⊢ IsStronglyProgressive (β := ι) f fun (i : ι) (ω : Ω) ↦ (min (↑i : WithTop ι) (τ ω)).untopA
have refine : ∀ (i : ι),
  Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
    min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)
Tactic: refine fun i ↦ (Measurable.untopA ?_).stronglyMeasurable
-- Lean 4 proof step from Mathlib.Probability.Process.Stopping (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
τ : Ω → WithTop ι
inst_2 : MeasurableSpace ι
inst_3 : TopologicalSpace ι
inst_4 : OrderTopology ι
inst_5 : SecondCountableTopology ι
inst_6 : BorelSpace ι
f : Filtration ι m
inst_7 : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  MeasurableSpace.prod (Subtype.instMeasurableSpace (p := fun (x : ι) ↦ x ∈ Set.Iic i)) ((↑f : ι → MeasurableSpace Ω) i)
m_set : (t : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) → MeasurableSpace (↑t : Type (max u_1 u_3)) :=
  fun (x : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω)) ↦
    Subtype.instMeasurableSpace (p := fun (x_1 : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦ x_1 ∈ x)
s : Set (Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) :=
  {p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω | τ p.2 ≤ (↑i : WithTop ι)}
⊢ Measurable (β := WithTop ι) fun (p : Prod.{u_3, u_1} (↑(Set.Iic i) : Type u_3) Ω) ↦
    min (↑(↑p.1 : ι) : WithTop ι) (τ p.2)
have hs : MeasurableSet s
Tactic: have hs : MeasurableSet[m_prod] s := @measurable_snd (Set.Iic i) Ω _ (f i) _ (hτ i)