awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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)
      ∅
⊢ Disjoint (cylinder (α := α) s S) (cylinder (α := α) t T) ↔
    Disjoint (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' T)
have simp_rw₂ : cylinder (α := α) (s ∪ t) (Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T) = ∅ ↔
  Eq (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T) ∅
Tactic: simp_rw [Set.disjoint_iff, subset_empty_iff, inter_cylinder, cylinder_eq_empty_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ ∅ ∈ measurableCylinders α
have simp_rw : ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → α (↑i_1 : ι))) (_ : MeasurableSet i_1), ∅ = cylinder (α := α) i i_1
Tactic: simp_rw [measurableCylinders, mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
⊢ t ∈ measurableCylinders α ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
have 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
Tactic: simp_rw [measurableCylinders, mem_iUnion, exists_prop, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
⊢ t ∈ measurableCylinders α ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
have 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
Tactic: simp_rw [measurableCylinders, mem_iUnion, exists_prop, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
⊢ t ∈ measurableCylinders α ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := α) s S
have 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
Tactic: simp_rw [measurableCylinders, mem_iUnion, exists_prop, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ MeasurableSet s
have obtain : ∀ (I : Finset ι) (t : Set ((i : ↥I) → α (↑i : ι))) (mt : MeasurableSet t)
  (hs : cylinder (α := α) I t ∈ measurableCylinders α), MeasurableSet (cylinder (α := α) I t)
Tactic: obtain ⟨I, t, mt, rfl⟩ := (mem_measurableCylinders s).1 hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
⊢ cylinder (α := α) s S ∈ measurableCylinders α
have rw : ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → α (↑i : ι))),
  MeasurableSet S_1 ∧ cylinder (α := α) s S = cylinder (α := α) s_1 S_1
Tactic: rw [mem_measurableCylinders]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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 α
have 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
Tactic: rw [mem_measurableCylinders] at *
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
⊢ ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ s ∩ t = cylinder (α := α) s_1 S
have 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
Tactic: obtain ⟨s₁, S₁, hS₁, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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₁
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ t = cylinder (α := α) s S
have 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
Tactic: obtain ⟨s₂, S₂, hS₂, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
have refine_1 : MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
  (Finset.restrict₂ (π := α) sorry ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) sorry f ∈ S₂})
Tactic: refine ⟨s₁ ∪ s₂,
    Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
      {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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₂})
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ = cylinder (α := α) s S
have refine_2 : cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
  cylinder (α := α) (s₁ ∪ s₂)
    (Finset.restrict₂ (π := α) sorry ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) sorry f ∈ S₂})
Tactic: refine ⟨s₁ ∪ s₂,
    Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
      {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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₂})
have refine_1 : MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι)) (Finset.restrict₂ (π := α) sorry ⁻¹' S₁)
Tactic: refine MeasurableSet.inter ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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₁)
⊢ MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
    (Finset.restrict₂ (π := α) ⋯ ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) ⋯ f ∈ S₂})
have refine_1₁ : MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
  {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) sorry f ∈ S₂}
Tactic: refine MeasurableSet.inter ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
have refine_1 : MeasurableSet (α := (i : ↥(s₁ ∪ s₂)) → α (↑i : ι))
  (Finset.restrict₂ (π := α) sorry ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) sorry f ∈ 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 _ _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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₂})
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))),
    MeasurableSet S ∧ cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ = cylinder (α := α) s S
have refine_2 : cylinder (α := α) s₁ S₁ ∩ cylinder (α := α) s₂ S₂ =
  cylinder (α := α) (s₁ ∪ s₂)
    (Finset.restrict₂ (π := α) sorry ⁻¹' S₁ ∩ {f : (i : ↥(s₁ ∪ s₂)) → α (↑i : ι) | Finset.restrict₂ (π := α) sorry f ∈ 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 _ _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ sᶜ ∈ measurableCylinders α
have 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
Tactic: rw [mem_measurableCylinders] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
⊢ ∃ (s_1 : Finset ι) (S : Set ((i : ↥s_1) → α (↑i : ι))), MeasurableSet S ∧ sᶜ = cylinder (α := α) s_1 S
have 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
Tactic: obtain ⟨s, S, hS, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
have refine : (cylinder (α := α) s S)ᶜ = cylinder (α := α) s Sᶜ
Tactic: refine ⟨s, Sᶜ, hS.compl, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
hS : MeasurableSet S
⊢ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s Sᶜ
have rw : cylinder (α := α) s Sᶜ = cylinder (α := α) s Sᶜ
Tactic: rw [compl_cylinder]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ univ ∈ measurableCylinders α
have rw : ∅ᶜ ∈ measurableCylinders α
Tactic: rw [← compl_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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 α
have rw : (sᶜ ∩ tᶜ)ᶜ ∈ measurableCylinders α
Tactic: rw [union_eq_compl_compl_inter_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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 α
have rw : tᶜ ∩ s ∈ measurableCylinders α
Tactic: rw [diff_eq_compl_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) = MeasurableSpace.pi (X := α)
have a : generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi (X := α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
a : generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi (X := α)
⊢ generateFrom (measurableCylinders α) = MeasurableSpace.pi (X := α)
have a₁ : MeasurableSpace.pi (X := α) ≤ generateFrom (measurableCylinders α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (measurableCylinders α) ≤ MeasurableSpace.pi (X := α)
have a : ∀ (S : Set ((i : ι) → α i)) (hS : S ∈ measurableCylinders α), MeasurableSet S
Tactic: refine MeasurableSpace.generateFrom_le (fun S hS ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
S : Set ((i : ι) → α i)
hS : S ∈ measurableCylinders α
⊢ MeasurableSet S
have a : ∀ (s : Finset ι) (S : Set ((i : ↥s) → α (↑i : ι))) (hSm : MeasurableSet S)
  (hS : cylinder (α := α) s S ∈ measurableCylinders α), MeasurableSet (cylinder (α := α) s S)
Tactic: obtain ⟨s, S, hSm, rfl⟩ := (mem_measurableCylinders _).mp hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi (X := α) ≤ generateFrom (measurableCylinders α)
have a : ∀ (i : ι), MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i) ≤ generateFrom (measurableCylinders α)
Tactic: refine iSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i) ≤ generateFrom (measurableCylinders α)
have 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 α)
Tactic: refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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 α)
have 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 α
Tactic: refine MeasurableSpace.generateFrom_mono (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
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 α
have 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
Tactic: simp only [singleton_pi, mem_image, mem_pi, mem_univ, mem_setOf_eq,
      forall_true_left, mem_measurableCylinders, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
have 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 sorry) : ι)) (t i)
        (f (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))}
Tactic: refine ⟨{i}, {f | f ⟨i, Finset.mem_singleton_self i⟩ ∈ t i}, measurable_pi_apply _ (ht i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ 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 ⋯))}
have 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 sorry) : ι))
            (t i) (f (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry))})
      x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
⊢ measurableCylinders X =
    ⋃ (a : ℕ),
      ⋃ (S : Set ((i : ↥(Finset.Iic a)) → X (↑i : ℕ))), ⋃ (_ : MeasurableSet S), {cylinder (α := X) (Finset.Iic a) S}
have 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
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
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
have 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
Tactic: simp only [mem_measurableCylinders, exists_prop, mem_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
have 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
Tactic: refine ⟨?_, fun ⟨N, S, mS, s_eq⟩ ↦ ⟨Finset.Iic N, S, mS, s_eq⟩⟩