awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpace] fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ

Tactic:
continuous_iff_continuousAt.2 (fun μ ↦ ?_)

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
refine :
  ∀ (μ : (i : ι) → ProbabilityMeasure (α i)),
    ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i))
      (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ) μ
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpace] fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ

Tactic:
refine continuous_iff_continuousAt.2 (fun μ ↦ ?_)

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s' i)) : ℝ≥0) (0 : ℝ≥0)
⊢ Set.pi (α := α) univ s ∩ Set.pi (α := α) univ s' ∈ S

Tactic:
⟨fun i ↦ s i ∩ s' i, pi_inter_distrib.symm, fun i ↦ (smeas i).inter (s'meas i),
      fun i ↦ ?_⟩

Premises used: Set.Mem, setOf, Inter.inter, And.intro, Exists.intro, Eq.symm, Set.pi_inter_distrib, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s' i)) : ℝ≥0) (0 : ℝ≥0)
refine :
  ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier ((fun (i : ι) ↦ s i ∩ s' i) i)) : ℝ≥0) (0 : ℝ≥0)
⊢ Set.pi (α := α) univ s ∩ Set.pi (α := α) univ s' ∈ S

Tactic:
refine ⟨fun i ↦ s i ∩ s' i, pi_inter_distrib.symm, fun i ↦ (smeas i).inter (s'meas i),
      fun i ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s' i)) : ℝ≥0) (0 : ℝ≥0)
i : ι
simp_rw :
  ∀
    (hs :
      ∀ (i : ι),
        Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i)) : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs' :
      ∀ (i : ι),
        Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i ∩ s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier ((fun (i : ι) ↦ s i ∩ s' i) i)) : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp_rw [null_iff_toMeasure_null] at hs hs' ⊢

Premises used: MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
i : ι
hs : ∀ (i : ι), Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i)) : ℝ≥0∞) (0 : ℝ≥0∞)
hs' :
  ∀ (i : ι), Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i ∩ s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
null_frontier_inter (hs i) (hs' i)

Premises used: null_frontier_inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
i : ι
hs : ∀ (i : ι), Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i)) : ℝ≥0∞) (0 : ℝ≥0∞)
hs' :
  ∀ (i : ι), Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i ∩ s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact null_frontier_inter (hs i) (hs' i)

Premises used: null_frontier_inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
⊢ IsPiSystem S

Tactic:
have : IsPiSystem S := by
    rintro - ⟨s, rfl, smeas, hs⟩ - ⟨s', rfl, s'meas, hs'⟩ -
    refine ⟨fun i ↦ s i ∩ s' i, pi_inter_distrib.symm, fun i ↦ (smeas i).inter (s'meas i),
      fun i ↦ ?_⟩
    simp_rw [null_iff_toMeasure_null] at hs hs' ⊢
    exact null_frontier_inter (hs i) (hs' i)
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set ((i : ι) → α i)), IsOpen[Pi.topologicalSpace] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' :
  ∀ s ∈ S,
    Tendsto (β := ℝ≥0)
      (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦ ((pi (α := α) i : (a : Set ((i : ι) → α i)) → ℝ≥0) s : ℝ≥0)) (𝓝 μ)
      (𝓝
          ((((fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ) μ : ProbabilityMeasure ((i : ι) → α i)) :
              (a : Set ((i : ι) → α i)) → ℝ≥0)
            s) :
        Filter ℝ≥0)
⊢ ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i)) (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ)
    μ

Tactic:
apply this.tendsto_probabilityMeasure_of_tendsto_of_mem

Premises used: IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
⊢ MeasurableSet (Set.pi (α := α) univ s)

Tactic:
MeasurableSet.univ_pi smeas

Premises used: MeasurableSet.univ_pi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
⊢ MeasurableSet (Set.pi (α := α) univ s)

Tactic:
exact MeasurableSet.univ_pi smeas

Premises used: MeasurableSet.univ_pi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
⊢ ∃ ε > 0, ball x ε ⊆ u

Tactic:
Metric.isOpen_iff.1 u_open x xu

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
h : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ u), ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ u := Metric.isOpen_iff.1 u_open x xu

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
⊢ ∀ (i : ι),
    ∃ r ∈ Ioo 0 ε,
      Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening r {x i})) : ℝ≥0∞)
        (0 : ℝ≥0∞)

Tactic:
have A (i) : ∃ r ∈ Ioo 0 ε, (μ i : Measure (α i)) (frontier (Metric.thickening r {x i})) = 0 :=
      exists_null_frontier_thickening _ _ εpos
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
A :
  ∀ (i : ι),
    ∃ r ∈ Ioo 0 ε,
      Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening r {x i})) : ℝ≥0∞)
        (0 : ℝ≥0∞)
h :
  ∀ (r : (i : ι) → ℝ) (rpos : ∀ (i : ι), r i ∈ Ioo 0 ε)
    (hr :
      ∀ (i : ι),
        Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
          (0 : ℝ≥0∞)),
    ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

Tactic:
choose! r rpos hr using A
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
i : ι
⊢ Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier ((fun (i : ι) ↦ ball (x i) (r i)) i)) : ℝ≥0) (0 : ℝ≥0)

Tactic:
simpa using hr i
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h : (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ∈ 𝓝 x
h₁ : (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ⊆ u
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

Tactic:
refine ⟨univ.pi (fun i ↦ ball (x i) (r i)), ⟨fun i ↦ ball (x i) (r i), rfl,
      fun i ↦ measurableSet_ball, fun i ↦ by simpa using hr i⟩, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h : IsOpen[Pi.topologicalSpace] (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
h₁ : Membership.mem (γ := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) x
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ∈ 𝓝 x

Tactic:
apply IsOpen.mem_nhds

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ (a : ι), Membership.mem (γ := Set ι) univ a → IsOpen[inst_2 a] (ball (x a) (r a))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ IsOpen[Pi.topologicalSpace] (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))

Tactic:
exact isOpen_set_pi finite_univ (by simp)

Premises used: isOpen_set_pi, Set.finite_univ