awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
simp_rw :
  Membership.mem (γ := Set (Set ((i : ι) → X i)))
      (⋃ (s : Finset ι),
        ⋃ (S : Set ((i : ↥s) → X (↑i : ι))), ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {cylinder (α := X) s S})
      t ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
simp_rw₁ :
  (∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
      Membership.mem (γ := Set (Set ((i : ι) → X i))) {cylinder (α := X) i i_1} t) ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
⊢ t ∈ closedCompactCylinders X ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
have simp_rw₂ : (∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
    t = cylinder (α := X) i i_1) ↔
  ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
Tactic: simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Finset ι
S : Set ((i : ↥s) → X (↑i : ι))
hS_closed : IsClosed S
hS_compact : IsCompact S
⊢ cylinder (α := X) s S ∈ closedCompactCylinders X
have rw : ∃ (s_1 : Finset ι) (S_1 : Set ((i : ↥s_1) → X (↑i : ι))),
  IsClosed S_1 ∧ IsCompact S_1 ∧ cylinder (α := X) s S = cylinder (α := X) s_1 S_1
Tactic: rw [mem_closedCompactCylinders]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (X i)
inst_3 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (X i)
ht : t ∈ closedCompactCylinders X
⊢ t ∈ measurableCylinders X
have rw : ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := X) s S
Tactic: rw [mem_measurableCylinders]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (X i)
inst_3 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (X i)
ht : t ∈ closedCompactCylinders X
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := X) s S
have refine_1 : MeasurableSet (closedCompactCylinders.set (X := X) (t := t) ht)
Tactic: refine ⟨closedCompactCylinders.finset ht, closedCompactCylinders.set ht, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (X i)
inst_3 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (X i)
ht : t ∈ closedCompactCylinders X
refine_1 : MeasurableSet (closedCompactCylinders.set (X := X) (t := t) ht)
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := X) s S
have refine_2 : t =
  cylinder (α := X) (closedCompactCylinders.finset (X := X) (t := t) ht)
    (closedCompactCylinders.set (X := X) (t := t) ht)
Tactic: refine ⟨closedCompactCylinders.finset ht, closedCompactCylinders.set ht, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
⊢ squareCylinders (α := α) C =
    ⋃ (s : Finset ι),
      (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
have h : ∀ (f : Set ((i : ι) → α i)),
  f ∈ squareCylinders (α := α) C ↔
    Membership.mem (γ := Set (Set ((i : ι) → α i)))
      (⋃ (s : Finset ι),
        (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C)
      f
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
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
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i
Tactic: have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
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
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ
Tactic: have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
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
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i
Tactic: have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
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
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ
Tactic: have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ 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
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
have rw : (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ squareCylinders (α := α) C
Tactic: rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
-- 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
⊢ (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ squareCylinders (α := α) C
have refine_1 : (fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
Tactic: refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
-- 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
refine_1 : (fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
⊢ (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ squareCylinders (α := α) C
have 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)
Tactic: refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
-- 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
⊢ (fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
have refine_1 : ∀ (i : ι), t₁' i ∩ t₂' i ∈ C i
Tactic: rw [mem_univ_pi]
-- 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 : ι
⊢ (t₁' i ∩ t₂' i).Nonempty
have obtain : ∀ (f : (i : ι) → α i) (hf : f ∈ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂), (t₁' i ∩ t₂' i).Nonempty
Tactic: obtain ⟨f, hf⟩ := hst_nonempty
Cleared hypotheses: hst_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
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₂
⊢ (t₁' i ∩ t₂' i).Nonempty
have hf₁ : (∀ 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
Cleared hypotheses: hf
-- 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
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
have refine_1 : f i ∈ t₁' i
Tactic: refine ⟨f i, ⟨?_, ?_⟩⟩
-- 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
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
⊢ (t₁' i ∩ t₂' i).Nonempty
have refine_2 : f i ∈ t₂' i
Tactic: refine ⟨f i, ⟨?_, ?_⟩⟩
-- 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
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
⊢ f i ∈ t₁' i
have pos : ∀ (hi₁ : i ∈ s₁), f i ∈ t₁' 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
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
⊢ f i ∈ t₁' i
have neg : ∀ (hi₁ : i ∉ s₁), f i ∈ t₁' 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
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
have neg : Membership.mem (γ := Set (α i)) univ (f 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
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
⊢ f i ∈ t₂' i
have pos : ∀ (hi₂ : i ∈ s₂), f i ∈ t₂' 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
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
⊢ f i ∈ t₂' i
have neg : ∀ (hi₂ : i ∉ s₂), f i ∈ t₂' 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
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
have neg : Membership.mem (γ := Set (α i)) univ (f i)
Tactic: rw [h2' i hi₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
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 ∈ C i
have this : (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 _