-- Mathlib/Probability/Process/PartitionFiltration.lean
lemma measurable_memPartitionSet_subtype (ht : ∀ n, MeasurableSet (t n)) (n : ℕ)
    (m : MeasurableSpace (memPartition t n)) :
    @Measurable α (memPartition t n) (partitionFiltration ht n) m
      (fun a ↦ ⟨memPartitionSet t n a, memPartitionSet_mem t n a⟩)

Proof state:
case h.e'_3.h
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet {x | memPartitionSet t n x = s}
x : α
⊢ x ∈ (fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩} ↔ x ∈ {x | memPartitionSet t n x = s}

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet {x | memPartitionSet t n x = s}
⊢ (fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩} = {x | memPartitionSet t n x = s}

Tactic:
ext x

Result:
case h.e'_3.h
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet {x | memPartitionSet t n x = s}
x : α
⊢ x ∈ (fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩} ↔ x ∈ {x | memPartitionSet t n x = s}

Proof state:
case mk
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet ((fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩})

Tactic:
suffices MeasurableSet[partitionFiltration ht n] {x | memPartitionSet t n x = s} by
  convert this
  ext x
  simp

Result:
case mk
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet {x | memPartitionSet t n x = s}

Proof state:
case mk
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet {x | memPartitionSet t n x = s}

Tactic:
simp_rw [memPartitionSet_eq_iff _ hs]

Result:
case mk
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet {x | x ∈ s}

Proof state:
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet {x | memPartitionSet t n x = s}
⊢ MeasurableSet ((fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩})

Tactic:
convert this

Result:
case h.e'_3
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
this : MeasurableSet {x | memPartitionSet t n x = s}
⊢ (fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩} = {x | memPartitionSet t n x = s}

Proof state:
case mk
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet {x | x ∈ s}

Tactic:
exact measurableSet_partitionFiltration_of_mem _ _ hs

Result:
no goals

Proof state:
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : ↑(memPartition t n)
⊢ MeasurableSet ((fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {s})

Tactic:
rcases s with ⟨s, hs⟩

Result:
case mk
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet ((fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩})

Proof state:
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
⊢ Measurable fun a => ⟨memPartitionSet t n a, ⋯⟩

Tactic:
refine @measurable_to_countable' (memPartition t n) α m _
  (partitionFiltration ht n) _ (fun s ↦ ?_)

Result:
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : ↑(memPartition t n)
⊢ MeasurableSet ((fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {s})