-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem generateFrom_squareCylinders [∀ i, MeasurableSpace (α i)] :
    MeasurableSpace.generateFrom (squareCylinders fun i ↦ {s : Set (α i) | MeasurableSet s}) =
      MeasurableSpace.pi

Proof state:
case a.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (t i)
⊢ (↑s).pi t ∈ {t | MeasurableSet t}

Tactic:
exact MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)

Result:
no goals

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

Tactic:
refine iSup_le fun i ↦ ?_

Result:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤
    MeasurableSpace.generateFrom (squareCylinders fun i => {s | MeasurableSet s})

Proof state:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤
    MeasurableSpace.generateFrom (squareCylinders fun i => {s | MeasurableSet s})

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

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

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

Tactic:
rw [MeasurableSpace.generateFrom_le_iff]

Result:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ (squareCylinders fun i => {s | MeasurableSet s}) ⊆ {t | MeasurableSet t}

Proof state:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ (squareCylinders fun i => {s | MeasurableSet s}) ⊆ {t | MeasurableSet t}

Tactic:
rintro S ⟨s, t, h, rfl⟩

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

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

Tactic:
rw [← Finset.coe_singleton, squareCylinders_eq_iUnion_image]

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

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

Tactic:
exact subset_iUnion
  (fun (s : Finset ι) ↦
    (fun t : ∀ i, Set (α i) ↦ (s : Set ι).pi t) '' univ.pi (fun i ↦ setOf MeasurableSet))
  ({i} : Finset ι)

Result:
no goals

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

Tactic:
refine MeasurableSpace.generateFrom_mono ?_

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

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

Tactic:
simp only [mem_univ_pi, mem_setOf_eq] at h

Result:
case a.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (t i)
⊢ (↑s).pi t ∈ {t | MeasurableSet t}

Proof state:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.generateFrom (squareCylinders fun i => {s | MeasurableSet s}) = MeasurableSpace.pi

Tactic:
apply le_antisymm

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

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