awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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
⊢ ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i)) (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ)
    μ
have hmeas : ∀ s ∈ S, MeasurableSet s
Tactic: apply this.tendsto_probabilityMeasure_of_tendsto_of_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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
⊢ ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i)) (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ)
    μ
have h : ∀ (u : Set ((i : ι) → α i)), IsOpen[Pi.topologicalSpace] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
Tactic: apply this.tendsto_probabilityMeasure_of_tendsto_of_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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
⊢ ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i)) (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ)
    μ
have 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)
Tactic: apply this.tendsto_probabilityMeasure_of_tendsto_of_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ u), ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ u := Metric.isOpen_iff.1 u_open x xu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (hypothesis)
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
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have A : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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∞)
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have 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
Tactic: choose! r rpos hr using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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∞)
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h : (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ∈ 𝓝 x
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⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h₁ : (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ⊆ 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⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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∞)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ∈ 𝓝 x
have h : IsOpen[Pi.topologicalSpace] (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
Tactic: apply IsOpen.mem_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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))
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ∈ 𝓝 x
have h₁ : Membership.mem (γ := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) x
Tactic: apply IsOpen.mem_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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∞)
⊢ Subset (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
    (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε)
have h : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) univ i), r i ≤ ε
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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∞)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ⊆ u
have calc : Subset (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
  (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε)
Tactic: calc univ.pi fun i ↦ ball (x i) (r i)
      _ ⊆ univ.pi fun i ↦ ball (x i) ε := by gcongr with i hi; exact (rpos i).2.le
      _ ⊆ u := by rwa [← ball_pi _ εpos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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∞)
calc :
  Subset (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
    (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ⊆ u
have calc₁ : (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε) ⊆ u
Tactic: calc univ.pi fun i ↦ ball (x i) (r i)
      _ ⊆ univ.pi fun i ↦ ball (x i) ε := by gcongr with i hi; exact (rpos i).2.le
      _ ⊆ u := by rwa [← ball_pi _ εpos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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)
⊢ Tendsto (β := ℝ≥0)
    (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦
      ((pi (α := α) i : (a : Set ((i : ι) → α i)) → ℝ≥0) (Set.pi (α := α) univ s) : ℝ≥0))
    (𝓝 μ)
    (𝓝
        ((((fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ) μ : ProbabilityMeasure ((i : ι) → α i)) :
            (a : Set ((i : ι) → α i)) → ℝ≥0)
          (Set.pi (α := α) univ s)) :
      Filter ℝ≥0)
have h' : Tendsto (β := ℝ≥0) (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦ ∏ i_1 : ι, (i i_1 : (a : Set (α i_1)) → ℝ≥0) (s i_1))
  (𝓝 μ) (𝓝 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) (s i)))
Tactic: simp only [pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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)
⊢ Tendsto (β := ℝ≥0)
    (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦ ∏ i_1 : ι, (i i_1 : (a : Set (α i_1)) → ℝ≥0) (s i_1)) (𝓝 μ)
    (𝓝 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) (s i)))
have apply : ∀ (i : ι) (hi : Membership.mem (γ := Finset ι) Finset.univ i),
  Tendsto (β := ℝ≥0) (fun (b : (i : ι) → ProbabilityMeasure (α i)) ↦ ((b i : (a : Set (α i)) → ℝ≥0) (s i) : ℝ≥0)) (𝓝 μ)
    (𝓝 ((μ i : (a : Set (α i)) → ℝ≥0) (s i)) : Filter ℝ≥0)
Tactic: apply tendsto_finsetProd _ (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (μ.prod ν).mass = μ.mass * ν.mass
have simp : ENNReal.toNNReal
    (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
      (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
  ENNReal.toNNReal (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ) *
    ENNReal.toNNReal (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ)
Tactic: simp only [coeFn_def, mass, univ_prod_univ.symm, toMeasure_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ ENNReal.toNNReal
      (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
    ENNReal.toNNReal (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ) *
      ENNReal.toNNReal (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ)
have rw : ENNReal.toNNReal
    (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
      (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
  (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
      (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)).toNNReal
Tactic: rw [← ENNReal.toNNReal_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
ν : FiniteMeasure β
⊢ Eq (α := FiniteMeasure (α × β)) (prod 0 ν) 0
have rw : mass (Ω := α × β) (prod 0 ν) = 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
ν : FiniteMeasure β
rw : mass (Ω := α × β) (prod 0 ν) = 0
⊢ Eq (α := FiniteMeasure (α × β)) (prod 0 ν) 0
have rw₁ : mass.{u_1} (Ω := α) 0 * ν.mass = 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
ν : FiniteMeasure β
rw : mass (Ω := α × β) (prod 0 ν) = 0
rw₁ : mass.{u_1} (Ω := α) 0 * ν.mass = 0
⊢ Eq (α := FiniteMeasure (α × β)) (prod 0 ν) 0
have rw₂ : 0 * ν.mass = 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
ν : FiniteMeasure β
rw : mass (Ω := α × β) (prod 0 ν) = 0
rw₁ : mass.{u_1} (Ω := α) 0 * ν.mass = 0
rw₂ : 0 * ν.mass = 0
⊢ Eq (α := FiniteMeasure (α × β)) (prod 0 ν) 0
have rw₃ : Eq (α := ℝ≥0) 0 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
⊢ Eq (α := FiniteMeasure (α × β)) (μ.prod 0) 0
have rw : mass (Ω := α × β) (μ.prod 0) = 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
rw : mass (Ω := α × β) (μ.prod 0) = 0
⊢ Eq (α := FiniteMeasure (α × β)) (μ.prod 0) 0
have rw₁ : μ.mass * mass.{u_2} (Ω := β) 0 = 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
rw : mass (Ω := α × β) (μ.prod 0) = 0
rw₁ : μ.mass * mass.{u_2} (Ω := β) 0 = 0
⊢ Eq (α := FiniteMeasure (α × β)) (μ.prod 0) 0
have rw₂ : μ.mass * 0 = 0
Tactic: rw [← mass_zero_iff, mass_prod, zero_mass, mul_zero]