awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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)
have h : Membership.mem (γ := Set (Set ((i : ℕ) → X i)))
  {cylinder (α := X) (Finset.Iic (t.sup id)) (Finset.restrict₂ (π := X) sorry ⁻¹' S)} (cylinder (α := X) t S)
Tactic: refine ⟨t.sup id, Finset.restrict₂ t.subset_Iic_sup_id ⁻¹' S,
    Finset.measurable_restrict₂ _ mS, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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)))
    {(Finset.Iic (t.sup id)).restrict (π := X) ⁻¹' Finset.restrict₂ (π := X) ⋯ ⁻¹' S} (t.restrict (π := X) ⁻¹' S)
have h : Membership.mem (γ := Set (Set ((i : ℕ) → X i))) {t.restrict (π := X) ⁻¹' S} (t.restrict (π := X) ⁻¹' S)
Tactic: rw [← preimage_comp, Finset.restrict₂_comp_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
g : α → (i : ι) → X i
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i
have simp_rw : MeasurableSpace.comap g (cylinderEvents (X := X) Δ) ≤ mα ↔
  ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun (a : α) ↦ g a i) (m i) ≤ mα
Tactic: simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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α
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i
have 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α
Tactic: simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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α
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i
have 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α
Tactic: simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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α
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i
have 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α
Tactic: simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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α
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable.{u_1, u_3} (β := X i) fun (a : α) ↦ g a i
have 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α
Tactic: simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
⊢ Measurable (β := (i : ι) → X i) fun (p : ((i : ι) → X i) × X i) ↦ update (β := X) p.1 i p.2
have 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
Tactic: rw [measurable_cylinderEvents_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ update (β := X) a.1 i a.2 j
have 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 sorry else a.1 j
Tactic: dsimp [update]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst : DecidableEq ι
j : ι
hj : 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
have 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 sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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 ⋯
⊢ 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
have neg : ∀ (h : ¬j = i), Measurable (β := X j) fun (a : ((i : ι) → X i) × X i) ↦ a.1 j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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) ↦ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ X x) a.2 ⋯
have pos : Measurable (β := X j) fun (a : ((i : ι) → X i) × X j) ↦ Eq.rec (motive := fun (x : ι) (x_1 : j = x) ↦ X x) a.2 sorry
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
inst : Unique ι
⊢ Measurable (α := X default) (uniqueElim (α := X))
have simp_rw : Measurable (β := X default) fun (x : X default) ↦ x
Tactic: simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
⊢ Measurable (α := (i : ι) → X i) (Δ.restrict (π := X))
have rw : ∀ (a : (↑Δ : Type u_2)), Measurable (β := X (↑a : ι)) fun (x : (i : ι) → X i) ↦ Δ.restrict (π := X) x a
Tactic: rw [@measurable_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ s = I.restrict (π := α) ⁻¹' t
have 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
Tactic: refine induction_on_inter generateFrom_squareCylinders.symm
    (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp))
    ⟨∅, ∅, by simp⟩ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ s = I.restrict (π := α) ⁻¹' t
have 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
Tactic: refine induction_on_inter generateFrom_squareCylinders.symm
    (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp))
    ⟨∅, ∅, by simp⟩ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
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
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ s = I.restrict (π := α) ⁻¹' t
have 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
Tactic: refine induction_on_inter generateFrom_squareCylinders.symm
    (isPiSystem_squareCylinders (fun _ ↦ isPiSystem_measurableSet) (by simp))
    ⟨∅, ∅, by simp⟩ ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
⊢ (↑I : Set ι).pi (α := α) t =
    (↑I : Set ι).restrict (π := α) ⁻¹'
      Set.pi (α := fun (a : (↑(↑I : Set ι) : Type u_2)) ↦ α (↑a : ι)) univ fun (i : (↑(↑I : Set ι) : Type u_2)) ↦
        t (↑i : ι)
have h : ∀ (x : (i : ι) → α i),
  x ∈ (↑I : Set ι).pi (α := α) t ↔
    Membership.mem (γ := Set ((i : ι) → α i))
      ((↑I : Set ι).restrict (π := α) ⁻¹'
        Set.pi (α := fun (a : (↑(↑I : Set ι) : Type u_2)) ↦ α (↑a : ι)) univ fun (i : (↑(↑I : Set ι) : Type u_2)) ↦
          t (↑i : ι))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (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
have refine_3 : ∀ (I : (i : ℕ) → Set ι) (t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))) (hI : ∀ (i : ℕ), (I i).Countable)
  (hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i),
  ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t
Tactic: choose! I t hI hf using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t
have refine_3 : Eq (α := Set ((i : ι) → α i)) (⋃ (i : ℕ), f i)
  (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
    (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
Tactic: refine ⟨⋃ n, I n, ⋃ n, (⋃ k, I k).restrict '' (f n), countable_iUnion hI, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (i : ℕ), f i)
    (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
      (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
have refine_3 : ∀ (x : (a : ι) → α a),
  Membership.mem (γ := Set ((a : ι) → α a)) (⋃ (i : ℕ), f i) x ↔
    Membership.mem (γ := Set ((a : ι) → α a))
      (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
        (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
⊢ Membership.mem (γ := Set ((a : ι) → α a)) (⋃ (i : ℕ), f i) x ↔
    Membership.mem (γ := Set ((a : ι) → α a))
      (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
        (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
      x
have refine_3 : (∃ (i : ℕ), (I i).restrict (π := α) x ∈ t i) ↔
  ∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)
Tactic: simp only [hf, mem_iUnion, mem_preimage, preimage_iUnion, mem_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
⊢ (∃ (i : ℕ), (I i).restrict (π := α) x ∈ t i) ↔
    ∃ (i : ℕ) (x_1 : (a : ι) → α a),
      (I i).restrict (π := α) x_1 ∈ t i ∧
        Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
          (restrict (π := α) (⋃ (n : ℕ), I n) x)
have refine_3 : (∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)) →
  ∀ (n : ℕ) (x' : (a : ι) → α a) (hn : (I n).restrict (π := α) x' ∈ t n)
    (hx :
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
        (restrict (π := α) (⋃ (n : ℕ), I n) x)),
    (I n).restrict (π := α) x ∈ t n
Tactic: refine ⟨fun ⟨i, hi⟩ ↦ ⟨i, x, hi, rfl⟩, fun ⟨n, x', hn, hx⟩ ↦ ⟨n, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
h :
  ∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)
n : ℕ
x' : (a : ι) → α a
hn : (I n).restrict (π := α) x' ∈ t n
hx :
  Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
    (restrict (π := α) (⋃ (n : ℕ), I n) x)
⊢ (I n).restrict (π := α) x ∈ t n
have this : ∀ (x : (i : ι) → α i),
  (I n).restrict (π := α) x =
    (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
        (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) sorry) :
          α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) sorry) : ι)))
      (restrict (π := α) (⋃ (k : ℕ), I k) x)
Tactic: have (x : Π i, α i) : (I n).restrict x =
      (fun (x : Π (i : ⋃ k, I k), α i) (i : I n) ↦ x ⟨i.1, subset_iUnion I n i.2⟩)
      ((⋃ k, I k).restrict x) := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
h :
  ∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)
n : ℕ
x' : (a : ι) → α a
hn : (I n).restrict (π := α) x' ∈ t n
hx :
  Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
    (restrict (π := α) (⋃ (n : ℕ), I n) x)
this :
  ∀ (x : (i : ι) → α i),
    (I n).restrict (π := α) x =
      (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
          (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
            α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
        (restrict (π := α) (⋃ (k : ℕ), I k) x)
⊢ (I n).restrict (π := α) x ∈ t n
have refine_3 : (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
      (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) sorry) :
        α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) sorry) : ι)))
    (restrict (π := α) (⋃ (k : ℕ), I k) x) ∈
  t n
Tactic: rwa [this, ← hx, ← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
h :
  ∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)
n : ℕ
x' : (a : ι) → α a
hn : (I n).restrict (π := α) x' ∈ t n
hx :
  Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
    (restrict (π := α) (⋃ (n : ℕ), I n) x)
this :
  ∀ (x : (i : ι) → α i),
    (I n).restrict (π := α) x =
      (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
          (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
            α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
        (restrict (π := α) (⋃ (k : ℕ), I k) x)
refine_3 :
  (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
        (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
          α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
      (restrict (π := α) (⋃ (k : ℕ), I k) x) ∈
    t n
⊢ (I n).restrict (π := α) x ∈ t n
have refine_3₁ : (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
      (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) sorry) :
        α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) sorry) : ι)))
    (restrict (π := α) (⋃ (n : ℕ), I n) x') ∈
  t n
Tactic: rwa [this, ← hx, ← this]