-- 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:
Ω : 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)
⊢ filtrationOfSet hsm = natural (fun i => (s i).indicator fun x => 1) ⋯

Tactic:
simp only [filtrationOfSet, natural, measurableSpace_iSup_eq, exists_prop, mk.injEq]

Result:
Ω : 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)
⊢ (fun i => MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) = fun i =>
    MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}

Proof state:
case h.refine_2.intro.intro.intro.intro.inl
Ω : 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' : Set.univ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ

case h.refine_2.intro.intro.intro.intro.inr.inl
Ω : 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 = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)

case h.refine_2.intro.intro.intro.intro.inr.inr.inl
Ω : 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)ᶜ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ

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 ∅

Tactic:
exacts [MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩,
  MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩), measurableSet_empty _]

Result:
no goals

Proof state:
case h.refine_2.intro.intro.intro.intro.inl
Ω : 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 = Set.univ
⊢ MeasurableSet t

case h.refine_2.intro.intro.intro.intro.inr.inl
Ω : 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 = s n
⊢ MeasurableSet t

case h.refine_2.intro.intro.intro.intro.inr.inr.inl
Ω : 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 = (s n)ᶜ
⊢ MeasurableSet t

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:
all_goals rw [heq] at hu'; rw [← hu']

Result:
case h.refine_2.intro.intro.intro.intro.inl
Ω : 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' : Set.univ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ

case h.refine_2.intro.intro.intro.intro.inr.inl
Ω : 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 = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)

case h.refine_2.intro.intro.intro.intro.inr.inr.inl
Ω : 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)ᶜ = t
heq : ((s n).indicator fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ

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 ∅