awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
⊢ ∃ ε > 0, ball x ε ⊆ u

Tactic:
Metric.isOpen_iff.1 u_open x xu

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.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_1 : IsPiSystem S
this_2 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
u : Set (α × β)
u_open : IsOpen[instTopologicalSpaceProd] u
x : α × β
xu : x ∈ u
h : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ u), ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

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

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.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_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
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
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

Tactic:
rcases exists_null_frontier_thickening (μ.1 : Measure α) {x.1} εpos with ⟨r, hr, μr⟩

Premises used: MeasureTheory.exists_null_frontier_thickening, Prod.fst, MeasureTheory.ProbabilityMeasure.toMeasure, Singleton.singleton
-- 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_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∞)
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
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u

Tactic:
rcases exists_null_frontier_thickening (μ.2 : Measure β) {x.2} εpos with ⟨r', hr', μr'⟩

Premises used: MeasureTheory.exists_null_frontier_thickening, MeasureTheory.ProbabilityMeasure.toMeasure, Singleton.singleton, Prod.snd
-- 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_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∞)
⊢ Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [thickening_singleton] at μr μr'

Premises used: Metric.thickening_singleton
-- 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_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∞)
⊢ Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [thickening_singleton] at μr μr'

Premises used: Metric.thickening_singleton
-- 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_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∞)
⊢ Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier (ball x.1 r)) : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [coeFn_def, μr]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_def
-- 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_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∞)
⊢ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier (ball x.2 r')) : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp [coeFn_def, μr']

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_def
-- 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_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
h₁ : ball x.1 r ×ˢ ball x.2 r' ⊆ u
⊢ ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ 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⟩, ?_, ?_⟩
-- 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_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∞)
⊢ x ∈ ball x.1 r ×ˢ ball x.2 r'

Tactic:
simp [hr.1, hr'.1]

Premises used: And.left
-- 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_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' ∈ 𝓝 x

Tactic:
exact (isOpen_ball.prod isOpen_ball).mem_nhds (by simp [hr.1, hr'.1])

Premises used: Metric.isOpen_ball, IsOpen.mem_nhds, IsOpen.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_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 ≤ ε
ht : r' ≤ ε
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε

Tactic:
gcongr
-- 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_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∞)
⊢ r ≤ ε

Tactic:
hr.2.le

Premises used: LT.lt.le, And.right
-- 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_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∞)
⊢ r' ≤ ε

Tactic:
hr'.2.le

Premises used: LT.lt.le, And.right
-- 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_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∞)
⊢ r ≤ ε

Tactic:
exacts [hr.2.le, hr'.2.le]

Premises used: LT.lt.le, And.right
-- 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_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∞)
rwa rwa₁ rwa₂ rwa₃ : ball (x.1, x.2) ε ⊆ u
⊢ ball x.1 ε ×ˢ ball x.2 ε ⊆ u

Tactic:
rwa [ball_prod_same]

Premises used: ball_prod_same