awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
left : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)
right : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧
    Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
left : EventuallyEq (β := ℝ≥0∞) (𝓝[<] 0) (fun (x : ℝ) ↦ 0) fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
h : ∀ (hr : r < 0), Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℝ) (Iio 0) r →
    Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)

Tactic:
(hr : r < 0)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
h : ∀ (r : ℝ) (hr : r < 0), Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[<] 0) (fun (x : ℝ) ↦ 0) fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))

Tactic:
filter_upwards [self_mem_nhdsWithin] with r (hr : r < 0)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
hr : r < 0
linarith : b - r ≤ b + r → 2 * (r - 0) + (b - r - (b + r)) = 0
linarith₁ : b - r ≤ b + r → GT.gt (α := ℝ) 2 0
⊢ ¬b - r ≤ b + r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
hr : r < 0
h : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
h₁ h₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)

Tactic:
rw [Icc_eq_empty (by linarith), measure_empty]

Premises used: Set.Icc_eq_empty, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)

Tactic:
simpa only [measure_singleton] using tendsto_measure_Icc_nhdsWithin_right μ b

Premises used: tendsto_measure_Icc_nhdsWithin_right, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
⊢ BorelSpace.{u_1} (WithTop ι)

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
α : Type u_2
mα : MeasurableSpace α
f : WithTop ι → α
h : Measurable.{u_1, u_2} (β := α) fun (p : ι) ↦ f (↑p : WithTop ι)
⊢ Measurable f

Tactic:
measurable_of_measurable_on_compl_singleton ⊤
    (MeasurableEquiv.neTopEquiv.symm.measurable_comp_iff.1 h)

Premises used: MeasurableEquiv.symm, WithTop.MeasurableEquiv.neTopEquiv, MeasurableEquiv.measurable_comp_iff, measurable_of_measurable_on_compl_singleton, Iff.mp, Top.top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
d : ι
⊢ Measurable (untopD d)

Tactic:
measurable_of_measurable_comp_coe measurable_id

Premises used: measurable_id, WithTop.measurable_of_measurable_comp_coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
inst_5 : Nonempty ι
⊢ Measurable.{u_1, u_1} (α := WithTop ι) untopA

Tactic:
measurable_untopD _

Premises used: WithTop.measurable_untopD
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
⊢ Measurable (β := WithTop ι) fun (x : ι) ↦ (↑x : WithTop ι)

Tactic:
continuous_coe.measurable

Premises used: WithTop.continuous_coe, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
α : Type u_2
mα : MeasurableSpace α
f : α → ι
hf : Measurable f
⊢ Measurable.{u_2, u_1} (β := WithTop ι) fun (x : α) ↦ (↑(f x) : WithTop ι)

Tactic:
measurable_coe.comp hf

Premises used: WithTop.measurable_coe, Measurable.comp, WithTop.some
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
α : Type u_2
mα : MeasurableSpace α
d : ι
f : α → WithTop ι
hf : Measurable f
⊢ Measurable.{u_2, u_1} (β := ι) fun (x : α) ↦ untopD d (f x)

Tactic:
(measurable_untopD d).comp hf

Premises used: Measurable.comp, WithTop.untopD, WithTop.measurable_untopD, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : MeasurableSpace ι
inst_4 : BorelSpace ι
α : Type u_2
mα : MeasurableSpace α
inst_5 : Nonempty ι
f : α → WithTop ι
hf : Measurable f
⊢ Measurable.{u_2, u_1} (β := ι) fun (x : α) ↦ (f x).untopA

Tactic:
hf.untopD _

Premises used: Measurable.untopD
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
simp_rw :
  ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
    ∅ = cylinder (α := X) i i_1
⊢ ∅ ∈ closedCompactCylinders X

Tactic:
simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, MeasureTheory.closedCompactCylinders, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
⊢ ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
    ∅ = cylinder (α := X) i i_1

Tactic:
⟨∅, ∅, isClosed_empty, isCompact_empty, (cylinder_empty _).symm⟩

Premises used: MeasureTheory.cylinder_empty, isClosed_empty, Exists.intro, EmptyCollection.emptyCollection, Eq.symm, isCompact_empty
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
⊢ ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
    ∅ = cylinder (α := X) i i_1

Tactic:
exact ⟨∅, ∅, isClosed_empty, isCompact_empty, (cylinder_empty _).symm⟩
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
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
⊢ t ∈ closedCompactCylinders X ↔
    ∃ (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]

Premises used: Set.mem_iUnion, exists_prop, MeasureTheory.closedCompactCylinders, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
ht : t ∈ closedCompactCylinders X
⊢ IsClosed (set (X := X) (t := t) ht)

Tactic:
((mem_closedCompactCylinders t).mp ht).choose_spec.choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, setOf, MeasureTheory.closedCompactCylinders.set, MeasureTheory.mem_closedCompactCylinders, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
ht : t ∈ closedCompactCylinders X
⊢ IsCompact (set (X := X) (t := t) ht)

Tactic:
((mem_closedCompactCylinders t).mp ht).choose_spec.choose_spec.2.1

Premises used: Exists.choose_spec, Set.Mem, setOf, MeasureTheory.closedCompactCylinders.set, MeasureTheory.mem_closedCompactCylinders, And.right, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
ht : t ∈ closedCompactCylinders X
⊢ t = cylinder (α := X) (finset (X := X) (t := t) ht) (set (X := X) (t := t) ht)

Tactic:
((mem_closedCompactCylinders t).mp ht).choose_spec.choose_spec.2.2

Premises used: MeasureTheory.closedCompactCylinders.finset, Exists.choose_spec, Set.Mem, setOf, MeasureTheory.closedCompactCylinders.set, MeasureTheory.mem_closedCompactCylinders, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
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
⊢ cylinder (α := X) s S ∈ closedCompactCylinders X

Tactic:
rw [mem_closedCompactCylinders]

Premises used: MeasureTheory.mem_closedCompactCylinders
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
⊢ ∃ (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:
⟨s, S, hS_closed, hS_compact, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
⊢ ∃ (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:
exact ⟨s, S, hS_closed, hS_compact, rfl⟩
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
rw : ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := X) s S
⊢ t ∈ measurableCylinders X

Tactic:
rw [mem_measurableCylinders]

Premises used: MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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

Tactic:
⟨closedCompactCylinders.finset ht, closedCompactCylinders.set ht, ?_, ?_⟩

Premises used: MeasureTheory.closedCompactCylinders.finset, MeasureTheory.closedCompactCylinders.set, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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)
refine_2 :
  t =
    cylinder (α := X) (closedCompactCylinders.finset (X := X) (t := t) ht)
      (closedCompactCylinders.set (X := X) (t := t) ht)
⊢ ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), MeasurableSet S ∧ t = cylinder (α := X) s S

Tactic:
refine ⟨closedCompactCylinders.finset ht, closedCompactCylinders.set ht, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
⊢ MeasurableSet (closedCompactCylinders.set (X := X) (t := t) ht)

Tactic:
(closedCompactCylinders.isClosed ht).measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.closedCompactCylinders.isClosed
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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
⊢ MeasurableSet (closedCompactCylinders.set (X := X) (t := t) ht)

Tactic:
exact (closedCompactCylinders.isClosed ht).measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.closedCompactCylinders.isClosed
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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 =
    cylinder (α := X) (closedCompactCylinders.finset (X := X) (t := t) ht)
      (closedCompactCylinders.set (X := X) (t := t) ht)

Tactic:
closedCompactCylinders.eq_cylinder ht

Premises used: MeasureTheory.closedCompactCylinders.eq_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
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 =
    cylinder (α := X) (closedCompactCylinders.finset (X := X) (t := t) ht)
      (closedCompactCylinders.set (X := X) (t := t) ht)

Tactic:
exact closedCompactCylinders.eq_cylinder ht

Premises used: MeasureTheory.closedCompactCylinders.eq_cylinder
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
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
⊢ squareCylinders (α := α) C =
    ⋃ (s : Finset ι),
      (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) '' Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C

Tactic:
ext1 f
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
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:
simp only [squareCylinders, mem_iUnion, mem_image, mem_univ_pi, mem_setOf_eq,
    eq_comm (a := f)]

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_setOf_eq, eq_comm, MeasureTheory.squareCylinders, 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
⊢ ∀ 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
-- 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
⊢ ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ

Tactic:
have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ 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
⊢ ∀ 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
-- 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
⊢ ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ

Tactic:
have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ 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
rw : (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ squareCylinders (α := α) C
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C

Tactic:
rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']

Premises used: Set.union_pi_inter, 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
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

Tactic:
⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩

Premises used: Set.Mem, setOf, Inter.inter, And.intro, MeasureTheory.squareCylinders, Exists.intro, Union.union