awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u v : ι → Ω → β
inst_2 : MeasurableSpace ι
inst_3 : Group β
inst_4 : ContinuousDiv β
hu : IsStronglyProgressive f u
hv : IsStronglyProgressive f v
⊢ IsStronglyProgressive.{u_1, u_2, u_3} (β := β) f fun (i : ι) (ω : Ω) ↦ u i ω / v i ω

Tactic:
fun i =>
  (hu i).div' (hv i)

Premises used: MeasureTheory.IsStronglyProgressive, MeasureTheory.StronglyMeasurable.div'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
inst_1 : MeasurableSpace ι
β : Type u_4
u : ι → Ω → β
inst_2 : SeminormedAddCommGroup β
hu : IsStronglyProgressive f u
⊢ IsStronglyProgressive (β := ℝ) f fun (t : ι) (ω : Ω) ↦ ‖u t ω‖

Tactic:
fun t ↦ (hu t).norm

Premises used: MeasureTheory.IsStronglyProgressive, MeasureTheory.StronglyMeasurable.norm
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : SecondCountableTopology β
inst_4 : OpensMeasurableSpace β
h : IsProgressive f u
⊢ IsStronglyProgressive f u

Tactic:
fun i ↦ (h i).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, MeasureTheory.IsStronglyProgressive
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : BorelSpace β
h : IsStronglyProgressive f u
⊢ IsProgressive f u

Tactic:
fun i ↦ (h i).measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.IsProgressive
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
fltr : Filter γ
inst_4 : fltr.NeBot
inst_5 : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
apply :
  Tendsto (β := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω → β)
    (fun (l : γ) (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ U l (↑p.1 : ι) p.2) fltr
    (𝓝 fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2)
⊢ StronglyMeasurable (β := β) fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2

Tactic:
apply @stronglyMeasurable_of_tendsto (Set.Iic i × Ω) β γ
    (MeasurableSpace.prod _ (f i)) _ _ fltr _ _ _ _ fun l => h l i

Premises used: stronglyMeasurable_of_tendsto
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
fltr : Filter γ
inst_4 : fltr.NeBot
inst_5 : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
rw :
  ∀ (h_tendsto : ∀ (x : ι), Tendsto (fun (i : γ) ↦ U i x) fltr (𝓝 (u x))) (i : ι)
    (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω),
    Tendsto (fun (i_1 : γ) ↦ U i_1 (↑x.1 : ι) x.2) fltr (𝓝 (u (↑x.1 : ι) x.2))
⊢ Tendsto (β := Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω → β)
    (fun (l : γ) (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ U l (↑p.1 : ι) p.2) fltr
    (𝓝 fun (p : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω) ↦ u (↑p.1 : ι) p.2)

Tactic:
rw [tendsto_pi_nhds] at h_tendsto ⊢

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
fltr : Filter γ
inst_4 : fltr.NeBot
inst_5 : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : ∀ (x : ι), Tendsto (fun (i : γ) ↦ U i x) fltr (𝓝 (u x))
i : ι
⊢ ∀ (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω),
    Tendsto (fun (i_1 : γ) ↦ U i_1 (↑x.1 : ι) x.2) fltr (𝓝 (u (↑x.1 : ι) x.2))

Tactic:
fun _ ↦ Tendsto.apply_nhds (h_tendsto _) _

Premises used: Prod.fst, Filter.Tendsto.apply_nhds, Subtype.val, Prod.snd
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
fltr : Filter γ
inst_4 : fltr.NeBot
inst_5 : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : ∀ (x : ι), Tendsto (fun (i : γ) ↦ U i x) fltr (𝓝 (u x))
i : ι
⊢ ∀ (x : Prod.{u_2, u_1} (↑(Set.Iic i) : Type u_2) Ω),
    Tendsto (fun (i_1 : γ) ↦ U i_1 (↑x.1 : ι) x.2) fltr (𝓝 (u (↑x.1 : ι) x.2))

Tactic:
exact fun _ ↦ Tendsto.apply_nhds (h_tendsto _) _

Premises used: Filter.Tendsto.apply_nhds
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : MeasurableSpace ι
inst_3 : PseudoMetrizableSpace β
U : ℕ → ι → Ω → β
h : ∀ (l : ℕ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U atTop (𝓝 u)
⊢ IsStronglyProgressive f u

Tactic:
isStronglyProgressive_of_tendsto' atTop h h_tendsto

Premises used: Filter.atTop, MeasureTheory.isStronglyProgressive_of_tendsto'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : TopologicalSpace ι
inst_3 : MetrizableSpace ι
inst_4 : SecondCountableTopology ι
inst_5 : MeasurableSpace ι
inst_6 : OpensMeasurableSpace ι
inst_7 : PseudoMetrizableSpace β
h : StronglyAdapted (β := fun (i : ι) ↦ β) f u
hu_cont : ∀ (ω : Ω), Continuous[inst_2, inst_1] fun (i : ι) ↦ u i ω
⊢ IsStronglyProgressive f u

Tactic:
fun i =>
  @stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable _ _ (Set.Iic i) _ _ _ _ _ _ _
    (f i) _ (fun ω => (hu_cont ω).comp continuous_induced_dom) fun j => (h j).mono (f.mono j.prop)

Premises used: Continuous.comp, MeasureTheory.IsStronglyProgressive, MeasureTheory.StronglyMeasurable.mono, Subtype.prop, continuous_induced_dom, MeasureTheory.Filtration.mono, MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable, Subtype.val
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : Type u_3
inst_1 : TopologicalSpace β
u : ι → Ω → β
inst_2 : TopologicalSpace ι
inst_3 : DiscreteTopology ι
inst_4 : SecondCountableTopology ι
inst_5 : MeasurableSpace ι
inst_6 : OpensMeasurableSpace ι
inst_7 : PseudoMetrizableSpace β
h : StronglyAdapted (β := fun (i : ι) ↦ β) f u
⊢ IsStronglyProgressive f u

Tactic:
h.isStronglyProgressive_of_continuous fun _ => continuous_of_discreteTopology

Premises used: MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous, continuous_of_discreteTopology
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
i j : ι
f : Filtration ι m
hij : i ≤ j
⊢ (↑f : ι → MeasurableSpace Ω) i ≤ (↑f : ι → MeasurableSpace Ω) j

Tactic:
f.mono' hij

Premises used: MeasureTheory.Filtration.mono'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
i : ι
⊢ (↑f : ι → MeasurableSpace Ω) i ≤ m

Tactic:
f.le' i

Premises used: MeasureTheory.Filtration.le'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f g : Filtration ι m
h : (↑f : ι → MeasurableSpace Ω) = (↑g : ι → MeasurableSpace Ω)
mk :
  ∀ (seq : ι → MeasurableSpace Ω) (mono' : Monotone seq) (le' : ∀ (i : ι), seq i ≤ m)
    (h :
      (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) =
        (↑g : ι → MeasurableSpace Ω)),
    { seq := seq, mono' := mono', le' := le' : Filtration ι m } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
g : Filtration ι m
seq : ι → MeasurableSpace Ω
mono' : Monotone seq
le' : ∀ (i : ι), seq i ≤ m
h :
  (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) = (↑g : ι → MeasurableSpace Ω)
mk :
  ∀ (seq_1 : ι → MeasurableSpace Ω) (mono'_1 : Monotone seq_1) (le'_1 : ∀ (i : ι), seq_1 i ≤ m)
    (h :
      (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) =
        (↑{ seq := seq_1, mono' := mono'_1, le' := le'_1 : Filtration ι m } : ι → MeasurableSpace Ω)),
    { seq := seq, mono' := mono', le' := le' : Filtration ι m } = { seq := seq_1, mono' := mono'_1, le' := le'_1 }
⊢ { seq := seq, mono' := mono', le' := le' : Filtration ι m } = g

Tactic:
cases g
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
seq : ι → MeasurableSpace Ω
mono' : Monotone seq
le' : ∀ (i : ι), seq i ≤ m
seq_1 : ι → MeasurableSpace Ω
mono'_1 : Monotone seq_1
le'_1 : ∀ (i : ι), seq_1 i ≤ m
h :
  (↑{ seq := seq, mono' := mono', le' := le' : Filtration ι m } : ι → MeasurableSpace Ω) =
    (↑{ seq := seq_1, mono' := mono'_1, le' := le'_1 : Filtration ι m } : ι → MeasurableSpace Ω)
⊢ { seq := seq, mono' := mono', le' := le' : Filtration ι m } = { seq := seq_1, mono' := mono'_1, le' := le'_1 }

Tactic:
congr
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
m' : MeasurableSpace Ω
hm' : m' ≤ m
i : ι
⊢ (↑(const ι m' hm') : ι → MeasurableSpace Ω) i = m'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f g : Filtration ι m
⊢ (↑(f ⊔ g) : ι → MeasurableSpace Ω) = (↑f : ι → MeasurableSpace Ω) ⊔ (↑g : ι → MeasurableSpace Ω)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f g : Filtration ι m
⊢ (↑(f ⊓ g) : ι → MeasurableSpace Ω) = (↑f : ι → MeasurableSpace Ω) ⊓ (↑g : ι → MeasurableSpace Ω)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) i)
    ((fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j)

Tactic:
sSup_le fun m' hm' => ?_

Premises used: sSup_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
refine :
  ∀ (m' : MeasurableSpace Ω)
    (hm' :
      Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s)
        m'),
    m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) i)
    ((fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j)

Tactic:
refine sSup_le fun m' hm' => ?_

Premises used: sSup_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) m'
⊢ ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'

Tactic:
rw [Set.mem_image] at hm'

Premises used: Set.mem_image
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'
obtain :
  ∀ (f : Filtration ι m) (hf_mem : f ∈ s) (hfm' : (↑f : ι → MeasurableSpace Ω) i = m'),
    m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
⊢ m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j

Tactic:
obtain ⟨f, hf_mem, hfm'⟩ := hm'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
rw :
  (↑f : ι → MeasurableSpace Ω) i ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
⊢ m' ≤ (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j

Tactic:
rw [← hfm']
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ (↑f : ι → MeasurableSpace Ω) i ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j

Tactic:
(f.mono hij).trans ?_

Premises used: MeasureTheory.Filtration.mono, LE.le.trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
refine :
  (↑f : ι → MeasurableSpace Ω) j ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j
⊢ (↑f : ι → MeasurableSpace Ω) i ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j

Tactic:
refine (f.mono hij).trans ?_

Premises used: MeasureTheory.Filtration.mono, LE.le.trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) j) '' s)
    ((↑f : ι → MeasurableSpace Ω) j)

Tactic:
have hfj_mem : f j ∈ (fun g : Filtration ι m => g j) '' s := ⟨f, hf_mem, rfl⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
hfj_mem :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) j) '' s)
    ((↑f : ι → MeasurableSpace Ω) j)
⊢ (↑f : ι → MeasurableSpace Ω) j ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j

Tactic:
le_sSup hfj_mem

Premises used: le_sSup
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
hfj_mem :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) j) '' s)
    ((↑f : ι → MeasurableSpace Ω) j)
⊢ (↑f : ι → MeasurableSpace Ω) j ≤
    (fun (i : ι) ↦ (sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) : MeasurableSpace Ω)) j

Tactic:
exact le_sSup hfj_mem

Premises used: le_sSup
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m

Tactic:
sSup_le fun m' hm' => ?_

Premises used: sSup_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
refine :
  ∀ (m' : MeasurableSpace Ω)
    (hm' :
      Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s)
        m'),
    m' ≤ m
⊢ sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ m

Tactic:
refine sSup_le fun m' hm' => ?_

Premises used: sSup_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) m'
⊢ ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'

Tactic:
rw [Set.mem_image] at hm'

Premises used: Set.mem_image
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, (↑x : ι → MeasurableSpace Ω) i = m'
obtain : ∀ f ∈ s, ∀ (hfm' : (↑f : ι → MeasurableSpace Ω) i = m'), m' ≤ m
⊢ m' ≤ m

Tactic:
obtain ⟨f, _, hfm'⟩ := hm'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
rw : (↑f : ι → MeasurableSpace Ω) i ≤ m
⊢ m' ≤ m

Tactic:
rw [← hfm']
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ (↑f : ι → MeasurableSpace Ω) i ≤ m

Tactic:
f.le i

Premises used: MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left : f ∈ s
hfm' : (↑f : ι → MeasurableSpace Ω) i = m'
⊢ (↑f : ι → MeasurableSpace Ω) i ≤ m

Tactic:
exact f.le i

Premises used: MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (↑(sSup s) : ι → MeasurableSpace Ω) i = sSup ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
pos :
  ∀ (h_nonempty : s.Nonempty),
    LE.le.{u_1} (α := MeasurableSpace Ω)
      ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
        i)
      ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
        j)
neg :
  ∀ (h_nonempty : ¬s.Nonempty),
    LE.le.{u_1} (α := MeasurableSpace Ω)
      ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
        i)
      ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
        j)
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      i)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      j)

Tactic:
by_cases h_nonempty : Set.Nonempty s

Premises used: Set.Nonempty
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬s.Nonempty
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      i)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      j)

Tactic:
simp only [h_nonempty, if_false, le_refl]

Premises used: le_refl, if_false
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
pos : ∀ a ∈ s, sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑a : ι → MeasurableSpace Ω) j
⊢ LE.le.{u_1} (α := MeasurableSpace Ω)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      i)
    ((fun (i : ι) ↦ if s.Nonempty then sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) else m)
      j)

Tactic:
simp only [h_nonempty, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp,
          forall_apply_eq_imp_iff₂]

Premises used: le_sInf_iff, if_true, and_imp, Set.mem_image, forall_exists_index, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
⊢ ∀ a ∈ s, sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑a : ι → MeasurableSpace Ω) j

Tactic:
fun f hf_mem => le_trans ?_ (f.mono hij)

Premises used: MeasureTheory.Filtration.mono, le_trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
pos :
  ∀ (f : Filtration ι m) (hf_mem : f ∈ s),
    sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑f : ι → MeasurableSpace Ω) i
⊢ ∀ a ∈ s, sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑a : ι → MeasurableSpace Ω) j

Tactic:
refine fun f hf_mem => le_trans ?_ (f.mono hij)

Premises used: le_trans
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
f : Filtration ι m
hf_mem : f ∈ s
⊢ Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) i) '' s)
    ((↑f : ι → MeasurableSpace Ω) i)

Tactic:
have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' s := ⟨f, hf_mem, rfl⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
f : Filtration ι m
hf_mem : f ∈ s
hfi_mem :
  Membership.mem (γ := Set (MeasurableSpace Ω)) ((fun (g : Filtration ι m) ↦ (↑g : ι → MeasurableSpace Ω) i) '' s)
    ((↑f : ι → MeasurableSpace Ω) i)
⊢ sInf ((fun (f : Filtration ι m) ↦ (↑f : ι → MeasurableSpace Ω) i) '' s) ≤ (↑f : ι → MeasurableSpace Ω) i

Tactic:
sInf_le hfi_mem

Premises used: sInf_le