awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi (X := α) ≤ generateFrom (measurableCylinders α)

Tactic:
iSup_le fun i ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
a : ∀ (i : ι), MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i) ≤ generateFrom (measurableCylinders α)
⊢ MeasurableSpace.pi (X := α) ≤ generateFrom (measurableCylinders α)

Tactic:
refine iSup_le fun i ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i) ≤ generateFrom (measurableCylinders α)

Tactic:
(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_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
a :
  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 (measurableCylinders α)
⊢ MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i) ≤ generateFrom (measurableCylinders α)

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_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ 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 (measurableCylinders α)

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

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
a :
  ∀ (x : Set ((i : ι) → α i)),
    Membership.mem (γ := 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})
        x →
      x ∈ measurableCylinders α
⊢ 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 (measurableCylinders α)

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

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
x : Set ((i : ι) → α i)
a :
  ∀ (x_1 : (i : ι) → Set (α i)),
    (∀ (i : ι), MeasurableSet (x_1 i)) →
      eval (β := α) i ⁻¹' x_1 i = x →
        ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ x = cylinder (α := α) s S
⊢ Membership.mem (γ := 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})
      x →
    x ∈ measurableCylinders α

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

Premises used: forall_true_left, Set.singleton_pi, and_imp, Set.mem_image, forall_exists_index, Set.mem_pi, Set.mem_setOf_eq, Set.mem_univ, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ eval (β := α) i ⁻¹' t i = cylinder (α := α) s S

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

Premises used: Finset.mem_singleton_self, setOf, Membership.mem, measurable_pi_apply, Subtype.mk, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
a :
  eval (β := α) i ⁻¹' t i =
    cylinder (α := α) {i}
      {f : (i_1 : ↥{i}) → α (↑i_1 : ι) |
        Membership.mem (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι)) (t i)
          (f (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))}
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), 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), ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
a :
  ∀ (x : (x : ι) → α x),
    x ∈ eval (β := α) i ⁻¹' t i ↔
      Membership.mem (γ := Set ((x : ι) → α x))
        (cylinder (α := α) {i}
          {f : (i_1 : ↥{i}) → α (↑i_1 : ι) |
            Membership.mem (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
              (t i) (f (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))})
        x
⊢ eval (β := α) i ⁻¹' t i =
    cylinder (α := α) {i}
      {f : (i_1 : ↥{i}) → α (↑i_1 : ι) |
        Membership.mem (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι)) (t i)
          (f (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))}

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : 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 ↔
    Membership.mem (γ := Set ((x : ι) → α x))
      (cylinder (α := α) {i}
        {f : (i_1 : ↥{i}) → α (↑i_1 : ι) |
          Membership.mem (α := α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
            (t i) (f (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))})
      x

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

Premises used: Finset.restrict, Set.mem_setOf_eq, Function.eval, MeasureTheory.mem_cylinder, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
h :
  ∀ (s : Set ((i : ℕ) → X i)),
    s ∈ measurableCylinders X ↔
      Membership.mem (γ := Set (Set ((i : ℕ) → X i)))
        (⋃ (a : ℕ),
          ⋃ (S : Set ((i : ↥(Finset.Iic a)) → X (↑i : ℕ))),
            ⋃ (_ : MeasurableSet S), {cylinder (α := X) (Finset.Iic a) S})
        s
⊢ measurableCylinders X =
    ⋃ (a : ℕ),
      ⋃ (S : Set ((i : ↥(Finset.Iic a)) → X (↑i : ℕ))), ⋃ (_ : MeasurableSet S), {cylinder (α := X) (Finset.Iic a) S}

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
s : Set ((i : ℕ) → X i)
h :
  (∃ (s_1 : Finset ℕ) (S : Set ((i : ↥s_1) → X (↑i : ℕ))), MeasurableSet S ∧ s = cylinder (α := X) s_1 S) ↔
    ∃ (i : ℕ) (i_1 : Set ((i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ℕ))),
      MeasurableSet i_1 ∧ Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {cylinder (α := X) (Finset.Iic i) i_1} s
⊢ s ∈ measurableCylinders X ↔
    Membership.mem (γ := Set (Set ((i : ℕ) → X i)))
      (⋃ (a : ℕ),
        ⋃ (S : Set ((i : ↥(Finset.Iic a)) → X (↑i : ℕ))), ⋃ (_ : MeasurableSet S), {cylinder (α := X) (Finset.Iic a) S})
      s

Tactic:
simp only [mem_measurableCylinders, exists_prop, mem_iUnion]

Premises used: Set.mem_iUnion, exists_prop, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
s : Set ((i : ℕ) → X i)
⊢ (∃ (s_1 : Finset ℕ) (S : Set ((i : ↥s_1) → X (↑i : ℕ))), MeasurableSet S ∧ s = cylinder (α := X) s_1 S) ↔
    ∃ (i : ℕ) (i_1 : Set ((i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ℕ))),
      MeasurableSet i_1 ∧ Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {cylinder (α := X) (Finset.Iic i) i_1} s

Tactic:
⟨?_, fun ⟨N, S, mS, s_eq⟩ ↦ ⟨Finset.Iic N, S, mS, s_eq⟩⟩

Premises used: MeasurableSet, Exists, MeasureTheory.cylinder, And, And.intro, Iff.intro, Exists.intro, Finset.Iic, Eq, _private.0.MeasureTheory.measurableCylinders_nat.match_1
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
s : Set ((i : ℕ) → X i)
h :
  (∃ (s_1 : Finset ℕ) (S : Set ((i : ↥s_1) → X (↑i : ℕ))), MeasurableSet S ∧ s = cylinder (α := X) s_1 S) →
    ∃ (i : ℕ) (i_1 : Set ((i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ℕ))),
      MeasurableSet i_1 ∧ Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {cylinder (α := X) (Finset.Iic i) i_1} s
⊢ (∃ (s_1 : Finset ℕ) (S : Set ((i : ↥s_1) → X (↑i : ℕ))), MeasurableSet S ∧ s = cylinder (α := X) s_1 S) ↔
    ∃ (i : ℕ) (i_1 : Set ((i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ℕ))),
      MeasurableSet i_1 ∧ Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {cylinder (α := X) (Finset.Iic i) i_1} s

Tactic:
refine ⟨?_, fun ⟨N, S, mS, s_eq⟩ ↦ ⟨Finset.Iic N, S, mS, s_eq⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X (↑i : ℕ))
mS : MeasurableSet S
⊢ ∃ (i : ℕ) (i_1 : Set ((i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ℕ))),
    MeasurableSet i_1 ∧
      Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {cylinder (α := X) (Finset.Iic i) i_1} (cylinder (α := X) t S)

Tactic:
⟨t.sup id, Finset.restrict₂ t.subset_Iic_sup_id ⁻¹' S,
    Finset.measurable_restrict₂ _ mS, ?_⟩

Premises used: Finset.measurable_restrict₂, id, Set.preimage, And.intro, Exists.intro, Finset.sup, Finset.restrict₂, Finset.subset_Iic_sup_id
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X (↑i : ℕ))
mS : MeasurableSet S
h :
  Membership.mem (γ := Set (Set ((i : ℕ) → X i)))
    {cylinder (α := X) (Finset.Iic (t.sup id)) (Finset.restrict₂ (π := X) ⋯ ⁻¹' S)} (cylinder (α := X) t S)
⊢ ∃ (i : ℕ) (i_1 : Set ((i_1 : ↥(Finset.Iic i)) → X (↑i_1 : ℕ))),
    MeasurableSet i_1 ∧
      Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {cylinder (α := X) (Finset.Iic i) i_1} (cylinder (α := X) t S)

Tactic:
refine ⟨t.sup id, Finset.restrict₂ t.subset_Iic_sup_id ⁻¹' S,
    Finset.measurable_restrict₂ _ mS, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X (↑i : ℕ))
mS : MeasurableSet S
h : Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {t.restrict (π := X) ⁻¹' S} (t.restrict (π := X) ⁻¹' S)
⊢ Membership.mem (γ := Set (Set ((i : ℕ) → X i)))
    {(Finset.Iic (t.sup id)).restrict (π := X) ⁻¹' Finset.restrict₂ (π := X) ⋯ ⁻¹' S} (t.restrict (π := X) ⁻¹' S)

Tactic:
rw [← preimage_comp, Finset.restrict₂_comp_restrict]

Premises used: Set.preimage_comp, Finset.restrict₂_comp_restrict
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X (↑i : ℕ))
mS : MeasurableSet S
⊢ Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {t.restrict (π := X) ⁻¹' S} (t.restrict (π := X) ⁻¹' S)

Tactic:
mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
t : Finset ℕ
S : Set ((i : ↥t) → X (↑i : ℕ))
mS : MeasurableSet S
⊢ Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {t.restrict (π := X) ⁻¹' S} (t.restrict (π := X) ⁻¹' S)

Tactic:
exact mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
⊢ Eq (α := MeasurableSpace ((i : ι) → X i)) (cylinderEvents (X := X) univ) (MeasurableSpace.pi (X := X))

Tactic:
simp [cylinderEvents, MeasurableSpace.pi]

Premises used: MeasureTheory.cylinderEvents, MeasurableSpace.pi
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ₁ Δ₂ : Set ι
h : Δ₁ ⊆ Δ₂
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (cylinderEvents (X := X) Δ₁) (cylinderEvents (X := X) Δ₂)

Tactic:
biSup_mono h

Premises used: biSup_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (cylinderEvents (X := X) Δ) (MeasurableSpace.pi (X := X))

Tactic:
simpa using cylinderEvents_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.cylinderEvents_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
g : α → (i : ι) → X i
simp_rw :
  MeasurableSpace.comap g (cylinderEvents (X := X) Δ) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun (a : α) ↦ g a i) (m i) ≤ mα
simp_rw₁ :
  MeasurableSpace.comap g (⨆ i ∈ Δ, MeasurableSpace.comap (fun (σ : (i : ι) → X i) ↦ σ i) (m i)) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun (a : α) ↦ g a i) (m i) ≤ mα
simp_rw₂ :
  ⨆ i ∈ Δ, MeasurableSpace.comap g (MeasurableSpace.comap (fun (σ : (i : ι) → X i) ↦ σ i) (m i)) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun (a : α) ↦ g a i) (m i) ≤ mα
simp_rw₃ :
  ⨆ i ∈ Δ, MeasurableSpace.comap ((fun (σ : (i : ι) → X i) ↦ σ i) ∘ g) (m i) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun (a : α) ↦ g a i) (m i) ≤ mα
simp_rw₄ :
  ⨆ i ∈ Δ, MeasurableSpace.comap (fun (x : α) ↦ g x i) (m i) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun (a : α) ↦ g a i) (m i) ≤ mα
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i

Tactic:
simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]

Premises used: MeasurableSpace.comap_comp, measurable_iff_comap_le, MeasureTheory.cylinderEvents, MeasurableSpace.comap_iSup, Function.comp_def, iSup_le_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
hi : i ∈ Δ
⊢ Measurable (β := X i) fun (f : (i : ι) → X i) ↦ f i

Tactic:
measurable_cylinderEvents_iff.1 measurable_id hi

Premises used: measurable_id, MeasureTheory.measurable_cylinderEvents_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
g : α → (i : ι) → X i
hi : i ∈ Δ
hg : Measurable g
⊢ Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i

Tactic:
(measurable_cylinderEvent_apply hi).comp hg

Premises used: Measurable.comp, MeasureTheory.measurable_cylinderEvent_apply
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
f : α → (i : ι) → X i
hf : ∀ (i : ι), Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ f a i
⊢ Measurable f

Tactic:
measurable_pi_iff.mpr hf

Premises used: Iff.mpr, measurable_pi_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
rw : ∀ ⦃i_1 : ι⦄, i_1 ∈ Δ → Measurable (β := X i_1) fun (a : ((i : ι) → X i) × X i) ↦ update (β := X) a.1 i a.2 i_1
⊢ Measurable (β := (i : ι) → X i) fun (p : ((i : ι) → X i) × X i) ↦ update (β := X) p.1 i p.2

Tactic:
rw [measurable_cylinderEvents_iff]

Premises used: MeasureTheory.measurable_cylinderEvents_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
dsimp :
  Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ X x) a.2 ⋯ else a.1 j
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ update (β := X) a.1 i a.2 j

Tactic:
dsimp [update]

Premises used: Function.update
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
pos :
  ∀ (h : j = i),
    Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ X x) a.2 ⋯
neg : ∀ (h : ¬j = i), Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ a.1 j
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ X x) a.2 ⋯ else a.1 j

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
h : j = i
pos : Measurable (β := X j) fun (a : ((i : ι) → X i) × X j) ↦ Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ X x) a.2 ⋯
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ X x) a.2 ⋯

Tactic:
subst h
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X j) ↦ a.2

Tactic:
measurable_snd

Premises used: measurable_snd
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X j) ↦ a.2

Tactic:
exact measurable_snd

Premises used: measurable_snd
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
h : ¬j = i
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ a.1 j

Tactic:
measurable_cylinderEvents_iff.1 measurable_fst hj

Premises used: MeasureTheory.measurable_cylinderEvents_iff, Iff.mp, measurable_fst
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
h : ¬j = i
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ a.1 j

Tactic:
exact measurable_cylinderEvents_iff.1 measurable_fst hj

Premises used: MeasureTheory.measurable_cylinderEvents_iff, Iff.mp, measurable_fst
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst : Unique ι
simp_rw : Measurable (β := X default) fun (x : X default) ↦ x
⊢ Measurable (α := X default) (uniqueElim (α := X))

Tactic:
simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]

Premises used: measurable_pi_iff, Unique.forall_iff, uniqueElim_default
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst : Unique ι
⊢ Measurable (β := X default) fun (x : X default) ↦ x

Tactic:
measurable_id

Premises used: measurable_id
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst : Unique ι
⊢ Measurable (β := X default) fun (x : X default) ↦ x

Tactic:
exact measurable_id

Premises used: measurable_id
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
f : (a : ι) → X a
a : ι
inst : DecidableEq ι
⊢ Measurable (update (β := X) f a)

Tactic:
measurable_update_cylinderEvents'.comp measurable_prodMk_left

Premises used: Function.update, Measurable.comp, MeasureTheory.measurable_update_cylinderEvents', dite, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
a : ι
inst : DecidableEq ι
x : X a
⊢ Measurable (β := (i : ι) → X i) fun (x_1 : (i : ι) → X i) ↦ update (β := X) x_1 a x

Tactic:
measurable_update_cylinderEvents'.comp measurable_prodMk_right

Premises used: Function.update, Measurable.comp, measurable_prodMk_right, MeasureTheory.measurable_update_cylinderEvents', dite
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
rw : ∀ (a : (↑Δ : Type u_2)), Measurable (β := X (↑a : ι)) fun (x : (i : ι) → X i) ↦ Δ.restrict (π := X) x a
⊢ Measurable (α := (i : ι) → X i) (Δ.restrict (π := X))

Tactic:
rw [@measurable_pi_iff]

Premises used: measurable_pi_iff
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
⊢ ∀ (a : (↑Δ : Type u_2)), Measurable (β := X (↑a : ι)) fun (x : (i : ι) → X i) ↦ Δ.restrict (π := X) x a

Tactic:
fun i ↦ measurable_cylinderEvent_apply i.2

Premises used: MeasureTheory.measurable_cylinderEvent_apply, Set.restrict, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
⊢ ∀ (a : (↑Δ : Type u_2)), Measurable (β := X (↑a : ι)) fun (x : (i : ι) → X i) ↦ Δ.restrict (π := X) x a

Tactic:
exact fun i ↦ measurable_cylinderEvent_apply i.2

Premises used: MeasureTheory.measurable_cylinderEvent_apply
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ (i : ι), Membership.mem (γ := Set (Set (α i))) {s : Set (α i) | MeasurableSet s} univ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ Set.Countable.{u_2} (α := ι) ∅ ∧
    Eq (α := Set ((i : ι) → α i)) ∅ (preimage (β := (a : (↑∅ : Type u_2)) → α (↑a : ι)) (restrict (π := α) ∅) ∅)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
refine_1 :
  ∀ (t : Set ((a : ι) → α a))
    (ht :
      Membership.mem (γ := Set (Set ((a : ι) → α a)))
        (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}) t),
    ∃ (I : Set ι) (t_1 : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ t = I.restrict (π := α) ⁻¹' t_1
refine_2 :
  ∀ (t : Set ((a : ι) → α a)) (htm : MeasurableSet t),
    (∃ (I : Set ι) (t_1 : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ t = I.restrict (π := α) ⁻¹' t_1) →
      ∃ (I : Set ι) (t_1 : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ tᶜ = I.restrict (π := α) ⁻¹' t_1
refine_3 :
  ∀ (f : ℕ → Set ((a : ι) → α a)),
    Pairwise (Disjoint on f) →
      ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ),
            ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))),
              I.Countable ∧ f i = I.restrict (π := α) ⁻¹' t) →
          ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))),
            I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ s = I.restrict (π := α) ⁻¹' t

Tactic:
refine induction_on_inter generateFrom_squareCylinders.symm
    (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp))
    ⟨∅, ∅, by simp⟩ ?_ ?_ ?_ s hs