awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Stopping
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} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})

Tactic:
MeasurableSet.inter (measurableSet_stopping_time_le_min hτ hπ) ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
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 Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
refine : MeasurableSet.{u_1} (α := Ω) {ω : Ω | π ω ≤ τ ω}
⊢ MeasurableSet.{u_1} (α := Ω) ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})

Tactic:
refine MeasurableSet.inter (measurableSet_stopping_time_le_min hτ hπ) ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min, MeasurableSet.inter
-- Module: Mathlib.Probability.Process.Stopping
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} (α := Ω) {ω : Ω | π ω ≤ τ ω}

Tactic:
(measurableSet_stopping_time_le_min hπ hτ)

Premises used: MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min
-- Module: Mathlib.Probability.Process.Stopping
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 Ω) {ω : Ω | τ ω = π ω} ({ω : Ω | τ ω ≤ π ω} ∩ {ω : Ω | π ω ≤ τ ω})
h : ∀ (x : Ω), min (τ x) (π x) = min (π x) (τ x)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | π ω ≤ τ ω}

Tactic:
convert! (measurableSet_stopping_time_le_min hπ hτ) using 3

Premises used: MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min
-- Module: Mathlib.Probability.Process.Stopping
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 : Ω
h h₁ : min (π x) (τ x) = min (π x) (τ x)
⊢ min (τ x) (π x) = min (π x) (τ x)

Tactic:
rw [min_comm]

Premises used: min_comm
-- Module: Mathlib.Probability.Process.Stopping
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} (α := Ω) {ω : Ω | τ ω = π ω}

Tactic:
have h := measurableSet_eq_stopping_time_min hτ hπ
-- Module: Mathlib.Probability.Process.Stopping
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} (α := Ω) {ω : Ω | τ ω = π ω} ∧ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}

Tactic:
rw [measurableSet_min_iff hτ hπ] at h

Premises used: MeasureTheory.IsStoppingTime.measurableSet_min_iff
-- Module: Mathlib.Probability.Process.Stopping
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} (α := Ω) {ω : Ω | τ ω = π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Probability.Process.Stopping
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} (α := Ω) {ω : Ω | τ ω = π ω}
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | τ ω = π ω}

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
u : ι → Ω → β
i : ι
⊢ (stoppedValue u fun (x : Ω) ↦ (↑i : WithTop ι)) = u i

Tactic:
rfl

Premises used: MeasureTheory.stoppedValue, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
⊢ stoppedProcess u τ = fun (i : ι) ↦ stoppedValue u fun (ω : Ω) ↦ min (↑i : WithTop ι) (τ ω)

Tactic:
rfl

Premises used: MeasureTheory.stoppedValue, MeasureTheory.stoppedProcess, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
i : ι
ω : Ω
⊢ stoppedProcess u τ i ω = stoppedValue u (fun (ω : Ω) ↦ min (↑i : WithTop ι) (τ ω)) ω

Tactic:
rfl

Premises used: MeasureTheory.stoppedValue, MeasureTheory.stoppedProcess, rfl
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
h :
  ∀ (ω : Ω),
    stoppedValue (stoppedProcess u τ) σ ω =
      if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
      else stoppedValue u (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)) ω
⊢ stoppedValue (stoppedProcess u τ) σ = fun (ω : Ω) ↦
    if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
    else stoppedValue u (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)) ω

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
h :
  u (min (↑(σ ω).untopA : WithTop ι) (τ ω)).untopA ω =
    if σ ω = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω else u (min (σ ω) (τ ω)).untopA ω
⊢ stoppedValue (stoppedProcess u τ) σ ω =
    if σ ω ≠ ⊤ then stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
    else stoppedValue u (fun (ω : Ω) ↦ min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)) ω

Tactic:
simp only [stoppedValue, stoppedProcess, ne_eq, ite_not]

Premises used: MeasureTheory.stoppedValue, MeasureTheory.stoppedProcess, ne_eq, ite_not
-- Module: Mathlib.Probability.Process.Stopping
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 ω
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 ω
⊢ u (min (↑(σ ω).untopA : WithTop ι) (τ ω)).untopA ω =
    if σ ω = ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω else u (min (σ ω) (τ ω)).untopA ω

Tactic:
cases σ ω
-- Module: Mathlib.Probability.Process.Stopping
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 ⊤ ⊤)) ω
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 ω
⊢ u (min (↑(untopA ⊤) : WithTop ι) (τ ω)).untopA ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) (τ ω)).untopA ω
    else u (min ⊤ (τ ω)).untopA ω

Tactic:
cases τ ω
-- Module: Mathlib.Probability.Process.Stopping
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 ω
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 ω
⊢ 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 τ ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
⊢ u (untopA (min (↑(untopA ⊤) : WithTop ι) ⊤)) ω =
    if Eq.{u_3 + 1} (α := WithTop ι) ⊤ ⊤ then u (min (↑(Classical.arbitrary ι) : WithTop ι) ⊤).untopA ω
    else u (untopA (min ⊤ ⊤)) ω

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
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:
simp
-- Module: Mathlib.Probability.Process.Stopping
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 ω

Tactic:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
a 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:
simp
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
ω : Ω
hω : σ ω ≠ ⊤
⊢ stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω

Tactic:
simp [stoppedValue_stoppedProcess, hω]

Premises used: MeasureTheory.stoppedValue_stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
μ : Measure Ω
hσ_1 : ∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤
ω : Ω
hσ : σ ω ≠ ⊤
⊢ stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω

Tactic:
simp [stoppedValue_stoppedProcess, hσ]

Premises used: MeasureTheory.stoppedValue_stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
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
h₁ h₂ :
  ∀ (ω : Ω) (hσ : σ ω ≠ ⊤), stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun (ω : Ω) ↦ min (σ ω) (τ ω)) ω
⊢ stoppedValue (stoppedProcess u τ) σ =ᶠ[ae μ] stoppedValue u fun (ω : Ω) ↦ min (σ ω) (τ ω)

Tactic:
filter_upwards [hσ] with ω hσ using by simp [stoppedValue_stoppedProcess, hσ]
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
i : ι
ω : Ω
h : (↑i : WithTop ι) ≤ τ ω
⊢ stoppedProcess u τ i ω = u i ω

Tactic:
simp [stoppedProcess, min_eq_left h]

Premises used: MeasureTheory.stoppedProcess, min_eq_left
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
i : ι
ω : Ω
h : τ ω ≤ (↑i : WithTop ι)
⊢ stoppedProcess u τ i ω = u (τ ω).untopA ω

Tactic:
simp [stoppedProcess, min_eq_right h]

Premises used: MeasureTheory.stoppedProcess, min_eq_right
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
h : ∀ (ω : Ω), 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)

Tactic:
ext ω
-- Module: Mathlib.Probability.Process.Stopping
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) ω
neg : ∀ (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) ω

Tactic:
by_cases hω : ω ∈ s
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
ω : Ω
hω : ω ∈ s
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω

Tactic:
simp [stoppedProcess, hω]

Premises used: MeasureTheory.stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
ω : Ω
hω : ω ∉ s
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω

Tactic:
simp [stoppedProcess, hω]

Premises used: MeasureTheory.stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
h : ∀ (i : ι) (ω : Ω), stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω
⊢ Eq (α := ι → Ω → β) (stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ) fun (i : ι) ↦
    s.indicator (stoppedProcess u τ i)

Tactic:
ext i ω
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst_2 : Zero β
s : Set Ω
i : ι
ω : Ω
h h₁ : s.indicator (stoppedProcess u τ i) ω = s.indicator (stoppedProcess u τ i) ω
⊢ stoppedProcess (fun (i : ι) ↦ s.indicator (u i)) τ i ω = s.indicator (stoppedProcess u τ i) ω

Tactic:
rw [stoppedProcess_indicator_comm]

Premises used: MeasureTheory.stoppedProcess_indicator_comm
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
h : ∀ (i : ι) (ω : Ω), stoppedProcess (stoppedProcess u τ) σ i ω = stoppedProcess u (σ ⊓ τ) i ω
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u (σ ⊓ τ)

Tactic:
ext i ω
-- Module: Mathlib.Probability.Process.Stopping
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 ω
⊢ stoppedProcess (stoppedProcess u τ) σ i ω = stoppedProcess u (σ ⊓ τ) i ω

Tactic:
simp_rw [stoppedProcess]

Premises used: MeasureTheory.stoppedProcess
-- Module: Mathlib.Probability.Process.Stopping
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 ω
neg :
  ∀ (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 ω

Tactic:
by_cases hτ : τ ω = ⊤
-- Module: Mathlib.Probability.Process.Stopping
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 ω

Tactic:
simp [hτ]
-- Module: Mathlib.Probability.Process.Stopping
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 ω
neg :
  ∀ (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 ω

Tactic:
by_cases hσ : σ ω = ⊤
-- Module: Mathlib.Probability.Process.Stopping
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 ω

Tactic:
simp [hσ]
-- Module: Mathlib.Probability.Process.Stopping
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 ω
neg :
  ∀ (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 ω

Tactic:
by_cases hστ : σ ω ≤ τ ω
-- Module: Mathlib.Probability.Process.Stopping
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 ω
pos₁ : (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) ≤ τ ω
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω

Tactic:
rw [min_eq_left, untopA_eq_untop coe_ne_top]

Premises used: WithTop.untopA_eq_untop, WithTop.coe_ne_top, min_eq_left
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
⊢ u ((↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι).untop ⋯) ω = u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω

Tactic:
simp [hστ]
-- Module: Mathlib.Probability.Process.Stopping
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 ι) ≤ τ ω

Tactic:
le_trans ?_ hστ

Premises used: le_trans
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : σ ω ≤ τ ω
pos : (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) ≤ σ ω
⊢ (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) ≤ τ ω

Tactic:
refine le_trans ?_ hστ

Premises used: le_trans
-- Module: Mathlib.Probability.Process.Stopping
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 ι) ≤ σ ω

Tactic:
simp [untopA_eq_untop]

Premises used: WithTop.untopA_eq_untop
-- Module: Mathlib.Probability.Process.Stopping
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 ω
neg₁ : min (↑i : WithTop ι) (σ ω) ≠ ⊤
⊢ u (min (↑(min (↑i : WithTop ι) (σ ω)).untopA : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω

Tactic:
nth_rewrite 2 [untopA_eq_untop]

Premises used: WithTop.untopA_eq_untop
-- Module: Mathlib.Probability.Process.Stopping
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 ω
neg₂ neg₃ : u (min (↑i : WithTop ι) (min (σ ω) (τ ω))).untopA ω = u (min (↑i : WithTop ι) (min (σ ω) (τ ω))).untopA ω
⊢ u (min (↑((min (↑i : WithTop ι) (σ ω)).untop ⋯) : WithTop ι) (τ ω)).untopA ω =
    u (min (↑i : WithTop ι) ((σ ⊓ τ) ω)).untopA ω

Tactic:
rw [coe_untop, min_assoc, Pi.inf_apply]

Premises used: WithTop.coe_untop, min_assoc, Pi.inf_apply
-- Module: Mathlib.Probability.Process.Stopping
Goal:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst : Nonempty ι
inst_1 : LinearOrder ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ min (↑i : WithTop ι) (σ ω) ≠ ⊤

Tactic:
(lt_of_le_of_lt (min_le_right _ _) <| lt_top_iff_ne_top.2 hσ).ne

Premises used: Iff.mpr, lt_of_le_of_lt, lt_top_iff_ne_top, min_le_right, LT.lt.ne