awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
h : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {t : Set Ω | ∃ j ≤ i, s j = t} t → MeasurableSet t
h₁ : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1} t → MeasurableSet t
⊢ Eq.{u_1 + 1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
    (MeasurableSpace.generateFrom {s_1 : Set Ω | ∃ (n : ι), MeasurableSet s_1})

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Premises used: le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)

Tactic:
measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, ?_⟩⟩

Premises used: MeasurableSpace.measurableSet_generateFrom, And.intro, Exists.intro
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
h : MeasurableSet (s j)
⊢ MeasurableSet (s j)

Tactic:
refine measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, ?_⟩⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
h : MeasurableSet (s j)
⊢ MeasurableSet (s j)

Tactic:
rw [comap_eq_generateFrom]

Premises used: MeasurableSpace.comap_eq_generateFrom
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)

Tactic:
measurableSet_generateFrom ⟨{1}, measurableSet_singleton 1, ?_⟩

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSpace.measurableSet_generateFrom, And.intro, Exists.intro, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
h : Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} = s j
⊢ MeasurableSet (s j)

Tactic:
refine measurableSet_generateFrom ⟨{1}, measurableSet_singleton 1, ?_⟩
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
h : ∀ (x : Ω), x ∈ Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} ↔ x ∈ s j
⊢ Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} = s j

Tactic:
ext x
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
x : Ω
⊢ x ∈ Set.preimage (β := β j) ((s j).indicator fun (x : Ω) ↦ 1) {1} ↔ x ∈ s j

Tactic:
simp
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
this :
  LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
    (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
⊢ MeasurableSet t

Tactic:
this _ ht
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
this :
  LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
    (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
⊢ MeasurableSet t

Tactic:
exact this _ ht
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
h :
  LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
    (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})
⊢ MeasurableSet t

Tactic:
suffices MeasurableSpace.generateFrom {t | n ≤ i ∧
      MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β n)) (mβ n)] t} ≤
        MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t} by
      exact this _ ht
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
    (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})

Tactic:
generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
h : ∀ (t : Set Ω), Membership.mem (γ := Set (Set Ω)) {t : Set Ω | n ≤ i ∧ MeasurableSet t} t → MeasurableSet t
⊢ LE.le.{u_1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {t : Set Ω | n ≤ i ∧ MeasurableSet t})
    (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t})

Tactic:
refine generateFrom_le ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
h : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ), MeasurableSet t
h₁ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n), MeasurableSet t
h₂ : ∀ (heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ), MeasurableSet t
h₃ : ∀ (heq : Membership.mem (γ := Set (Set Ω)) {∅} (((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u)), MeasurableSet t
⊢ MeasurableSet t

Tactic:
obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)

Premises used: Set.indicator_const_preimage, OfNat.ofNat
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : Membership.mem (γ := Set (Set Ω)) {∅} (((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u)
⊢ ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅

Tactic:
rw [Set.mem_singleton_iff] at heq

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : Membership.mem (γ := Set (Set Ω)) {∅} (((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u)
⊢ ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅

Tactic:
on_goal 4 => rw [Set.mem_singleton_iff] at heq

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
⊢ Set.univ = t

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
hu'₁ : Set.univ = t
⊢ ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
h : MeasurableSet.{u_1} (α := Ω) Set.univ
⊢ MeasurableSet t

Tactic:
rw [← hu']
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n
⊢ s n = t

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n
hu'₁ : s n = t
⊢ ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n
h : MeasurableSet (s n)
⊢ MeasurableSet t

Tactic:
rw [← hu']
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ (s n)ᶜ = t

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ
hu'₁ : (s n)ᶜ = t
⊢ ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ
h : MeasurableSet (s n)ᶜ
⊢ MeasurableSet t

Tactic:
rw [← hu']
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
⊢ ∅ = t

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
hu'₁ : ∅ = t
⊢ ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅

Tactic:
rw [heq] at hu'
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
h : MeasurableSet.{u_1} (α := Ω) ∅
⊢ MeasurableSet t

Tactic:
rw [← hu']
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet.{u_1} (α := Ω) Set.univ

Tactic:
MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)

Tactic:
measurableSet_generateFrom ⟨n, hn, rfl⟩

Premises used: MeasurableSpace.measurableSet_generateFrom, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ

Tactic:
MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩)

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl, And.intro, Exists.intro, rfl
-- Module: Mathlib.Probability.Process.Filtration
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : Preorder ι
inst_4 : (i : ι) → MulZeroOneClass (β i)
inst_5 : ∀ (i : ι), Nontrivial.{u_3} (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t_1 : Set Ω
n : ι
ht : MeasurableSet t_1
t : Set Ω
hn : n ≤ i
u : Set (β n)
left : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun (x : Ω) ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet.{u_1} (α := Ω) ∅

Tactic:
measurableSet_empty _

Premises used: MeasurableSet, MeasurableSpace.measurableSet_empty