-- Mathlib/Probability/Process/Filtration.lean
theorem filtrationOfSet_eq_natural [MulZeroOneClass β] [Nontrivial β] {s : ι → Set Ω}
    (hsm : ∀ i, MeasurableSet[m] (s i)) :
    filtrationOfSet hsm = natural (fun i => (s i).indicator (fun _ => 1 : Ω → β)) fun i =>
      stronglyMeasurable_one.indicator (hsm i)

Proof state:
case h.refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ t ∈ {s_1 | ∃ n, MeasurableSet s_1}, MeasurableSet t

Tactic:
rintro t ⟨n, ht⟩

Result:
case h.refine_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSet t

Proof state:
case h.refine_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x => 1) ⁻¹' u = t
heq : ((s n).indicator fun x => 1) ⁻¹' u ∈ {∅}
⊢ MeasurableSet t

Tactic:
rw [Set.mem_singleton_iff] at heq

Result:
case h.refine_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x => 1) ⁻¹' u = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Proof state:
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t} = MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}

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

Result:
case h.refine_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ t ∈ {t | ∃ j ≤ i, s j = t}, MeasurableSet t

case h.refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ t ∈ {s_1 | ∃ n, MeasurableSet s_1}, MeasurableSet t

Proof state:
case h.refine_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x => 1) ⁻¹' u = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Tactic:
rw [heq] at hu'

Result:
case h.refine_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Proof state:
case h.refine_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ ((s j).indicator fun x => 1) ⁻¹' {1} = s j

Tactic:
ext x

Result:
case h.refine_1.intro.intro.h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
x : Ω
⊢ x ∈ ((s j).indicator fun x => 1) ⁻¹' {1} ↔ x ∈ s j

Proof state:
case h.refine_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Tactic:
rw [← hu']

Result:
case h.refine_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet ∅

Proof state:
case h.refine_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)

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

Result:
case h.refine_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ ((s j).indicator fun x => 1) ⁻¹' {1} = s j