awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) x

Tactic:
simpa using fun i ↦ (rpos i).1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) univ i), r i ≤ ε
⊢ Subset (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
    (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε)

Tactic:
gcongr with i hi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
i : ι
hi : Membership.mem (γ := Set ι) univ i
⊢ r i ≤ ε

Tactic:
(rpos i).2.le

Premises used: LT.lt.le, And.right
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
i : ι
hi : Membership.mem (γ := Set ι) univ i
⊢ r i ≤ ε

Tactic:
exact (rpos i).2.le

Premises used: LT.lt.le, And.right
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ : ball x ε ⊆ u
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε) ⊆ u

Tactic:
rwa [← ball_pi _ εpos]

Premises used: ball_pi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this_1 : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun (i : ι) ↦ pseudoMetrizableSpacePseudoMetric (α i)
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : (i : ι) → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr :
  ∀ (i : ι),
    Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (thickening (r i) {x i})) : ℝ≥0∞)
      (0 : ℝ≥0∞)
calc :
  Subset (α := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i))
    (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε)
calc₁ : (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) ε) ⊆ u
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ ball (x i) (r i)) ⊆ u

Tactic:
calc univ.pi fun i ↦ ball (x i) (r i)
      _ ⊆ univ.pi fun i ↦ ball (x i) ε := by gcongr with i hi; exact (rpos i).2.le
      _ ⊆ u := by rwa [← ball_pi _ εpos]

Premises used: Set.univ, Metric.ball, Set.pi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
h' :
  Tendsto (β := ℝ≥0)
    (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦ ∏ i_1 : ι, (i i_1 : (a : Set (α i_1)) → ℝ≥0) (s i_1)) (𝓝 μ)
    (𝓝 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) (s i)))
⊢ Tendsto (β := ℝ≥0)
    (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦
      ((pi (α := α) i : (a : Set ((i : ι) → α i)) → ℝ≥0) (Set.pi (α := α) univ s) : ℝ≥0))
    (𝓝 μ)
    (𝓝
        ((((fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ) μ : ProbabilityMeasure ((i : ι) → α i)) :
            (a : Set ((i : ι) → α i)) → ℝ≥0)
          (Set.pi (α := α) univ s)) :
      Filter ℝ≥0)

Tactic:
simp only [pi_pi]

Premises used: MeasureTheory.ProbabilityMeasure.pi_pi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
apply :
  ∀ (i : ι) (hi : Membership.mem (γ := Finset ι) Finset.univ i),
    Tendsto (β := ℝ≥0) (fun (b : (i : ι) → ProbabilityMeasure (α i)) ↦ ((b i : (a : Set (α i)) → ℝ≥0) (s i) : ℝ≥0))
      (𝓝 μ) (𝓝 ((μ i : (a : Set (α i)) → ℝ≥0) (s i)) : Filter ℝ≥0)
⊢ Tendsto (β := ℝ≥0)
    (fun (i : (i : ι) → ProbabilityMeasure (α i)) ↦ ∏ i_1 : ι, (i i_1 : (a : Set (α i_1)) → ℝ≥0) (s i_1)) (𝓝 μ)
    (𝓝 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) (s i)))

Tactic:
apply tendsto_finsetProd _ (fun i hi ↦ ?_)

Premises used: tendsto_finsetProd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
i : ι
hi : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Tendsto (β := ℝ≥0) (fun (b : (i : ι) → ProbabilityMeasure (α i)) ↦ ((b i : (a : Set (α i)) → ℝ≥0) (s i) : ℝ≥0)) (𝓝 μ)
    (𝓝 ((μ i : (a : Set (α i)) → ℝ≥0) (s i)) : Filter ℝ≥0)

Tactic:
tendsto_measure_of_null_frontier_of_tendsto (Tendsto.apply_nhds (fun ⦃U⦄ a ↦ a) i) (hs i)

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
this : IsPiSystem S
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
i : ι
hi : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Tendsto (β := ℝ≥0) (fun (b : (i : ι) → ProbabilityMeasure (α i)) ↦ ((b i : (a : Set (α i)) → ℝ≥0) (s i) : ℝ≥0)) (𝓝 μ)
    (𝓝 ((μ i : (a : Set (α i)) → ℝ≥0) (s i)) : Filter ℝ≥0)

Tactic:
exact tendsto_measure_of_null_frontier_of_tendsto (Tendsto.apply_nhds (fun ⦃U⦄ a ↦ a) i) (hs i)

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
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.FiniteMeasure.coeFn_def, MeasureTheory.Measure.prod_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
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.FiniteMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
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.FiniteMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
simp :
  ENNReal.toNNReal
      (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
    ENNReal.toNNReal (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ) *
      ENNReal.toNNReal (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ)
⊢ (μ.prod ν).mass = μ.mass * ν.mass

Tactic:
simp only [coeFn_def, mass, univ_prod_univ.symm, toMeasure_prod]

Premises used: MeasureTheory.FiniteMeasure.mass, MeasureTheory.FiniteMeasure.coeFn_def, Set.univ_prod_univ, Eq.symm, MeasureTheory.FiniteMeasure.toMeasure_prod
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
rw :
  ENNReal.toNNReal
      (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
        (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)).toNNReal
⊢ ENNReal.toNNReal
      (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
    ENNReal.toNNReal (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ) *
      ENNReal.toNNReal (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ)

Tactic:
rw [← ENNReal.toNNReal_mul]

Premises used: ENNReal.toNNReal_mul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ ENNReal.toNNReal
      (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
        (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)).toNNReal

Tactic:
congr_arg ENNReal.toNNReal (Measure.prod_prod univ univ)

Premises used: Set.univ, ENNReal.toNNReal, MeasureTheory.Measure.prod_prod, congr_arg
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ ENNReal.toNNReal
      (((↑μ : Measure α).prod (↑ν : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set α) (β := Set β) univ univ)) =
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
        (((↑ν : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)).toNNReal

Tactic:
exact congr_arg ENNReal.toNNReal (Measure.prod_prod univ univ)

Premises used: Set.univ, ENNReal.toNNReal, MeasureTheory.Measure.prod_prod, congr_arg
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
ν : FiniteMeasure β
rw : mass (Ω := α × β) (prod 0 ν) = 0
rw₁ : mass.{u_1} (Ω := α) 0 * ν.mass = 0
rw₂ : 0 * ν.mass = 0
rw₃ rw₄ : Eq (α := ℝ≥0) 0 0
⊢ Eq (α := FiniteMeasure (α × β)) (prod 0 ν) 0

Tactic:
rw [← mass_zero_iff, mass_prod, zero_mass, zero_mul]

Premises used: MeasureTheory.FiniteMeasure.mass_prod, MulZeroClass.zero_mul, MeasureTheory.FiniteMeasure.zero_mass, MeasureTheory.FiniteMeasure.mass_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
rw₃ rw₄ : Eq (α := ℝ≥0) 0 0
⊢ Eq (α := FiniteMeasure (α × β)) (μ.prod 0) 0

Tactic:
rw [← mass_zero_iff, mass_prod, zero_mass, mul_zero]

Premises used: MeasureTheory.FiniteMeasure.mass_prod, MulZeroClass.mul_zero, MeasureTheory.FiniteMeasure.zero_mass, MeasureTheory.FiniteMeasure.mass_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
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∞)
⊢ (μ.prod ν).map Prod.fst = HSMul.hSMul (α := ℝ≥0) ((ν : (a : Set β) → ℝ≥0) univ : ℝ≥0) μ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s : Set α
h : 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:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
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∞)
⊢ (μ.prod ν).map Prod.snd = HSMul.hSMul (α := ℝ≥0) ((μ : (a : Set α) → ℝ≥0) univ : ℝ≥0) ν

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s : Set β
h : 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:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
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
a :
  Eq (α := Measure (α' × β')) (↑(prod (μ.map f) (ν.map g)) : Measure (α' × β'))
    (↑((μ.prod ν).map (Prod.map f g)) : Measure (α' × β'))
⊢ Eq (α := FiniteMeasure (α' × β')) (prod (μ.map f) (ν.map g)) ((μ.prod ν).map (Prod.map f g))

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 β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : 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 β
μ : FiniteMeasure α
ν : FiniteMeasure β
a : (↑((μ.prod ν).map Prod.swap) : Measure (β × α)) = (↑(ν.prod μ) : Measure (β × α))
⊢ (μ.prod ν).map Prod.swap = ν.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 β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (↑((μ.prod ν).map Prod.swap) : 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 β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ IsProbabilityMeasure ((↑μ : Measure α).prod (↑ν : Measure β))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (↑(μ.prod ν) : Measure (α × β)) = (↑μ : Measure α).prod (↑ν : Measure β)

Tactic:
rfl

Premises used: rfl