awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
simp_rw : ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → α (↑i_1 : ι))) (_ : MeasurableSet i_1), ∅ = cylinder (α := α) i i_1
⊢ ∅ ∈ measurableCylinders α

Tactic:
simp_rw [measurableCylinders, mem_iUnion, mem_singleton_iff]

Premises used: MeasureTheory.measurableCylinders, Set.mem_iUnion, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → α (↑i_1 : ι))) (_ : MeasurableSet i_1), ∅ = cylinder (α := α) i i_1

Tactic:
⟨∅, ∅, MeasurableSet.empty, (cylinder_empty _).symm⟩

Premises used: MeasureTheory.cylinder_empty, MeasurableSet.empty, Exists.intro, EmptyCollection.emptyCollection, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → α (↑i_1 : ι))) (_ : MeasurableSet i_1), ∅ = cylinder (α := α) i i_1

Tactic:
exact ⟨∅, ∅, MeasurableSet.empty, (cylinder_empty _).symm⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
simp_rw :
  Membership.mem (γ := Set (Set ((i : ι) → α i)))
      (⋃ (s : Finset ι), ⋃ (S : Set ((i : ↥s) → α (↑i : ι))), ⋃ (_ : MeasurableSet S), {cylinder (α := α) s S}) t ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
simp_rw₁ :
  (∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → α (↑i_1 : ι))) (_ : MeasurableSet i_1),
      Membership.mem (γ := Set (Set ((i : ι) → α i))) {cylinder (α := α) i i_1} t) ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
simp_rw₂ :
  (∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → α (↑i_1 : ι))),
      MeasurableSet i_1 ∧ Membership.mem (γ := Set (Set ((i : ι) → α i))) {cylinder (α := α) i i_1} t) ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
⊢ t ∈ measurableCylinders α ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S

Tactic:
simp_rw [measurableCylinders, mem_iUnion, exists_prop, mem_singleton_iff]

Premises used: MeasureTheory.measurableCylinders, Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
obtain :
  ∀ (I : Finset ι) (t : Set ((i : ↥I) → α (↑i : ι))) (mt : MeasurableSet t)
    (hs : cylinder (α := α) I t ∈ measurableCylinders α), MeasurableSet (cylinder (α := α) I t)
⊢ MeasurableSet s

Tactic:
obtain ⟨I, t, mt, rfl⟩ := (mem_measurableCylinders s).1 hs

Premises used: mt, Iff.mp, MeasureTheory.mem_measurableCylinders, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
I : Finset ι
t : Set ((i : ↥I) → α (↑i : ι))
mt : MeasurableSet t
hs : cylinder (α := α) I t ∈ measurableCylinders α
⊢ MeasurableSet (cylinder (α := α) I t)

Tactic:
mt.cylinder

Premises used: MeasurableSet.cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
I : Finset ι
t : Set ((i : ↥I) → α (↑i : ι))
mt : MeasurableSet t
hs : cylinder (α := α) I t ∈ measurableCylinders α
⊢ MeasurableSet (cylinder (α := α) I t)

Tactic:
exact mt.cylinder

Premises used: MeasurableSet.cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
ht : t ∈ measurableCylinders α
⊢ MeasurableSet (set (α := α) (t := t) ht)

Tactic:
((mem_measurableCylinders t).mp ht).choose_spec.choose_spec.left

Premises used: Exists.choose_spec, Set.Mem, setOf, And.left, MeasureTheory.measurableCylinders.set, Iff.mp, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
ht : t ∈ measurableCylinders α
⊢ t = cylinder (α := α) (finset (α := α) (t := t) ht) (set (α := α) (t := t) ht)

Tactic:
((mem_measurableCylinders t).mp ht).choose_spec.choose_spec.right

Premises used: Exists.choose_spec, Set.Mem, setOf, And.right, MeasureTheory.measurableCylinders.set, MeasureTheory.measurableCylinders.finset, Iff.mp, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
rw :
  ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
    MeasurableSet S_1 ∧ cylinder (α := α) s S = cylinder (α := α) s_1 S_1
⊢ cylinder (α := α) s S ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders]

Premises used: MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
⊢ ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
    MeasurableSet S_1 ∧ cylinder (α := α) s S = cylinder (α := α) s_1 S_1

Tactic:
⟨s, S, hS, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
⊢ ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
    MeasurableSet S_1 ∧ cylinder (α := α) s S = cylinder (α := α) s_1 S_1

Tactic:
exact ⟨s, S, hS, rfl⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
rw :
  ∀ (hs : ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s = cylinder (α := α) s_1 S)
    (ht : ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S),
    ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s ∩ t = cylinder (α := α) s_1 S
⊢ s ∩ t ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders] at *

Premises used: MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s = cylinder (α := α) s_1 S
ht : ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
obtain :
  ∀ (s₁ : Finset ι) (S₁ : Set ((i : ↥s₁) → α (↑i : ι))) (hS₁ : MeasurableSet S₁),
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
      MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ t = cylinder (α := α) s S
⊢ ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s ∩ t = cylinder (α := α) s_1 S

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

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
ht : ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
obtain :
  ∀ (s₂ : Finset ι) (S₂ : Set ((i : ↥s₂) → α (↑i : ι))) (hS₂ : MeasurableSet S₂),
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
      MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ = cylinder (α := α) s S
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ t = cylinder (α := α) s S

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

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ = cylinder (α := α) s S

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

Premises used: setOf, Membership.mem, Finset.subset_union_left, Inter.inter, Set.preimage, And.intro, Exists.intro, Finset.restrict₂, Union.union, Finset.subset_union_right
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
refine_1 :
  MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})
refine_2 :
  cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
    cylinder (α := α) (s₁ ∪ s₂)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    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₂}, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})

Tactic:
MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
refine_1 : MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι)) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁)
refine_1₁ :
  MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂}
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})

Tactic:
refine MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι)) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁)

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

Premises used: measurable_pi_lambda, measurable_pi_apply, Finset.restrict₂
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι)) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁)

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

Premises used: measurable_pi_lambda, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂}

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

Premises used: measurable_pi_lambda, Set.Mem, setOf, measurable_pi_apply, Set.preimage, Finset.restrict₂
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂}

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

Premises used: measurable_pi_lambda, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
    cylinder (α := α) (s₁ ∪ s₂)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})

Tactic:
inter_cylinder _ _ _ _

Premises used: MeasureTheory.inter_cylinder, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
⊢ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
    cylinder (α := α) (s₁ ∪ s₂)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})

Tactic:
exact inter_cylinder _ _ _ _

Premises used: MeasureTheory.inter_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s₁ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
hS₁ : MeasurableSet S₁
s₂ : Finset ι
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
hS₂ : MeasurableSet S₂
refine_1 :
  MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})
refine_2 refine_2₁ :
  cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
    cylinder (α := α) (s₁ ∪ s₂)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ = cylinder (α := α) s S

Tactic:
classical
  refine ⟨s₁ ∪ s₂,
    Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
      {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_, ?_⟩
  · refine MeasurableSet.inter ?_ ?_
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₂
  · exact inter_cylinder _ _ _ _

Premises used: MeasureTheory.inter_cylinder, measurable_pi_lambda, measurable_pi_apply, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ IsPiSystem (measurableCylinders α)

Tactic:
fun _ hS _ hT _ ↦ inter_mem_measurableCylinders hS hT

Premises used: Set.Mem, IsPiSystem, MeasureTheory.inter_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
rw :
  ∀ (hs : ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s = cylinder (α := α) s_1 S),
    ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ sᶜ = cylinder (α := α) s_1 S
⊢ sᶜ ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders] at hs ⊢

Premises used: MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s = cylinder (α := α) s_1 S
obtain :
  ∀ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))) (hS : MeasurableSet S),
    ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
      MeasurableSet S_1 ∧ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s_1 S_1
⊢ ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ sᶜ = cylinder (α := α) s_1 S

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

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
⊢ ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
    MeasurableSet S_1 ∧ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s_1 S_1

Tactic:
⟨s, Sᶜ, hS.compl, ?_⟩

Premises used: Compl.compl, MeasurableSet.compl, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
refine : (cylinder (α := α) s S)ᶜ = cylinder (α := α) s Sᶜ
⊢ ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
    MeasurableSet S_1 ∧ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s_1 S_1

Tactic:
refine ⟨s, Sᶜ, hS.compl, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
rw rw₁ : cylinder (α := α) s Sᶜ = cylinder (α := α) s Sᶜ
⊢ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s Sᶜ

Tactic:
rw [compl_cylinder]

Premises used: MeasureTheory.compl_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
rw : ∅ᶜ ∈ measurableCylinders α
⊢ univ ∈ measurableCylinders α

Tactic:
rw [← compl_empty]

Premises used: Set.compl_empty
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ ∅ᶜ ∈ measurableCylinders α

Tactic:
compl_mem_measurableCylinders (empty_mem_measurableCylinders α)

Premises used: MeasureTheory.empty_mem_measurableCylinders, Set.Mem, setOf, MeasureTheory.compl_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ ∅ᶜ ∈ measurableCylinders α

Tactic:
exact compl_mem_measurableCylinders (empty_mem_measurableCylinders α)

Premises used: MeasureTheory.empty_mem_measurableCylinders, MeasureTheory.compl_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
rw : (sᶜ ∩ tᶜ)ᶜ ∈ measurableCylinders α
⊢ s ∪ t ∈ measurableCylinders α

Tactic:
rw [union_eq_compl_compl_inter_compl]

Premises used: Set.union_eq_compl_compl_inter_compl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : 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:
compl_mem_measurableCylinders (inter_mem_measurableCylinders
    (compl_mem_measurableCylinders hs) (compl_mem_measurableCylinders ht))

Premises used: MeasureTheory.compl_mem_measurableCylinders, MeasureTheory.inter_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : 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:
exact compl_mem_measurableCylinders (inter_mem_measurableCylinders
    (compl_mem_measurableCylinders hs) (compl_mem_measurableCylinders ht))

Premises used: MeasureTheory.compl_mem_measurableCylinders, MeasureTheory.inter_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
rw : tᶜ ∩ s ∈ measurableCylinders α
⊢ s \ t ∈ measurableCylinders α

Tactic:
rw [diff_eq_compl_inter]

Premises used: Set.diff_eq_compl_inter
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ tᶜ ∩ s ∈ measurableCylinders α

Tactic:
inter_mem_measurableCylinders (compl_mem_measurableCylinders ht) hs

Premises used: MeasureTheory.compl_mem_measurableCylinders, MeasureTheory.inter_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ tᶜ ∩ s ∈ measurableCylinders α

Tactic:
exact inter_mem_measurableCylinders (compl_mem_measurableCylinders ht) hs

Premises used: MeasureTheory.compl_mem_measurableCylinders, MeasureTheory.inter_mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
a : generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi (X := α)
a₁ : MeasurableSpace.pi (X := α) ≤ generateFrom (measurableCylinders α)
⊢ generateFrom (measurableCylinders α) = MeasurableSpace.pi (X := α)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi (X := α)

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

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
a : ∀ (S : Set ((i : ι) → α i)) (hS : S ∈ measurableCylinders α), MeasurableSet S
⊢ generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi (X := α)

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

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
S : Set ((i : ι) → α i)
hS : S ∈ measurableCylinders α
a :
  ∀ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))) (hSm : MeasurableSet S)
    (hS : cylinder (α := α) s S ∈ measurableCylinders α), MeasurableSet (cylinder (α := α) s S)
⊢ MeasurableSet S

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

Premises used: Iff.mp, MeasureTheory.mem_measurableCylinders, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hSm : MeasurableSet S
hS : cylinder (α := α) s S ∈ measurableCylinders α
⊢ MeasurableSet (cylinder (α := α) s S)

Tactic:
hSm.cylinder

Premises used: MeasurableSet.cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hSm : MeasurableSet S
hS : cylinder (α := α) s S ∈ measurableCylinders α
⊢ MeasurableSet (cylinder (α := α) s S)

Tactic:
exact hSm.cylinder

Premises used: MeasurableSet.cylinder