awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0) s =
    (∫⁻ (x : α), ((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂(↑μ : Measure α)).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply s_mble]

Premises used: MeasureTheory.Measure.prod_apply, MeasureTheory.ProbabilityMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0) s =
    (∫⁻ (y : β), ((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s) ∂(↑ν : Measure β)).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply_symm s_mble]

Premises used: MeasureTheory.Measure.prod_apply_symm, MeasureTheory.ProbabilityMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set α
t : Set β
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set α) → ℝ≥0) s : ℝ≥0) ((ν : (a : Set β) → ℝ≥0) t : ℝ≥0)

Tactic:
simp [coeFn_def]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
a : (↑((μ.prod ν).map ⋯) : Measure α) = (↑μ : Measure α)
⊢ (μ.prod ν).map ⋯ = μ

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (↑((μ.prod ν).map ⋯) : Measure α) = (↑μ : Measure α)

Tactic:
simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod,
             measure_univ, one_smul]

Premises used: MeasureTheory.Measure.map_fst_prod, MeasureTheory.ProbabilityMeasure.toMeasure_prod, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, MeasureTheory.ProbabilityMeasure.val_eq_to_measure, MeasureTheory.ProbabilityMeasure.toMeasure_map
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
a : (↑((μ.prod ν).map ⋯) : Measure β) = (↑ν : Measure β)
⊢ (μ.prod ν).map ⋯ = ν

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (↑((μ.prod ν).map ⋯) : Measure β) = (↑ν : Measure β)

Tactic:
simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_snd_prod,
             measure_univ, one_smul]

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure_prod, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, MeasureTheory.ProbabilityMeasure.val_eq_to_measure, MeasureTheory.ProbabilityMeasure.toMeasure_map, MeasureTheory.Measure.map_snd_prod
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
a : (↑((μ.map ⋯).prod (ν.map ⋯)) : Measure (α' × β')) = (↑((μ.prod ν).map ⋯) : Measure (α' × β'))
⊢ (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
a a₁ :
  Eq (α := Measure (α' × β')) (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
    (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))
⊢ Eq (α := Measure (α' × β')) (Measure.prod (Measure.map f (↑μ : Measure α)) (Measure.map g (↑ν : Measure β)))
    (Measure.map (Prod.map f g) ((↑μ : Measure α).prod (↑ν : Measure β)))

Tactic:
rw [Measure.map_prod_map _ _ f_mble g_mble]

Premises used: MeasureTheory.Measure.map_prod_map
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
a : (↑((μ.prod ν).map ⋯) : Measure (β × α)) = (↑(ν.prod μ) : Measure (β × α))
⊢ (μ.prod ν).map ⋯ = ν.prod μ

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (↑((μ.prod ν).map ⋯) : Measure (β × α)) = (↑(ν.prod μ) : Measure (β × α))

Tactic:
simp [Measure.prod_swap]

Premises used: MeasureTheory.Measure.prod_swap
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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

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

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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 β
refine :
  ∀ (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)),
    ContinuousAt (Y := ProbabilityMeasure (α × β))
      (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace]
    fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2

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

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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

Tactic:
⟨a ∩ a', b ∩ b', ameas.inter a'meas, ?_, bmeas.inter b'meas, ?_, prod_inter_prod⟩

Premises used: Set.Mem, setOf, Inter.inter, And.intro, Exists.intro, Set.prod_inter_prod, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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)
refine_2 : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier (b ∩ b')) : ℝ≥0) (0 : ℝ≥0)
⊢ a ×ˢ b ∩ a' ×ˢ b' ∈ S

Tactic:
refine ⟨a ∩ a', b ∩ b', ameas.inter a'meas, ?_, bmeas.inter b'meas, ?_, prod_inter_prod⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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 :
  ∀ (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∞)
⊢ Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier (a ∩ a')) : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [null_iff_toMeasure_null] at ha ha' ⊢

Premises used: MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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 : 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:
null_frontier_inter ha ha'

Premises used: null_frontier_inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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 : 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:
exact null_frontier_inter ha ha'

Premises used: null_frontier_inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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_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∞)
⊢ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier (b ∩ b')) : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [null_iff_toMeasure_null] at hb hb' ⊢

Premises used: MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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 : 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:
null_frontier_inter hb hb'

Premises used: null_frontier_inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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 : 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:
exact null_frontier_inter hb hb'

Premises used: null_frontier_inter
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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}
⊢ 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'
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
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)
⊢ ContinuousAt (Y := ProbabilityMeasure (α × β))
    (fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ

Tactic:
apply this.tendsto_probabilityMeasure_of_tendsto_of_mem

Premises used: IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
bmeas : MeasurableSet b
⊢ MeasurableSet (a ×ˢ b)

Tactic:
ameas.prod bmeas

Premises used: MeasurableSet.prod
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
bmeas : MeasurableSet b
⊢ MeasurableSet (a ×ˢ b)

Tactic:
exact ameas.prod bmeas

Premises used: MeasurableSet.prod