awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.sum fun (i : ↥T) ↦ (↑μ : Measure Ω).restrict (s (↑i : ι)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [Measure.sum_fintype, Finset.univ_eq_attach, Measure.coe_finsetSum, Finset.sum_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, MeasureTheory.Measure.sum_fintype, Finset.sum_apply, Finset.univ_eq_attach
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
rw : ∑ x ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑x : ι)) : (a : Set Ω) → ℝ≥0∞) t
| ∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t

Tactic:
rw [← Finset.sum_attach]

Premises used: Finset.sum_attach
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
conv_rhs :
  Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
h :
  Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ x ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑x : ι)) : (a : Set Ω) → ℝ≥0∞) t)
⊢ Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)

Tactic:
conv_rhs => rw [← Finset.sum_attach]

Premises used: Finset.sum_attach
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
rw : (μ.restrict A).mass = 0 ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
rw₁ rw₂ :
  Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0) ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
⊢ μ.restrict A = 0 ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [← mass_zero_iff, restrict_mass]

Premises used: MeasureTheory.FiniteMeasure.restrict_mass, MeasureTheory.FiniteMeasure.mass_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A ≠ 0 ↔ Ne (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
rw :
  MeasurableSet.{u_1} (α := Measure Ω)
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsFiniteMeasure μ}

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
⊢ MeasurableSet.{u_1} (α := Measure Ω)
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))

Tactic:
Measure.measurable_coe MeasurableSet.univ measurableSet_Ico

Premises used: MeasureTheory.Measure.measurable_coe, measurableSet_Ico, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
⊢ MeasurableSet.{u_1} (α := Measure Ω)
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))

Tactic:
exact Measure.measurable_coe MeasurableSet.univ measurableSet_Ico

Premises used: MeasureTheory.Measure.measurable_coe, measurableSet_Ico, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
suffices :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsFiniteMeasure μ}

Tactic:
suffices { μ : Measure Ω | IsFiniteMeasure μ } = (fun μ => μ univ) ⁻¹' (Set.Ico 0 ∞) by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ measurableSet_Ico
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
h :
  ∀ (μ : Measure Ω),
    Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ} μ ↔
      Membership.mem (γ := Set (Measure Ω))
        (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞)) μ
⊢ Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))

Tactic:
ext μ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
h : IsFiniteMeasure μ ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ} μ ↔
    Membership.mem (γ := Set (Measure Ω))
      (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞)) μ

Tactic:
simp only [mem_setOf_eq, mem_preimage, mem_Ico, zero_le, true_and]

Premises used: zero_le, Set.mem_Ico, Set.mem_setOf_eq, Set.mem_preimage, true_and
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
⊢ IsFiniteMeasure μ ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
isFiniteMeasure_iff μ

Premises used: MeasureTheory.isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
⊢ IsFiniteMeasure μ ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact isFiniteMeasure_iff μ

Premises used: MeasureTheory.isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
have Heval {u v} (Hu : MeasurableSet u) (Hv : MeasurableSet v) :
      Measurable fun a : (FiniteMeasure α × FiniteMeasure β) ↦
      a.1.toMeasure u * a.2.toMeasure v :=
    Measurable.mul
      ((Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst))
      ((Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd))
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
apply :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) univ
apply₁ :
  ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s →
      Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
        ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
⊢ Measurable (β := Measure (α × β)) fun (μ : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    (↑μ.1 : Measure α).prod (↑μ.2 : Measure β)

Tactic:
apply Measurable.measure_of_isPiSystem generateFrom_prod.symm isPiSystem_prod _

Premises used: isPiSystem_prod, generateFrom_prod, Measurable.measure_of_isPiSystem, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
      (SProd.sprod (α := Set α) (β := Set β) univ univ)
simp_rw₁ :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) univ

Tactic:
simp_rw [← Set.univ_prod_univ, Measure.prod_prod, Heval MeasurableSet.univ MeasurableSet.univ]

Premises used: MeasureTheory.Measure.prod_prod, Set.univ_prod_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
simp :
  ∀ (s : Set (α × β)) (x : Set α),
    MeasurableSet x →
      ∀ (x_1 : Set β),
        MeasurableSet x_1 →
          x ×ˢ x_1 = s →
            Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
              ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s →
      Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
        ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
simp only [mem_image2, mem_setOf_eq, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image2, forall_exists_index, Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
s : Set (α × β)
_ :
  ∀ (x : Set α),
    MeasurableSet x →
      ∀ (x_1 : Set β),
        MeasurableSet x_1 →
          x ×ˢ x_1 = s →
            Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
              ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∀ (x : Set α),
    MeasurableSet x →
      ∀ (x_1 : Set β),
        MeasurableSet x_1 →
          x ×ˢ x_1 = s →
            Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
              ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
s : Set (α × β)
x : Set α
Hu : MeasurableSet x
_ :
  ∀ (x_1 : Set β),
    MeasurableSet x_1 →
      x ×ˢ x_1 = s →
        Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
          ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∀ (x_1 : Set β),
    MeasurableSet x_1 →
      x ×ˢ x_1 = s →
        Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
          ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
s : Set (α × β)
x : Set α
Hu : MeasurableSet x
x_1 : Set β
Hv : MeasurableSet x_1
Heq : x ×ˢ x_1 = s
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) (x ×ˢ x_1)
simp_rw₁ :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) x_1 : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
simp_rw [← Heq, Measure.prod_prod, Heval Hu Hv]

Premises used: MeasureTheory.Measure.prod_prod
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
f : ℕ → Set Ω
hf : Summable (α := ℝ≥0) fun (n : ℕ) ↦ (μ : (a : Set Ω) → ℝ≥0) (f n)
⊢ LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (⋃ (n : ℕ), f n) : ℝ≥0) (∑' (n : ℕ), (μ : (a : Set Ω) → ℝ≥0) (f n) : ℝ≥0)

Tactic:
simpa [← ENNReal.coe_le_coe, ENNReal.coe_tsum hf] using MeasureTheory.measure_iUnion_le f

Premises used: ENNReal.coe_tsum, ENNReal.coe_le_coe, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
      ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
a : (↑μ : Measure Ω) = (↑ν : Measure Ω)
⊢ μ = ν

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
      ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ (↑μ : Measure Ω) = (↑ν : Measure Ω)

Tactic:
ext_of_forall_lintegral_eq_of_IsFiniteMeasure h

Premises used: MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
      ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ (↑μ : Measure Ω) = (↑ν : Measure Ω)

Tactic:
exact ext_of_forall_lintegral_eq_of_IsFiniteMeasure h

Premises used: MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
h₁ :
  ∀ (f : Ω →ᵇ ℝ≥0),
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
      ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ μ = ν

Tactic:
apply ext_of_forall_lintegral_eq

Premises used: MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
f : Ω →ᵇ ℝ≥0
h₁ :
  (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal =
    (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)).toReal
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)

Tactic:
apply (ENNReal.toReal_eq_toReal_iff' (lintegral_lt_top_of_nnreal μ f).ne
      (lintegral_lt_top_of_nnreal ν f).ne).mp

Premises used: ENNReal.toReal_eq_toReal_iff', BoundedContinuousFunction.lintegral_lt_top_of_nnreal, Iff.mp, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
f : Ω →ᵇ ℝ≥0
h₁ :
  Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
    (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑ν : Measure Ω))
⊢ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal =
    (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)).toReal

Tactic:
rw [toReal_lintegral_coe_eq_integral f μ, toReal_lintegral_coe_eq_integral f ν]

Premises used: BoundedContinuousFunction.toReal_lintegral_coe_eq_integral, MeasureTheory.FiniteMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
f : Ω →ᵇ ℝ≥0
⊢ Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
    (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑ν : Measure Ω))

Tactic:
h ⟨⟨fun x => (f x).toReal, Continuous.comp' NNReal.continuous_coe f.continuous⟩,
      f.map_bounded'⟩

Premises used: Continuous.comp', ContinuousMap.mk, NNReal.continuous_coe, BoundedContinuousFunction.continuous, BoundedContinuousFunction.mk, BoundedContinuousFunction.map_bounded', DFunLike.coe, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
f : Ω →ᵇ ℝ≥0
⊢ Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
    (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑ν : Measure Ω))

Tactic:
exact h ⟨⟨fun x => (f x).toReal, Continuous.comp' NNReal.continuous_coe f.continuous⟩,
      f.map_bounded'⟩

Premises used: Continuous.comp', ContinuousMap.mk, NNReal.continuous_coe, BoundedContinuousFunction.continuous, BoundedContinuousFunction.mk, BoundedContinuousFunction.map_bounded', DFunLike.coe, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ (↑(μ.testAgainstNN f) : ℝ≥0∞) = ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
ENNReal.coe_toNNReal (f.lintegral_lt_top_of_nnreal _).ne

Premises used: ENNReal.coe_toNNReal, BoundedContinuousFunction.lintegral_lt_top_of_nnreal, MeasureTheory.FiniteMeasure.testAgainstNN, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
c : ℝ≥0
⊢ μ.testAgainstNN (const Ω c) = c * μ.mass

Tactic:
simp [← ENNReal.coe_inj]

Premises used: ENNReal.coe_inj
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : LE.le (α := (a : Ω) → ℝ≥0) (⇑f : (a : Ω) → ℝ≥0) (⇑g : (a : Ω) → ℝ≥0)
simp :
  ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
    ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g

Tactic:
simp only [← ENNReal.coe_le_coe, testAgainstNN_coe_eq]

Premises used: MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : LE.le (α := (a : Ω) → ℝ≥0) (⇑f : (a : Ω) → ℝ≥0) (⇑g : (a : Ω) → ℝ≥0)
hfg : ∀ (x : Ω), LE.le (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) x : ℝ≥0) ((g : (a : Ω) → ℝ≥0) x : ℝ≥0)
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
    ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : LE.le (α := (a : Ω) → ℝ≥0) (⇑f : (a : Ω) → ℝ≥0) (⇑g : (a : Ω) → ℝ≥0)
x : Ω
⊢ LE.le (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) x : ℝ≥0) ((g : (a : Ω) → ℝ≥0) x : ℝ≥0)

Tactic:
apply f_le_g
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 0 = 0

Tactic:
simpa only [zero_mul] using μ.testAgainstNN_const 0

Premises used: MeasureTheory.FiniteMeasure.testAgainstNN_const, MulZeroClass.zero_mul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
simp : ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) = μ.mass
⊢ μ.testAgainstNN 1 = μ.mass

Tactic:
simp only [testAgainstNN, coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_one]

Premises used: BoundedContinuousFunction.coe_one, Pi.one_apply, ENNReal.coe_one, MeasureTheory.FiniteMeasure.testAgainstNN, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) = μ.mass

Tactic:
rfl