awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
s : Set β
hs : MeasurableSet s
hs_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (a : α) ↦ ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)) x)
                    (0 x))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (a : α) ↦
                        AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                          ((η : (a : α) → Measure β) a))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := ℝ≥0∞)
                          ((fun (a : α) ↦ ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞))
                            x)
                          (0 x))
                      x}
                  x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
have h₁ : ∀ (a : α),
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 a : ℝ≥0∞) →
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a) →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 a : ℝ≥0∞)
Tactic: filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
⊢ ∀ᵐ (ω : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) ω) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have rw : ∀ (x : α),
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) →
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) x)
      (sum fun (ω : α) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
          ((κ : (a : α) → Measure β) ω : Measure β))
Tactic: rw [Measure.comp_eq_sum_of_countable, ae_iff_of_countable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ κ ∘ₖ boolKernel μ ν = boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν)
have h : ∀ (b : Bool),
  Eq (α := Measure β) ((κ ∘ₖ boolKernel μ ν : (a : Bool) → Measure β) b : Measure β)
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) b :
      Measure β)
Tactic: ext b : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
b : Bool
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) b)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) b)
have h : Eq.{u_2 + 1} (α := Measure β)
  (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) false)
    (⇑κ : (a : α) → Measure β))
  ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) false)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
b : Bool
h :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) false)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) false)
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) b)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) b)
have h₁ : Eq.{u_2 + 1} (α := Measure β)
  (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) true)
    (⇑κ : (a : α) → Measure β))
  ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) true)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
⊢ (⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π =
    HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
      HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
            HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
            HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (a : Bool), (((Kernel.boolKernel μ ν : (a : Bool) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
  (HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
        HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
      (a : Set α) → ℝ≥0∞)
    s
Tactic: rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ μ ⊗ₘ κ = 0
have h₁ : ¬IsSFiniteKernel (mα := PUnit.instMeasurableSpace) (Kernel.const Unit μ)
Tactic: rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_left, Kernel.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = 0
have h₁ : ¬IsSFiniteKernel (mα := Prod.instMeasurableSpace) (Kernel.prodMkLeft Unit κ)
Tactic: rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_right, Kernel.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
have simp_rw : (((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β)) :
      (a : Set (α × β)) → ℝ≥0∞)
    s =
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
Tactic: simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
simp_rw :
  (((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β)) :
        (a : Set (α × β)) → ℝ≥0∞)
      s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
have simp_rw₁ : ∫⁻ (b : α),
    ((((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) ((), b) : Measure β) :
        (a : Set β) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
Tactic: simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
simp_rw :
  (((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β)) :
        (a : Set (α × β)) → ℝ≥0∞)
      s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
simp_rw₁ :
  ∫⁻ (b : α),
      ((((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) ((), b) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
have simp_rw₂ : ∫⁻ (b : α),
    ((((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) ((), b) : Measure β) :
        (a : Set β) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂μ =
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
Tactic: simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
⊢ Eq (α := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
have e_a : Eq (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
  (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
⊢ Eq (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η)
have e_a : ∀ (a : Unit),
  ∀ᵐ (b : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) a : Measure α),
    Eq.{u_2 + 1} (α := Measure β)
      (((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) (a, b) : Measure β)
      (((Kernel.prodMkLeft Unit η : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) (a, b) : Measure β)
Tactic: refine Kernel.compProd_congr ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = 0 ↔ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
have refine_1 : ∀ (h : μ ⊗ₘ κ = 0),
  ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
refine_1 :
  ∀ (h : μ ⊗ₘ κ = 0),
    ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ μ ⊗ₘ κ = 0 ↔ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
have refine_2 : ∀ (h : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)),
  μ ⊗ₘ κ = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
have refine_1 : ∀ᵐ (a : α) ∂μ, Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0
Tactic: refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0
have refine_1 : Eq (α := ℝ≥0∞) ((0 : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, ← compProd_apply_prod .univ .univ, h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ μ ⊗ₘ κ = 0
have refine_2 : μ ⊗ₘ κ = μ ⊗ₘ 0
Tactic: rw [← compProd_zero_right μ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ (κ ⊗ₖ η : (a : α) → Measure (β × γ)) a = (κ : (a : α) → Measure β) a ⊗ₘ η.sectR a
have h : ∀ (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((κ : (a : α) → Measure β) a ⊗ₘ η.sectR a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((κ : (a : α) → Measure β) a ⊗ₘ η.sectR a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ((κ : (a : α) → Measure β) a ⊗ₘ η.sectR a : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ((κ : (a : α) → Measure β) a ⊗ₘ η.sectR a : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((κ : (a : α) → Measure β) a ⊗ₘ η.sectR a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (a_1 : β),
    (((η.sectR a : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ μ ⊗ₘ Kernel.id = map (fun (x : α) ↦ (x, x)) μ
have h : ∀ (s : Set (α × α)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.id : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (fun (x : α) ↦ (x, x)) μ : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.id : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (fun (x : α) ↦ (x, x)) μ : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α), (((Kernel.id : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
  (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
Tactic: rw [compProd_apply hs, map_apply (measurable_id.prod measurable_id) hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (((Kernel.id : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
have h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
Tactic: have h_meas a : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (((Kernel.id : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
have h : ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
Tactic: simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), indicator ((fun (x : α) ↦ (x, x)) ⁻¹' s) 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
have rw : MeasurableSet (α := α) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
Tactic: rw [lintegral_indicator_one]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
have calc : ∫⁻ (a : α), indicator ((fun (x : α) ↦ (x, x)) ⁻¹' s) 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
Tactic: calc ∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ
  _ = ∫⁻ a, ((fun x ↦ (x, x)) ⁻¹' s).indicator 1 a ∂μ := rfl
  _ = μ ((fun x ↦ (x, x)) ⁻¹' s) := by
    rw [lintegral_indicator_one]
    exact (measurable_id.prod measurable_id) hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : α → Prop
hp : MeasurableSet.{u_1} (α := α) {x : α | p x}
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b).1
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b).1) x} x}
    a
Tactic: filter_upwards [h] with a ha using by simp [ha]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : α → Prop
hp : MeasurableSet.{u_1} (α := α) {x : α | p x}
h : ∀ᵐ (a : α) ∂μ, p a
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b).1) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b).1
have h₂ : ∀ (a : α), p a → ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p a
Tactic: filter_upwards [h] with a ha using by simp [ha]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
⊢ μ ⊗ₘ Kernel.const α ν = μ.prod ν
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.const α ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs