awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : μ.mass * 0 = 0
⊢ Eq (α := FiniteMeasure (α × β)) (μ.prod 0) 0
have rw₃ : Eq (α := ℝ≥0) 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 α
ν : FiniteMeasure β
⊢ (μ.prod ν).map Prod.fst = HSMul.hSMul (α := ℝ≥0) ((ν : (a : Set β) → ℝ≥0) univ : ℝ≥0) μ
have h : ∀ (s : Set α),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((↑((μ.prod ν).map Prod.fst) : Measure α) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((↑(HSMul.hSMul (α := ℝ≥0) ((ν : (a : Set β) → ℝ≥0) univ : ℝ≥0) μ) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- 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 ν).map Prod.snd = HSMul.hSMul (α := ℝ≥0) ((μ : (a : Set α) → ℝ≥0) univ : ℝ≥0) ν
have h : ∀ (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((↑((μ.prod ν).map Prod.snd) : Measure β) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((↑(HSMul.hSMul (α := ℝ≥0) ((μ : (a : Set α) → ℝ≥0) univ : ℝ≥0) ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst_2 : MeasurableSpace α'
β' : Type u_4
inst_3 : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Eq (α := FiniteMeasure (α' × β')) (prod (μ.map f) (ν.map g)) ((μ.prod ν).map (Prod.map f g))
have a : Eq (α := Measure (α' × β')) (↑(prod (μ.map f) (ν.map g)) : Measure (α' × β'))
  (↑((μ.prod ν).map (Prod.map f g)) : Measure (α' × β'))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst_2 : MeasurableSpace α'
β' : Type u_4
inst_3 : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Eq (α := Measure (α' × β')) (Measure.prod (Measure.map f (↑μ : Measure α)) (Measure.map g (↑ν : Measure β)))
    (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
have a : Eq (α := Measure (α' × β')) (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
  (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
Tactic: rw [Measure.map_prod_map _ _ f_mble g_mble]
-- 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 ν).map Prod.swap = ν.prod μ
have a : (↑((μ.prod ν).map Prod.swap) : Measure (β × α)) = (↑(ν.prod μ) : Measure (β × α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = μ
have a : (↑((μ.prod ν).map sorry) : Measure α) = (↑μ : Measure α)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = ν
have a : (↑((μ.prod ν).map sorry) : Measure β) = (↑ν : Measure β)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst_2 : MeasurableSpace α'
β' : Type u_4
inst_3 : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯
have a : (↑((μ.map sorry).prod (ν.map sorry)) : Measure (α' × β')) = (↑((μ.prod ν).map sorry) : Measure (α' × β'))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst_2 : MeasurableSpace α'
β' : Type u_4
inst_3 : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Eq (α := Measure (α' × β')) (Measure.prod (Measure.map f (↑μ : Measure α)) (Measure.map g (↑ν : Measure β)))
    (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
have a : Eq (α := Measure (α' × β')) (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
  (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
Tactic: rw [Measure.map_prod_map _ _ f_mble g_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureProd (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = ν.prod μ
have a : (↑((μ.prod ν).map sorry) : Measure (β × α)) = (↑(ν.prod μ) : Measure (β × α))
Tactic: apply Subtype.ext
-- 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 β
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace]
    fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2
have refine : ∀ (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)),
  ContinuousAt (Y := ProbabilityMeasure (α × β))
    (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ
Tactic: refine continuous_iff_continuousAt.2 (fun μ ↦ ?_)
-- 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}
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)
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a') : ℝ≥0) (0 : ℝ≥0)
b'meas : MeasurableSet b'
hb' : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b') : ℝ≥0) (0 : ℝ≥0)
⊢ a ×ˢ b ∩ a' ×ˢ b' ∈ S
have refine_1 : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier (a ∩ a')) : ℝ≥0) (0 : ℝ≥0)
Tactic: refine ⟨a ∩ a', b ∩ b', ameas.inter a'meas, ?_, bmeas.inter b'meas, ?_, prod_inter_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}
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)
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a') : ℝ≥0) (0 : ℝ≥0)
b'meas : MeasurableSet b'
hb' : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b') : ℝ≥0) (0 : ℝ≥0)
refine_1 : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier (a ∩ a')) : ℝ≥0) (0 : ℝ≥0)
⊢ a ×ˢ b ∩ a' ×ˢ b' ∈ S
have refine_2 : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier (b ∩ b')) : ℝ≥0) (0 : ℝ≥0)
Tactic: refine ⟨a ∩ a', b ∩ b', ameas.inter a'meas, ?_, bmeas.inter b'meas, ?_, prod_inter_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}
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)
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a') : ℝ≥0) (0 : ℝ≥0)
b'meas : MeasurableSet b'
hb' : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b') : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier (a ∩ a')) : ℝ≥0) (0 : ℝ≥0)
have refine_1 : ∀ (ha : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier a) : ℝ≥0∞) (0 : ℝ≥0∞))
  (bmeas : MeasurableSet b) (hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)) (a' : Set α)
  (b' : Set β) (a'meas : MeasurableSet a')
  (ha' : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier a') : ℝ≥0∞) (0 : ℝ≥0∞))
  (b'meas : MeasurableSet b') (hb' : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b') : ℝ≥0) (0 : ℝ≥0)),
  Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (a ∩ a')) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [null_iff_toMeasure_null] at ha ha' ⊢
Cleared hypotheses: ha, bmeas, hb, a', b', a'meas, ha', b'meas, hb'
-- 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}
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)
a' : Set α
b' : Set β
a'meas : MeasurableSet a'
ha' : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a') : ℝ≥0) (0 : ℝ≥0)
b'meas : MeasurableSet b'
hb' : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b') : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier (b ∩ b')) : ℝ≥0) (0 : ℝ≥0)
have refine_2 : ∀ (hb : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier b) : ℝ≥0∞) (0 : ℝ≥0∞)) (a' : Set α)
  (b' : Set β) (a'meas : MeasurableSet a')
  (ha' : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a') : ℝ≥0) (0 : ℝ≥0)) (b'meas : MeasurableSet b')
  (hb' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier b') : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (b ∩ b')) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [null_iff_toMeasure_null] at hb hb' ⊢
Cleared hypotheses: hb, a', b', a'meas, ha', b'meas, hb'
-- 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}
⊢ ContinuousAt (Y := ProbabilityMeasure (α × β))
    (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ
have this : IsPiSystem S
Tactic: have : IsPiSystem S := by
    rintro - ⟨a, b, ameas, ha, bmeas, hb, rfl⟩ - ⟨a', b', a'meas, ha', b'meas, hb', rfl⟩ -
    refine ⟨a ∩ a', b ∩ b', ameas.inter a'meas, ?_, bmeas.inter b'meas, ?_, prod_inter_prod⟩
    · rw [null_iff_toMeasure_null] at ha ha' ⊢
      exact null_frontier_inter ha ha'
    · rw [null_iff_toMeasure_null] at hb hb' ⊢
      exact null_frontier_inter hb hb'
-- 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
⊢ ContinuousAt (Y := ProbabilityMeasure (α × β))
    (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ
have hmeas : ∀ s ∈ S, MeasurableSet s
Tactic: apply this.tendsto_probabilityMeasure_of_tendsto_of_mem
-- 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
hmeas : ∀ s ∈ S, MeasurableSet s
⊢ ContinuousAt (Y := ProbabilityMeasure (α × β))
    (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ
have h : ∀ (u : Set (α × β)), IsOpen[instTopologicalSpaceProd] 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.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
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set (α × β)), IsOpen[instTopologicalSpaceProd] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
⊢ ContinuousAt (Y := ProbabilityMeasure (α × β))
    (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ
have h' : ∀ s ∈ S,
  Tendsto (β := ℝ≥0)
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      ((i.1.prod i.2 : (a : Set (α × β)) → ℝ≥0) s : ℝ≥0))
    (𝓝 μ)
    (𝓝
        ((((fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ :
              ProbabilityMeasure (α × β)) :
            (a : Set (α × β)) → ℝ≥0)
          s) :
      Filter ℝ≥0)
Tactic: apply this.tendsto_probabilityMeasure_of_tendsto_of_mem
-- 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
⊢ ∃ 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.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
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h : ∀ (r : ℝ) (hr : r ∈ Ioo 0 ε)
  (μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (thickening r {x.1})) : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
Tactic: rcases exists_null_frontier_thickening (μ.1 : Measure α) {x.1} εpos with ⟨r, hr, μ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 : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (thickening r {x.1})) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have h : ∀ (r' : ℝ) (hr' : r' ∈ Ioo 0 ε)
  (μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (thickening r' {x.2})) : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
Tactic: rcases exists_null_frontier_thickening (μ.2 : Measure β) {x.2} εpos with ⟨r', hr', μr'⟩
-- 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∞)
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
have μr₁ : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [thickening_singleton] at μr μr'
Cleared hypotheses: μr, μr'