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
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ℝ
hr : r ∈ Ioo 0 ε
r' : ℝ
hr' : r' ∈ Ioo 0 ε
μr : Eq (α := ℝ≥0∞) (((↑μ.1 : Measure α) : (a : Set α) → ℝ≥0∞) (frontier (ball x.1 r)) : ℝ≥0∞) (0 : ℝ≥0∞)
μr' : Eq (α := ℝ≥0∞) (((↑μ.2 : Measure β) : (a : Set β) → ℝ≥0∞) (frontier (ball x.2 r')) : ℝ≥0∞) (0 : ℝ≥0∞)
calc : ball x.1 r ×ˢ ball x.2 r' ⊆ ball x.1 ε ×ˢ ball x.2 ε
calc₁ : ball x.1 ε ×ˢ ball x.2 ε ⊆ u
⊢ ball x.1 r ×ˢ ball x.2 r' ⊆ u

Tactic:
calc ball x.1 r ×ˢ ball x.2 r'
      _ ⊆ ball x.1 ε ×ˢ ball x.2 ε := by gcongr; exacts [hr.2.le, hr'.2.le]
      _ ⊆ _ := by rwa [ball_prod_same]

Premises used: Metric.ball, Prod.fst, 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 : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
h' :
  Tendsto
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((i.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((i.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) b : ℝ≥0)))
⊢ Tendsto (β := ℝ≥0)
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      ((i.1.prod i.2 : (a : Set (α × β)) → ℝ≥0) (a ×ˢ b) : ℝ≥0))
    (𝓝 μ)
    (𝓝
        ((((fun (μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ μ.1.prod μ.2) μ :
              ProbabilityMeasure (α × β)) :
            (a : Set (α × β)) → ℝ≥0)
          (a ×ˢ b)) :
      Filter ℝ≥0)

Tactic:
simp only [prod_prod]

Premises used: MeasureTheory.ProbabilityMeasure.prod_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
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
h' :
  Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.1 : (a : Set α) → ℝ≥0) a : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.1 : (a : Set α) → ℝ≥0) a) : Filter ℝ≥0)
h'₁ :
  Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.2 : (a : Set β) → ℝ≥0) b) : Filter ℝ≥0)
⊢ Tendsto
    (fun (i : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦
      HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((i.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((i.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) a : ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) b : ℝ≥0)))

Tactic:
apply Filter.Tendsto.mul

Premises used: Filter.Tendsto.mul
-- 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
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.1 : (a : Set α) → ℝ≥0) a : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.1 : (a : Set α) → ℝ≥0) a) : Filter ℝ≥0)

Tactic:
tendsto_measure_of_null_frontier_of_tendsto tendsto_id.fst_nhds ha

Premises used: Filter.tendsto_id, Filter.Tendsto.fst_nhds, 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 β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.1 : (a : Set α) → ℝ≥0) a : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.1 : (a : Set α) → ℝ≥0) a) : Filter ℝ≥0)

Tactic:
exact tendsto_measure_of_null_frontier_of_tendsto tendsto_id.fst_nhds ha

Premises used: Filter.tendsto_id, Filter.Tendsto.fst_nhds, 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 β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.2 : (a : Set β) → ℝ≥0) b) : Filter ℝ≥0)

Tactic:
tendsto_measure_of_null_frontier_of_tendsto tendsto_id.snd_nhds hb

Premises used: Filter.tendsto_id, Filter.Tendsto.snd_nhds, 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 β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SecondCountableTopology α
inst_5 : SecondCountableTopology β
inst_6 : PseudoMetrizableSpace α
inst_7 : PseudoMetrizableSpace β
inst_8 : OpensMeasurableSpace α
inst_9 : OpensMeasurableSpace β
μ : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)
S : Set (Set (α × β)) :=
  {t : Set (α × β) |
    ∃ (a : Set α) (b : Set β),
      MeasurableSet a ∧
        Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0) ∧
          MeasurableSet b ∧ Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0) ∧ t = a ×ˢ b}
this : IsPiSystem S
a : Set α
b : Set β
ameas : MeasurableSet a
ha : Eq (α := ℝ≥0) ((μ.1 : (a : Set α) → ℝ≥0) (frontier a) : ℝ≥0) (0 : ℝ≥0)
bmeas : MeasurableSet b
hb : Eq (α := ℝ≥0) ((μ.2 : (a : Set β) → ℝ≥0) (frontier b) : ℝ≥0) (0 : ℝ≥0)
⊢ Tendsto (β := ℝ≥0)
    (fun (x : Prod.{u_1, u_2} (ProbabilityMeasure α) (ProbabilityMeasure β)) ↦ ((x.2 : (a : Set β) → ℝ≥0) b : ℝ≥0))
    (𝓝 μ) (𝓝 ((μ.2 : (a : Set β) → ℝ≥0) b) : Filter ℝ≥0)

Tactic:
exact tendsto_measure_of_null_frontier_of_tendsto tendsto_id.snd_nhds hb

Premises used: Filter.tendsto_id, Filter.Tendsto.snd_nhds, MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
Measurable.of_comap_le <| le_iSup_of_le s <| le_iSup_of_le hs <| le_rfl

Premises used: le_rfl, Measurable.of_comap_le, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : β) ↦ (f b : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : MeasurableSet s
rw : borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s) ∘ f) mβ
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s) (MeasurableSpace.map f mβ)

Tactic:
rw [MeasurableSpace.map_comp]

Premises used: MeasurableSpace.map_comp
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : β) ↦ (f b : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s) ∘ f) mβ

Tactic:
h s hs

Premises used: MeasurableSet, Measurable, setOf, Set.preimage, ENNReal, WithTop
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : β) ↦ (f b : (a : Set α) → ℝ≥0∞) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) s) ∘ f) mβ

Tactic:
exact h s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
⊢ MeasurableAdd₂.{u_3} (Measure α)

Tactic:
⟨Measure.measurable_of_measurable_coe _ fun s hs => ?_⟩

Premises used: MeasurableAdd₂.mk, MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 + b.2 : (a : Set α) → ℝ≥0∞) s
⊢ MeasurableAdd₂.{u_3} (Measure α)

Tactic:
refine ⟨Measure.measurable_of_measurable_coe _ fun s hs => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((b.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((b.2 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
Measurable.add ?_ ?_

Premises used: Measurable.add
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
refine_1 : Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 : (a : Set α) → ℝ≥0∞) s
refine_2 : Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.2 : (a : Set α) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((b.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((b.2 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine Measurable.add ?_ ?_

Premises used: Measurable.add
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 : (a : Set α) → ℝ≥0∞) s

Tactic:
(Measure.measurable_coe hs).comp measurable_fst

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.1 : (a : Set α) → ℝ≥0∞) s

Tactic:
exact (Measure.measurable_coe hs).comp measurable_fst

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.2 : (a : Set α) → ℝ≥0∞) s

Tactic:
(Measure.measurable_coe hs).comp measurable_snd

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α_1 : Type u_1
β : Type u_2
mα : MeasurableSpace α_1
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α × Measure α) ↦ (b.2 : (a : Set α) → ℝ≥0∞) s

Tactic:
exact (Measure.measurable_coe hs).comp measurable_snd

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (x : α) ↦ f x • μ

Tactic:
Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
refine : ∀ (s : Set β) (hs : MeasurableSet s), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (f b • μ : (a : Set β) → ℝ≥0∞) s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (x : α) ↦ f x • μ

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
s : Set β
hs : MeasurableSet s
simp : Measurable (β := ℝ≥0∞) fun (b : α) ↦ HMul.hMul (β := ℝ≥0∞) (f b) ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (f b • μ : (a : Set β) → ℝ≥0∞) s

Tactic:
simp only [Measure.smul_apply, smul_eq_mul]

Premises used: MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ HMul.hMul (β := ℝ≥0∞) (f b) ((μ : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
⊢ Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s

Tactic:
⟨fun hμ _s hs => (measurable_coe hs).comp hμ, measurable_of_measurable_coe μ⟩

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp, Iff.intro, MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
rw : ∀ (s : Set β), MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
⊢ Measurable μ

Tactic:
rw [measurable_measure]

Premises used: MeasureTheory.Measure.measurable_measure
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s : Set β
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s_1 s : Set β
hs : s ∈ S
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s

Tactic:
h_basic s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s_1 s : Set β
hs : s ∈ S
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s

Tactic:
exact h_basic s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s_1 s : Set β
hsm : MeasurableSet s
ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
compl :
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) sᶜ

Tactic:
simp only [measure_compl hsm (measure_ne_top _ _)]

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s_1 s : Set β
hsm : MeasurableSet s
ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
h_univ.sub ihs

Premises used: Measurable.sub
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s_1 s : Set β
hsm : MeasurableSet s
ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) ((μ b : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact h_univ.sub ihs

Premises used: Measurable.sub
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s : Set β
f : ℕ → Set β
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) (f i)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) (⋃ (i : ℕ), f i)

Tactic:
simpa only [measure_iUnion hfd hfm] using .tsum ihf

Premises used: MeasureTheory.measure_iUnion