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
refine_1 : (fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
refine_2 :
  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)
⊢ (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ squareCylinders (α := α) C

Tactic:
refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' 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_1 : ∀ (i : ι), t₁' i ∩ t₂' i ∈ C i
⊢ (fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
rw [mem_univ_pi]

Premises used: Set.mem_univ_pi
-- 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 : ι
obtain :
  ∀ (f : (i : ι) → α i) (hf : f ∈ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂), (t₁' i ∩ t₂' i).Nonempty
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
obtain ⟨f, hf⟩ := hst_nonempty
-- 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
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 : ι
f : (i : ι) → α i
hf : f ∈ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂
⊢ (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i

Tactic:
rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf

Premises used: Set.mem_inter_iff, Set.mem_pi, Set.pi_congr, rfl
-- 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
⟨f i, ⟨?_, ?_⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
refine_1 : f i ∈ t₁' i
refine_2 : f i ∈ t₂' i
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
refine ⟨f 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
pos : ∀ (hi₁ : i ∈ s₁), f i ∈ t₁' i
neg : ∀ (hi₁ : i ∉ s₁), f i ∈ t₁' i
⊢ f i ∈ t₁' 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₁ : i ∈ s₁
⊢ f i ∈ t₁' i

Tactic:
hf.1 i hi₁

Premises used: And.left
-- 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₁ : i ∈ s₁
⊢ f i ∈ t₁' i

Tactic:
exact hf.1 i hi₁

Premises used: And.left
-- 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₁ : i ∉ s₁
neg : Membership.mem (γ := Set (α i)) univ (f i)
⊢ f i ∈ t₁' 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₁ : i ∉ s₁
⊢ Membership.mem (γ := Set (α i)) univ (f i)

Tactic:
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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₁ : i ∉ s₁
⊢ Membership.mem (γ := Set (α i)) univ (f i)

Tactic:
exact 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
pos : ∀ (hi₂ : i ∈ s₂), f i ∈ t₂' i
neg : ∀ (hi₂ : i ∉ s₂), f i ∈ t₂' i
⊢ f i ∈ t₂' 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₂ : i ∈ s₂
⊢ f i ∈ t₂' i

Tactic:
hf.2 i hi₂

Premises used: And.right
-- 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₂ : i ∈ s₂
⊢ f i ∈ t₂' i

Tactic:
exact hf.2 i hi₂

Premises used: And.right
-- 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₂ : i ∉ s₂
neg : Membership.mem (γ := Set (α i)) univ (f i)
⊢ f i ∈ t₂' 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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₂ : i ∉ s₂
⊢ Membership.mem (γ := Set (α i)) univ (f i)

Tactic:
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
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 : ι
f : (i : ι) → α i
hf : (∀ i ∈ (↑s₁ : Set ι), f i ∈ t₁' i) ∧ ∀ i ∈ (↑s₂ : Set ι), f i ∈ t₂' i
hi₂ : i ∉ s₂
⊢ Membership.mem (γ := Set (α i)) univ (f i)

Tactic:
exact 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 : ι
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
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 _
-- 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
⊢ t₁' i ∩ t₂' i ∈ C i

Tactic:
hC i _ ?_ _ ?_ this
-- 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
refine_1 : t₁' i ∈ C i
refine_1₁ : t₂' i ∈ C i
⊢ t₁' i ∩ t₂' i ∈ C i

Tactic:
refine hC i _ ?_ _ ?_ this
-- 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 [← 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₁
⊢ 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