awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₁
neg : univ ∈ C i
⊢ t₁' i ∈ C i

Tactic:
rw [h1' i hi₁]
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₁
⊢ univ ∈ C i

Tactic:
hC_univ i
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₁
⊢ univ ∈ C i

Tactic:
exact hC_univ i
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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
neg : ∀ (hi₂ : i ∉ s₂), t₂' i ∈ C i
⊢ t₂' i ∈ C i

Tactic:
by_cases hi₂ : i ∈ s₂
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₂
pos : t₂ i ∈ C i
⊢ t₂' i ∈ C i

Tactic:
rw [← h2 i hi₂]
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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

Tactic:
h₂ i (mem_univ _)

Premises used: Set.Mem, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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

Tactic:
exact h₂ i (mem_univ _)

Premises used: Set.mem_univ
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₂
neg : univ ∈ C i
⊢ t₂' i ∈ C i

Tactic:
rw [h2' i hi₂]
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₂
⊢ univ ∈ C i

Tactic:
hC_univ i
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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₂
⊢ univ ∈ C i

Tactic:
exact hC_univ i
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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
refine_2 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)
⊢ 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)

Tactic:
rw [Finset.coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
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})
⊢ 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})

Tactic:
simp only [singleton_pi]

Premises used: Set.singleton_pi
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
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}))
⊢ 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:
rw [MeasurableSpace.comap_eq_generateFrom]

Premises used: MeasurableSpace.comap_eq_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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}))

Tactic:
MeasurableSpace.generateFrom_mono fun S ↦ ?_

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
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
⊢ 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:
refine MeasurableSpace.generateFrom_mono fun S ↦ ?_

Premises used: MeasurableSpace.generateFrom_mono
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
simp :
  ∀ (x : Set (α i)),
    MeasurableSet x →
      eval (β := α) i ⁻¹' x = S →
        ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S
⊢ 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:
simp only [mem_setOf_eq, mem_image, mem_univ_pi, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, Set.mem_univ_pi
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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 : ι
hji : j = i
⊢ Set (α j)

Tactic:
convert! t
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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)
refine_2 : eval (β := α) i ⁻¹' (fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) i = S
⊢ ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S

Tactic:
refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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)
neg :
  ∀ (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)

Tactic:
by_cases hji : j = i
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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 : ι
hji : j = i
pos : MeasurableSet (α := α j) (cast ⋯ t)
⊢ MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)

Tactic:
simp only [hji, eq_mpr_eq_cast, dif_pos]

Premises used: dif_pos, eq_mpr_eq_cast
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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 : ι
hji : j = i
⊢ MeasurableSet t

Tactic:
ht
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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 : ι
hji : j = i
h₁ : α j = α i → HEq (α := Set (α j)) (cast ⋯ t) t
⊢ MeasurableSet (α := α j) (cast ⋯ t)

Tactic:
convert! ht
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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 : ι
hji : j = i
e_1 : α j = α i
⊢ HEq (α := Set (α j)) (cast ⋯ t) t

Tactic:
simp only [cast_heq]

Premises used: cast_heq
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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 : ι
hji : ¬j = i
⊢ MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)

Tactic:
simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]

Premises used: dif_neg, not_false_iff, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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
⊢ eval (β := α) i ⁻¹' (fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) i = S

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
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)
refine_2 refine_2₁ : eval (β := α) i ⁻¹' (fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) i = S
⊢ ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S

Tactic:
classical
  refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
  · by_cases hji : j = i
    · simp only [hji, eq_mpr_eq_cast, dif_pos]
      convert! ht
      simp only [cast_heq]
    · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
  · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp [h]

Premises used: cast_heq, dif_pos, dif_neg, eq_mpr_eq_cast, not_false_iff, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
a :
  LE.le (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))
a₁ :
  LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.pi (X := α))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
⊢ Eq (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))

Tactic:
apply le_antisymm

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

Tactic:
rw [MeasurableSpace.generateFrom_le_iff]

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

Tactic:
simp only [mem_univ_pi, mem_setOf_eq] at h

Premises used: Set.mem_setOf_eq, Set.mem_univ_pi
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (t i)
⊢ Membership.mem (γ := Set (Set ((i : ι) → α i))) {t : Set ((i : ι) → α i) | MeasurableSet t}
    ((↑s : Set ι).pi (α := α) t)

Tactic:
MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)

Premises used: MeasurableSet, Set.Mem, setOf, Finset.countable_toSet, MeasurableSet.pi
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (t i)
⊢ Membership.mem (γ := Set (Set ((i : ι) → α i))) {t : Set ((i : ι) → α i) | MeasurableSet t}
    ((↑s : Set ι).pi (α := α) t)

Tactic:
exact MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)

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

Tactic:
iSup_le fun i ↦ ?_

Premises used: Set.Mem, setOf, iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
a :
  ∀ (i : ι),
    LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i))
      (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
⊢ LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.pi (X := α))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))

Tactic:
refine iSup_le fun i ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))

Tactic:
(comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_

Premises used: MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton, LE.le.trans