-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem generateFrom_measurableCylinders :
    MeasurableSpace.generateFrom (measurableCylinders α) = MeasurableSpace.pi

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
S : Set ((i : ι) → α i)
hS : S ∈ measurableCylinders α
⊢ MeasurableSet S

Tactic:
obtain ⟨s, S, hSm, rfl⟩ := (mem_measurableCylinders _).mp hS

Result:
case a.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hSm : MeasurableSet S
hS : cylinder s S ∈ measurableCylinders α
⊢ MeasurableSet (cylinder s S)

Proof state:
case a.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hSm : MeasurableSet S
hS : cylinder s S ∈ measurableCylinders α
⊢ MeasurableSet (cylinder s S)

Tactic:
exact hSm.cylinder

Result:
no goals

Proof state:
case a.h
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' t i ↔ x ∈ cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}

Tactic:
simp only [mem_preimage, Function.eval, mem_cylinder, mem_setOf_eq, Finset.restrict]

Result:
no goals

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤ MeasurableSpace.generateFrom (measurableCylinders α)

Tactic:
refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.generateFrom ((fun t => {i}.pi t) '' univ.pi fun i => {s | MeasurableSet s}) ≤
    MeasurableSpace.generateFrom (measurableCylinders α)

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∃ s S, MeasurableSet S ∧ eval i ⁻¹' t i = cylinder s S

Tactic:
refine ⟨{i}, {f | f ⟨i, Finset.mem_singleton_self i⟩ ∈ t i}, measurable_pi_apply _ (ht i), ?_⟩

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ eval i ⁻¹' t i = cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.generateFrom ((fun t => {i}.pi t) '' univ.pi fun i => {s | MeasurableSet s}) ≤
    MeasurableSpace.generateFrom (measurableCylinders α)

Tactic:
refine MeasurableSpace.generateFrom_mono (fun x ↦ ?_)

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
x : Set ((i : ι) → α i)
⊢ (x ∈ (fun t => {i}.pi t) '' univ.pi fun i => {s | MeasurableSet s}) → x ∈ measurableCylinders α

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
x : Set ((i : ι) → α i)
⊢ ∀ (x_1 : (i : ι) → Set (α i)),
    (∀ (i : ι), MeasurableSet (x_1 i)) → eval i ⁻¹' x_1 i = x → ∃ s S, MeasurableSet S ∧ x = cylinder s S

Tactic:
rintro t ht rfl

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∃ s S, MeasurableSet S ∧ eval i ⁻¹' t i = cylinder s S

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi ≤ MeasurableSpace.generateFrom (measurableCylinders α)

Tactic:
refine iSup_le fun i ↦ ?_

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤ MeasurableSpace.generateFrom (measurableCylinders α)

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
x : Set ((i : ι) → α i)
⊢ (x ∈ (fun t => {i}.pi t) '' univ.pi fun i => {s | MeasurableSet s}) → x ∈ measurableCylinders α

Tactic:
simp only [singleton_pi, Function.eval, mem_image, mem_pi, mem_univ, mem_setOf_eq,
  forall_true_left, mem_measurableCylinders, exists_prop, forall_exists_index, and_imp]

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
x : Set ((i : ι) → α i)
⊢ ∀ (x_1 : (i : ι) → Set (α i)),
    (∀ (i : ι), MeasurableSet (x_1 i)) → eval i ⁻¹' x_1 i = x → ∃ s S, MeasurableSet S ∧ x = cylinder s S

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi

Tactic:
refine MeasurableSpace.generateFrom_le (fun S hS ↦ ?_)

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
S : Set ((i : ι) → α i)
hS : S ∈ measurableCylinders α
⊢ MeasurableSet S

Proof state:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ eval i ⁻¹' t i = cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}

Tactic:
ext1 x

Result:
case a.h
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' t i ↔ x ∈ cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.generateFrom (measurableCylinders α) = MeasurableSpace.pi

Tactic:
apply le_antisymm

Result:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi

case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi ≤ MeasurableSpace.generateFrom (measurableCylinders α)