awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (thickening r {x.1})) : ℝ≥0∞) (0 : ℝ≥0∞)
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (thickening r' {x.2})) : ℝ≥0∞) (0 : ℝ≥0∞)
μr₁ : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have μr'₁ : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [thickening_singleton] at μr μr'
Cleared hypotheses: μr, μr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h : ball x.1 r ×ˢ ball x.2 r' ∈ 𝓝 x
Tactic: refine ⟨ball x.1 r ×ˢ ball x.2 r', ⟨ball x.1 r, ball x.2 r', measurableSet_ball,
      by simp [coeFn_def, μr], measurableSet_ball, by simp [coeFn_def, μr'], rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
h : ball x.1 r ×ˢ ball x.2 r' ∈ 𝓝 x
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h₁ : ball x.1 r ×ˢ ball x.2 r' ⊆ u
Tactic: refine ⟨ball x.1 r ×ˢ ball x.2 r', ⟨ball x.1 r, ball x.2 r', measurableSet_ball,
      by simp [coeFn_def, μr], measurableSet_ball, by simp [coeFn_def, μr'], rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε
have hs : r ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
hs : r ≤ ε
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε
have ht : r' ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ u
have calc : ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε
Tactic: calc ball x.1 r ×ˢ ball x.2 r'
      _ ⊆ ball x.1 ε ×ˢ ball x.2 ε := by gcongr; exacts [hr.2.le, hr'.2.le]
      _ ⊆ _ := by rwa [ball_prod_same]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
calc : ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ u
have calc₁ : ball x.1 ε ×ˢ ball x.2 ε ⊆ u
Tactic: calc ball x.1 r ×ˢ ball x.2 r'
      _ ⊆ ball x.1 ε ×ˢ ball x.2 ε := by gcongr; exacts [hr.2.le, hr'.2.le]
      _ ⊆ _ := by rwa [ball_prod_same]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto (β := ℝ≥0)
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      ((i.1.prod i.2 : (a : Set (α × β)) → ℝ≥0) (a ×ˢ b) : ℝ≥0))
    (𝓝 μ)
    (𝓝
        ((((fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ :
              ProbabilityMeasure (α × β)) :
            (a : Set (α × β)) → ℝ≥0)
          (a ×ˢ b)) :
      Filter ℝ≥0)
have h' : Tendsto
  (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((i.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((i.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
  (𝓝 μ) (𝓝 (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) b : ℝ≥0)))
Tactic: simp only [prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((i.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((i.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) b : ℝ≥0)))
have h' : Tendsto (β := ℝ≥0)
  (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.1 : (a : Set α) → ℝ≥0) a : ℝ≥0)) (𝓝 μ)
  (𝓝 ((μ.1 : (a : Set α) → ℝ≥0) a) : Filter ℝ≥0)
Tactic: apply Filter.Tendsto.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
h' :
  Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.1 : (a : Set α) → ℝ≥0) a : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.1 : (a : Set α) → ℝ≥0) a) : Filter ℝ≥0)
⊢ Tendsto
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((i.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((i.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) b : ℝ≥0)))
have h'₁ : Tendsto (β := ℝ≥0)
  (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.2 : (a : Set β) → ℝ≥0) b : ℝ≥0)) (𝓝 μ)
  (𝓝 ((μ.2 : (a : Set β) → ℝ≥0) b) : Filter ℝ≥0)
Tactic: apply Filter.Tendsto.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : β) ↦ (f b : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s) (MeasurableSpace.map f mβ)
have rw : borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s) ∘ f) mβ
Tactic: rw [MeasurableSpace.map_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
⊢ MeasurableAdd₂.{u_3} (Measure α)
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 + b.2 : (a : Set α) → ℝ≥0∞) s
Tactic: refine ⟨Measure.measurable_of_measurable_coe _ fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((b.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((b.2 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine_1 : Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 : (a : Set α) → ℝ≥0∞) s
Tactic: refine Measurable.add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
refine_1 : Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 : (a : Set α) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((b.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((b.2 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine_2 : Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.2 : (a : Set α) → ℝ≥0∞) s
Tactic: refine Measurable.add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (x : α) ↦ f x • μ
have refine : ∀ (s : Set β) (hs : MeasurableSet s), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (f b • μ : (a : Set β) → ℝ≥0∞) s
Tactic: refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (f b • μ : (a : Set β) → ℝ≥0∞) s
have simp : Measurable (β := ℝ≥0∞) fun (b : α) ↦ HMul.hMul (β := ℝ≥0∞) (f b) ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [Measure.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
⊢ Measurable μ
have rw : ∀ (s : Set β), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
Tactic: rw [measurable_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s_1 s : Set β
hsm : MeasurableSet s
ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) sᶜ
have compl : Measurable (β := ℝ≥0∞) fun (b : α) ↦
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [measure_compl hsm (measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
have empty : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) ∅
Tactic: induction s, hs using MeasurableSpace.induction_on_inter hgen hpi with
  | empty => simp
  | basic s hs => exact h_basic s hs
  | compl s hsm ihs =>
    simp only [measure_compl hsm (measure_ne_top _ _)]
    exact h_univ.sub ihs
  | iUnion f hfd hfm ihf =>
    simpa only [measure_iUnion hfd hfm] using .tsum ihf
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s : Set β
hs : MeasurableSet s
empty : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) ∅
basic : ∀ (s : Set β) (hs : s ∈ S), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
have compl : ∀ (s : Set β) (hsm : MeasurableSet s) (ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) sᶜ
Tactic: induction s, hs using MeasurableSpace.induction_on_inter hgen hpi with
  | empty => simp
  | basic s hs => exact h_basic s hs
  | compl s hsm ihs =>
    simp only [measure_compl hsm (measure_ne_top _ _)]
    exact h_univ.sub ihs
  | iUnion f hfd hfm ihf =>
    simpa only [measure_iUnion hfd hfm] using .tsum ihf
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s : Set β
hs : MeasurableSet s
empty : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) ∅
basic : ∀ (s : Set β) (hs : s ∈ S), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
compl :
  ∀ (s : Set β) (hsm : MeasurableSet s) (ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) sᶜ
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
have iUnion : ∀ (f : ℕ → Set β) (hfd : Pairwise (Function.onFun Disjoint f)) (hfm : ∀ (i : ℕ), MeasurableSet (f i))
  (ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) (f i)),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) (⋃ (i : ℕ), f i)
Tactic: induction s, hs using MeasurableSpace.induction_on_inter hgen hpi with
  | empty => simp
  | basic s hs => exact h_basic s hs
  | compl s hsm ihs =>
    simp only [measure_compl hsm (measure_ne_top _ _)]
    exact h_univ.sub ihs
  | iUnion f hfd hfm ihf =>
    simpa only [measure_iUnion hfd hfm] using .tsum ihf
Cleared hypotheses: hs