-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem inter_mem_measurableCylinders (hs : s ∈ measurableCylinders α)
    (ht : t ∈ measurableCylinders α) :
    s ∩ t ∈ measurableCylinders α

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
ht : ∃ s S, MeasurableSet S ∧ t = cylinder s S
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
⊢ ∃ s S, MeasurableSet S ∧ cylinder s₁ S₁ ∩ t = cylinder s S

Tactic:
obtain ⟨s₂, S₂, hS₂, rfl⟩ := ht

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ ∃ s S, MeasurableSet S ∧ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder s S

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s ∩ t ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders] at *

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S
ht : ∃ s S, MeasurableSet S ∧ t = cylinder s S
⊢ ∃ s_1 S, MeasurableSet S ∧ s ∩ t = cylinder s_1 S

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁)

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ ∃ s S, MeasurableSet S ∧ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder s S

Tactic:
refine ⟨s₁ ∪ s₂,
  Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
    {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

Tactic:
exact inter_cylinder _ _ _ _

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet {f | Finset.restrict₂ ⋯ f ∈ S₂}

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₂

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ {f | Finset.restrict₂ ⋯ f ∈ S₂})

Tactic:
refine MeasurableSet.inter ?_ ?_

Result:
case intro.intro.intro.intro.intro.intro.refine_1.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (Finset.restrict₂ ⋯ ⁻¹' S₁)

case intro.intro.intro.intro.intro.intro.refine_1.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
hS₂ : MeasurableSet S₂
⊢ MeasurableSet {f | Finset.restrict₂ ⋯ f ∈ S₂}

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S
ht : ∃ s S, MeasurableSet S ∧ t = cylinder s S
⊢ ∃ s_1 S, MeasurableSet S ∧ s ∩ t = cylinder s_1 S

Tactic:
obtain ⟨s₁, S₁, hS₁, rfl⟩ := hs

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
ht : ∃ s S, MeasurableSet S ∧ t = cylinder s S
s₁ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
hS₁ : MeasurableSet S₁
⊢ ∃ s S, MeasurableSet S ∧ cylinder s₁ S₁ ∩ t = cylinder s S