awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
⊢ t₁' i ∩ t₂' i ∈ C i
have refine_1 : t₁' i ∈ C i
Tactic: refine hC i _ ?_ _ ?_ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
refine_1 : t₁' i ∈ C i
⊢ t₁' i ∩ t₂' i ∈ C i
have refine_1₁ : t₂' i ∈ C i
Tactic: refine hC i _ ?_ _ ?_ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
⊢ t₁' i ∈ C i
have pos : ∀ (hi₁ : i ∈ s₁), t₁' i ∈ C i
Tactic: by_cases hi₁ : i ∈ s₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
pos : ∀ (hi₁ : i ∈ s₁), t₁' i ∈ C i
⊢ t₁' i ∈ C i
have neg : ∀ (hi₁ : i ∉ s₁), t₁' i ∈ C i
Tactic: by_cases hi₁ : i ∈ s₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∈ s₁
⊢ t₁' i ∈ C i
have pos : t₁ i ∈ C i
Tactic: rw [← h1 i hi₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∉ s₁
⊢ t₁' i ∈ C i
have neg : univ ∈ C i
Tactic: rw [h1' i hi₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
⊢ t₂' i ∈ C i
have pos : ∀ (hi₂ : i ∈ s₂), t₂' i ∈ C i
Tactic: by_cases hi₂ : i ∈ s₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
pos : ∀ (hi₂ : i ∈ s₂), t₂' i ∈ C i
⊢ t₂' i ∈ C i
have neg : ∀ (hi₂ : i ∉ s₂), t₂' i ∈ C i
Tactic: by_cases hi₂ : i ∈ s₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∈ s₂
⊢ t₂' i ∈ C i
have pos : t₂ i ∈ C i
Tactic: rw [← h2 i hi₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∉ s₂
⊢ t₂' i ∈ C i
have neg : univ ∈ C i
Tactic: rw [h2' i hi₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ
h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
⊢ Eq (α := Set ((i : ι) → α i)) (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i)
    ((↑(s₁ ∪ s₂) : Set ι).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i)
have refine_2 : Eq (α := Set ((i : ι) → α i)) (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i)
  (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i)
Tactic: rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
let let₁ let₂ let₃ : (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have let₄ : let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i),
  (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
Tactic: classical
  let t₁' := s₁.piecewise t₁ (fun i ↦ univ)
  let t₂' := s₂.piecewise t₂ (fun i ↦ univ)
  have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
  refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
  · rw [mem_univ_pi]
    intro i
    have : (t₁' i ∩ t₂' i).Nonempty := by
      obtain ⟨f, hf⟩ := hst_nonempty
      rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf
      refine ⟨f i, ⟨?_, ?_⟩⟩
      · by_cases hi₁ : i ∈ s₁
        · exact hf.1 i hi₁
        · rw [h1' i hi₁]
          exact mem_univ _
      · by_cases hi₂ : i ∈ s₂
        · exact hf.2 i hi₂
        · rw [h2' i hi₂]
          exact mem_univ _
    refine hC i _ ?_ _ ?_ this
    · by_cases hi₁ : i ∈ s₁
      · rw [← h1 i hi₁]
        exact h₁ i (mem_univ _)
      · rw [h1' i hi₁]
        exact hC_univ i
    · by_cases hi₂ : i ∈ s₂
      · rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)
      · rw [h2' i hi₂]
        exact hC_univ i
  · rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
let let₁ let₂ let₃ : (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₄ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have let₅ : let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ),
  (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
Tactic: classical
  let t₁' := s₁.piecewise t₁ (fun i ↦ univ)
  let t₂' := s₂.piecewise t₂ (fun i ↦ univ)
  have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
  refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
  · rw [mem_univ_pi]
    intro i
    have : (t₁' i ∩ t₂' i).Nonempty := by
      obtain ⟨f, hf⟩ := hst_nonempty
      rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf
      refine ⟨f i, ⟨?_, ?_⟩⟩
      · by_cases hi₁ : i ∈ s₁
        · exact hf.1 i hi₁
        · rw [h1' i hi₁]
          exact mem_univ _
      · by_cases hi₂ : i ∈ s₂
        · exact hf.2 i hi₂
        · rw [h2' i hi₂]
          exact mem_univ _
    refine hC i _ ?_ _ ?_ this
    · by_cases hi₁ : i ∈ s₁
      · rw [← h1 i hi₁]
        exact h₁ i (mem_univ _)
      · rw [h1' i hi₁]
        exact hC_univ i
    · by_cases hi₂ : i ∈ s₂
      · rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)
      · rw [h2' i hi₂]
        exact hC_univ i
  · rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
let let₁ let₂ let₃ : (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₄ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₅ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have let₆ : let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
let t₂' := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ;
∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ)
  (h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i),
  (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
Tactic: classical
  let t₁' := s₁.piecewise t₁ (fun i ↦ univ)
  let t₂' := s₂.piecewise t₂ (fun i ↦ univ)
  have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
  refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
  · rw [mem_univ_pi]
    intro i
    have : (t₁' i ∩ t₂' i).Nonempty := by
      obtain ⟨f, hf⟩ := hst_nonempty
      rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf
      refine ⟨f i, ⟨?_, ?_⟩⟩
      · by_cases hi₁ : i ∈ s₁
        · exact hf.1 i hi₁
        · rw [h1' i hi₁]
          exact mem_univ _
      · by_cases hi₂ : i ∈ s₂
        · exact hf.2 i hi₂
        · rw [h2' i hi₂]
          exact mem_univ _
    refine hC i _ ?_ _ ?_ this
    · by_cases hi₁ : i ∈ s₁
      · rw [← h1 i hi₁]
        exact h₁ i (mem_univ _)
      · rw [h1' i hi₁]
        exact hC_univ i
    · by_cases hi₂ : i ∈ s₂
      · rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)
      · rw [h2' i hi₂]
        exact hC_univ i
  · rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval (β := α) i) (m 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})
have simp : MeasurableSpace.comap (eval (β := α) i) (m i) ≤
  generateFrom
    ((fun (a : (i : ι) → Set (α i)) ↦ eval (β := α) i ⁻¹' a i) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
Tactic: simp only [singleton_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval (β := α) i) (m i) ≤
    generateFrom
      ((fun (a : (i : ι) → Set (α i)) ↦ eval (β := α) i ⁻¹' a i) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
have rw : LE.le (α := MeasurableSpace ((x : ι) → α x))
  (generateFrom {t : Set ((x : ι) → α x) | ∃ (s : Set (α i)), MeasurableSet s ∧ eval (β := α) i ⁻¹' s = t})
  (generateFrom
    ((fun (a : (i : ι) → Set (α i)) ↦ eval (β := α) i ⁻¹' a i) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
Tactic: rw [MeasurableSpace.comap_eq_generateFrom]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ LE.le (α := MeasurableSpace ((x : ι) → α x))
    (generateFrom {t : Set ((x : ι) → α x) | ∃ (s : Set (α i)), MeasurableSet s ∧ eval (β := α) i ⁻¹' s = t})
    (generateFrom
      ((fun (a : (i : ι) → Set (α i)) ↦ eval (β := α) i ⁻¹' a i) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
have refine : ∀ (S : Set ((x : ι) → α x)),
  Membership.mem (γ := Set (Set ((x : ι) → α x)))
      {t : Set ((x : ι) → α x) | ∃ (s : Set (α i)), MeasurableSet s ∧ eval (β := α) i ⁻¹' s = t} S →
    Membership.mem (γ := Set (Set ((x : ι) → α x)))
      ((fun (a : (i : ι) → Set (α i)) ↦ eval (β := α) i ⁻¹' a i) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
      S
Tactic: refine MeasurableSpace.generateFrom_mono fun S ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
⊢ Membership.mem (γ := Set (Set ((x : ι) → α x)))
      {t : Set ((x : ι) → α x) | ∃ (s : Set (α i)), MeasurableSet s ∧ eval (β := α) i ⁻¹' s = t} S →
    Membership.mem (γ := Set (Set ((x : ι) → α x)))
      ((fun (a : (i : ι) → Set (α i)) ↦ eval (β := α) i ⁻¹' a i) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
      S
have simp : ∀ (x : Set (α i)),
  MeasurableSet x →
    eval (β := α) i ⁻¹' x = S →
      ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S
Tactic: simp only [mem_setOf_eq, mem_image, mem_univ_pi, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
⊢ ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S
have refine_1 : ∀ (j : ι), MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr sorry t else univ : Set (α j))) j)
Tactic: refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
refine_1 :
  ∀ (j : ι), MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)
⊢ ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S
have refine_2 : eval (β := α) i ⁻¹' (fun (j : ι) ↦ (if hji : j = i then Eq.mpr sorry t else univ : Set (α j))) i = S
Tactic: refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
j : ι
⊢ MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)
have pos : ∀ (hji : j = i),
  MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr sorry t else univ : Set (α j))) j)
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
j : ι
pos :
  ∀ (hji : j = i),
    MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)
⊢ MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)
have neg : ∀ (hji : ¬j = i),
  MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr sorry t else univ : Set (α j))) j)
Tactic: by_cases hji : j = i