awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
a :
  LE.le (α := MeasurableSpace ((x : ι) → α x))
    (generateFrom
      ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
⊢ LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))

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

Premises used: MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton, LE.le.trans
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ LE.le (α := MeasurableSpace ((x : ι) → α x))
    (generateFrom
      ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))

Tactic:
MeasurableSpace.generateFrom_mono ?_

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
a :
  Subset (α := Set (Set ((i : ι) → α i)))
    ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
    (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
⊢ LE.le (α := MeasurableSpace ((x : ι) → α x))
    (generateFrom
      ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))

Tactic:
refine MeasurableSpace.generateFrom_mono ?_

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
a :
  Subset (α := Set (Set ((i : ι) → α i)))
    ((fun (t : (i : ι) → Set (α i)) ↦ (↑{i} : Set ι).pi (α := α) t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
    (⋃ (s : Finset ι),
      (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
⊢ Subset (α := Set (Set ((i : ι) → α i)))
    ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
    (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})

Tactic:
rw [← Finset.coe_singleton, squareCylinders_eq_iUnion_image]

Premises used: Finset.coe_singleton, MeasureTheory.squareCylinders_eq_iUnion_image
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ Subset (α := Set (Set ((i : ι) → α i)))
    ((fun (t : (i : ι) → Set (α i)) ↦ (↑{i} : Set ι).pi (α := α) t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
    (⋃ (s : Finset ι),
      (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})

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

Premises used: MeasurableSet, Set.univ, setOf, Set.subset_iUnion, SetLike.coe, Set.image, Set.pi, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ Subset (α := Set (Set ((i : ι) → α i)))
    ((fun (t : (i : ι) → Set (α i)) ↦ (↑{i} : Set ι).pi (α := α) t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
    (⋃ (s : Finset ι),
      (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | 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 ι)

Premises used: MeasurableSet, Set.univ, setOf, Set.subset_iUnion, SetLike.coe, Set.image, Set.pi, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
f : (i : ι) → α i
⊢ f ∈ cylinder (α := α) s S ↔ s.restrict (π := α) f ∈ S

Tactic:
mem_preimage

Premises used: Set.Mem, MeasureTheory.cylinder, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
rw : Eq (α := Set ((i : ι) → α i)) (s.restrict (π := α) ⁻¹' ∅) ∅
rw₁ rw₂ : Eq (α := Set ((i : ι) → α i)) ∅ ∅
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅

Tactic:
rw [cylinder, preimage_empty]

Premises used: Set.preimage_empty, MeasureTheory.cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
rw : Eq (α := Set ((i : ι) → α i)) (s.restrict (π := α) ⁻¹' univ) univ
rw₁ rw₂ : Eq (α := Set ((i : ι) → α i)) univ univ
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s univ) univ

Tactic:
rw [cylinder, preimage_univ]

Premises used: MeasureTheory.cylinder, Set.preimage_univ
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : S = ∅
rw : Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅
⊢ cylinder (α := α) s S = ∅

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : S = ∅
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅

Tactic:
cylinder_empty _

Premises used: MeasureTheory.cylinder_empty
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : S = ∅
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅

Tactic:
exact cylinder_empty _

Premises used: MeasureTheory.cylinder_empty
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
refine : ∀ (h : cylinder (α := α) s S = ∅), S = ∅
⊢ cylinder (α := α) s S = ∅ ↔ S = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by (rw [h]; exact cylinder_empty _)⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
by_contra : ∀ (hS : ¬S = ∅), False
⊢ S = ∅

Tactic:
by_contra hS
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : ¬S = ∅
⊢ S.Nonempty

Tactic:
rw [← Ne, ← nonempty_iff_ne_empty] at hS

Premises used: Ne, Set.nonempty_iff_ne_empty
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
⊢ f ∈ S

Tactic:
have hf : f ∈ S := hS.choose_spec
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
rw : s.restrict (π := α) f' ∈ S
⊢ f' ∈ cylinder (α := α) s S

Tactic:
rw [mem_cylinder]

Premises used: MeasureTheory.mem_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
⊢ s.restrict (π := α) f' ∈ S

Tactic:
simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']

Premises used: Finset.coe_mem, dif_pos, Finset.restrict_def
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
⊢ f' ∈ cylinder (α := α) s S

Tactic:
have hf' : f' ∈ cylinder s S := by
    rw [mem_cylinder]
    simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
hf' : f' ∈ cylinder (α := α) s S
⊢ Membership.mem (γ := Set ((i : ι) → α i)) ∅ f'

Tactic:
rw [h] at hf'
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
hf' : Membership.mem (γ := Set ((i : ι) → α i)) ∅ f'
⊢ False

Tactic:
notMem_empty _ hf'

Premises used: Set.notMem_empty
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
hf' : Membership.mem (γ := Set ((i : ι) → α i)) ∅ f'
⊢ False

Tactic:
exact notMem_empty _ hf'

Premises used: Set.notMem_empty
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
let let₁ let₂ : False
let₃ :
  let f' : (i : ι) → α i := fun (i : ι) ↦
    if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i;
  ∀ (hf' : f' ∈ cylinder (α := α) s S), False
let₄ :
  let f' : (i : ι) → α i := fun (i : ι) ↦
    if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i;
  ∀ (hf' : Membership.mem (γ := Set ((i : ι) → α i)) ∅ f'), False
⊢ False

Tactic:
classical
  let f' : ∀ i, α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
  have hf' : f' ∈ cylinder s S := by
    rw [mem_cylinder]
    simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']
  rw [h] at hf'
  exact notMem_empty _ hf'
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
inst : DecidableEq ι
⊢ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
    cylinder (α := α) (s₁ ∪ s₂) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' S₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, Finset.restrict, Set.inter, MeasureTheory.cylinder, Set.preimage, Finset.restrict₂, Multiset.ndunion, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : ↥s) → α (↑i : ι))
⊢ cylinder (α := α) s S₁ ∩ cylinder (α := α) s S₂ = cylinder (α := α) s (S₁ ∩ S₂)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, MeasureTheory.cylinder, Set.preimage, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : ↥s₁) → α (↑i : ι))
S₂ : Set ((i : ↥s₂) → α (↑i : ι))
inst : DecidableEq ι
⊢ cylinder (α := α) s₁ S₁ ∪ cylinder (α := α) s₂ S₂ =
    cylinder (α := α) (s₁ ∪ s₂) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ (π := α) ⋯ ⁻¹' S₂)

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Finset.restrict, MeasureTheory.cylinder, Set.preimage, Finset.restrict₂, Multiset.ndunion, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : ↥s) → α (↑i : ι))
⊢ cylinder (α := α) s S₁ ∪ cylinder (α := α) s S₂ = cylinder (α := α) s (S₁ ∪ S₂)

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, MeasureTheory.cylinder, Set.preimage, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : ∀ (f : (i : ι) → α i), f ∈ (cylinder (α := α) s S)ᶜ ↔ f ∈ cylinder (α := α) s Sᶜ
⊢ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s Sᶜ

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
f : (i : ι) → α i
⊢ f ∈ (cylinder (α := α) s S)ᶜ ↔ f ∈ cylinder (α := α) s Sᶜ

Tactic:
simp only [mem_compl_iff, mem_cylinder]

Premises used: MeasureTheory.mem_cylinder, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α (↑i : ι))
h : ∀ (f : (i : ι) → α i), f ∈ cylinder (α := α) s S \ cylinder (α := α) s T ↔ f ∈ cylinder (α := α) s (S \ T)
⊢ cylinder (α := α) s S \ cylinder (α := α) s T = cylinder (α := α) s (S \ T)

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α (↑i : ι))
f : (i : ι) → α i
⊢ f ∈ cylinder (α := α) s S \ cylinder (α := α) s T ↔ f ∈ cylinder (α := α) s (S \ T)

Tactic:
simp only [mem_diff, mem_cylinder]

Premises used: Set.mem_diff, MeasureTheory.mem_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
rw :
  ∀ (h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder (α := α) I S ↔ x ∈ cylinder (α := α) J T) (hJI : J ⊆ I),
    S = Finset.restrict₂ (π := α) hJI ⁻¹' T
⊢ S = Finset.restrict₂ (π := α) hJI ⁻¹' T

Tactic:
rw [Set.ext_iff] at h_eq

Premises used: Set.ext_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder (α := α) I S ↔ x ∈ cylinder (α := α) J T
hJI : J ⊆ I
⊢ ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T

Tactic:
simp only [mem_cylinder] at h_eq

Premises used: MeasureTheory.mem_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
h : ∀ (f : (i : ↥I) → α (↑i : ι)), f ∈ S ↔ f ∈ Finset.restrict₂ (π := α) hJI ⁻¹' T
⊢ S = Finset.restrict₂ (π := α) hJI ⁻¹' T

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
h : f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
⊢ f ∈ S ↔ f ∈ Finset.restrict₂ (π := α) hJI ⁻¹' T

Tactic:
simp only [mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
⊢ (I.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      S ↔
    (J.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      T

Tactic:
specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i

Premises used: Membership.mem, Nonempty.some, dite, Subtype.mk
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
f : (i : ↥I) → α (↑i : ι)
h_eq :
  (I.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      S ↔
    (J.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      T
⊢ ∀ (j : ↥J), (↑j : ι) ∈ I

Tactic:
have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
f : (i : ↥I) → α (↑i : ι)
h_eq :
  (I.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      S ↔
    (J.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      T
h_mem : ∀ (j : ↥J), (↑j : ι) ∈ I
⊢ f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T

Tactic:
simpa only [Finset.restrict_def, Finset.coe_mem, dite_true, h_mem] using h_eq

Premises used: Finset.coe_mem, Finset.restrict_def, dite_true
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
h :
  ∀
    (h_eq :
      (I.restrict (π := α) fun (i : ι) ↦
            if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
          S ↔
        (J.restrict (π := α) fun (i : ι) ↦
            if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
          T),
    f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
h₁ :
  ∀
    (h_eq :
      (I.restrict (π := α) fun (i : ι) ↦
            if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
          S ↔
        (J.restrict (π := α) fun (i : ι) ↦
            if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
          T)
    (h_mem : ∀ (j : ↥J), (↑j : ι) ∈ I), f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
⊢ f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T

Tactic:
classical
  specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i
  have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop
  simpa only [Finset.restrict_def, Finset.coe_mem, dite_true, h_mem] using h_eq

Premises used: Finset.coe_mem, Finset.restrict_def, dite_true
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
J : Finset ι
h : ∀ (f : (i : ι) → α i), f ∈ cylinder (α := α) I S ↔ f ∈ cylinder (α := α) (I ∪ J) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
J : Finset ι
f : (i : ι) → α i
⊢ f ∈ cylinder (α := α) I S ↔ f ∈ cylinder (α := α) (I ∪ J) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)

Tactic:
simp only [mem_cylinder, Finset.restrict_def, Finset.restrict₂_def, mem_preimage]

Premises used: Finset.restrict₂_def, MeasureTheory.mem_cylinder, Finset.restrict_def, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
T : Set ((i : ↥t) → α (↑i : ι))
inst_1 : DecidableEq ι
simp_rw :
  cylinder (α := α) s S ∩ cylinder (α := α) t T ⊆ ∅ ↔
    Subset (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι)))
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T) ∅
simp_rw₁ :
  cylinder (α := α) s S ∩ cylinder (α := α) t T = ∅ ↔
    Eq (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T)
      ∅
simp_rw₂ :
  cylinder (α := α) (s ∪ t) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T) = ∅ ↔
    Eq (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T)
      ∅
⊢ Disjoint (cylinder (α := α) s S) (cylinder (α := α) t T) ↔
    Disjoint (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' T)

Tactic:
simp_rw [Set.disjoint_iff, subset_empty_iff, inter_cylinder, cylinder_eq_empty_iff]

Premises used: MeasureTheory.inter_cylinder, MeasureTheory.cylinder_eq_empty_iff, Set.subset_empty_iff, Set.disjoint_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → TopologicalSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hs : IsClosed S
⊢ IsClosed (MeasureTheory.cylinder (α := α) s S)

Tactic:
hs.preimage (continuous_pi fun _ ↦ continuous_apply _)

Premises used: Finset.restrict, continuous_pi, MeasureTheory.cylinder, continuous_apply, IsClosed.preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
⊢ MeasurableSet (cylinder (α := α) s S)

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

Premises used: measurable_pi_lambda, Finset.restrict, measurable_pi_apply, MeasureTheory.cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_3
M : Type u_1
inst : Zero M
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
c : M
x y : (i : ι) → α i
hxy : ∀ i ∈ (↑I : Set ι), x i = y i
⊢ x ∈ cylinder (α := α) I S ↔ y ∈ cylinder (α := α) I S

Tactic:
simp [Finset.restrict_def, hxy]

Premises used: Finset.restrict_def