awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
⊢ bayesRisk ℓ P π ≤
    ⨅ (y : 𝓨),
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
have simp_rw : ∀ (i : 𝓨),
  ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), avgRisk ℓ P κ π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ i)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
Tactic: simp_rw [le_iInf_iff, bayesRisk]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
⊢ ∀ (i : 𝓨),
    ⨅ (κ : Kernel 𝓧 𝓨), ⨅ (_ : IsMarkovKernel κ), avgRisk ℓ P κ π ≤
      ∫⁻ (θ : Θ),
        HMul.hMul (β := ℝ≥0∞) (ℓ θ i)
          ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
have refine : ∀ (y : 𝓨),
  ⨅ (_ : IsMarkovKernel (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac y))),
      avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac y)) π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
Tactic: refine fun y ↦ iInf_le_of_le (Kernel.const _ (Measure.dirac y)) ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
⊢ ⨅ (_ : IsMarkovKernel (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac y))),
      avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac y)) π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
have simp : ∫⁻ (θ : Θ),
    HMul.hMul (β := ℝ≥0∞) (∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y)
      ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
  ∫⁻ (θ : Θ),
    HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
Tactic: simp only [iInf_pos, avgRisk_const_right', mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
⊢ ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) (ℓ θ y)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
have hfg : ∀ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y ≤ ℓ θ y
Tactic: gcongr with θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
θ : Θ
⊢ ∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y ≤ ℓ θ y
have hfg : ℓ θ y ≤ ℓ θ y
Tactic: rw [lintegral_dirac' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
⊢ bayesRisk ℓ (Kernel.const Θ μ) π =
    ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
have refine : ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
  bayesRisk ℓ (Kernel.const Θ μ) π
Tactic: refine le_antisymm ((bayesRisk_le_iInf' hl _ _).trans_eq (by simp)) ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    bayesRisk ℓ (Kernel.const Θ μ) π
have simp_rw : ∀ (i : Kernel 𝓧 𝓨) (i_1 : IsMarkovKernel i),
  ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    avgRisk ℓ (Kernel.const Θ μ) i π
Tactic: simp_rw [bayesRisk, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    avgRisk ℓ (Kernel.const Θ μ) κ π
have rw : ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
  ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
Tactic: rw [avgRisk_const_left' hl]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂(⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ
have refine : ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : 𝓨), ∫⁻ (θ : Θ), ℓ θ x ∂π : ℝ≥0∞)
    ((((⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine le_trans ?_ (iInf_mul_le_lintegral (fun y ↦ ∫⁻ θ, ℓ θ y ∂π))
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
⊢ ⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : 𝓨), ∫⁻ (θ : Θ), ℓ θ x ∂π : ℝ≥0∞)
      ((((⇑κ : (a : 𝓧) → Measure 𝓨) ∘ₘ μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
  (⨅ (i : 𝓨), HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ i ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
Tactic: rw [Measure.comp_apply_univ, ENNReal.iInf_mul' hl_pos (fun hμ ↦ h_zero (by simpa using hμ))]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
⊢ LE.le (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π)
    (⨅ (i : 𝓨), HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ i ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞))
have h : ∀ (y : 𝓨),
  ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ y ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: gcongr with y
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst : SFinite μ
π : Measure Θ
inst_1 : SFinite π
hl_pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) 0 → ∃ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
κ : Kernel 𝓧 𝓨
hκ : IsMarkovKernel κ
y : 𝓨
⊢ ∫⁻ (θ : Θ), HMul.hMul (β := ℝ≥0∞) (ℓ θ y) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    HMul.hMul (β := ℝ≥0∞) (∫⁻ (θ : Θ), ℓ θ y ∂π) ((μ : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have h : Measurable (β := ℝ≥0∞) fun (θ : Θ) ↦ ℓ θ y
Tactic: rw [lintegral_mul_const]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ ∫⁻ (θ : Θ),
      (↑C : ℝ≥0∞) *
        ∫⁻ (x : 𝓧),
          (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ∂(P : (a : Θ) → Measure 𝓧) θ ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * ∫⁻ (x : 𝓧), κ.bound ∂(P : (a : Θ) → Measure 𝓧) θ ∂π
have hfg : ∀ (θ : Θ) (x : 𝓧), (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: gcongr with θ x
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
| ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * ∫⁻ (x : 𝓧), κ.bound ∂(P : (a : Θ) → Measure 𝓧) θ ∂π
have simp : ∫⁻ (θ : Θ),
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound)
    ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π
Tactic: simp only [lintegral_const, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * ∫⁻ (x : 𝓧), κ.bound ∂(P : (a : Θ) → Measure 𝓧) θ ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π
have conv_lhs : ∫⁻ (θ : Θ),
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound)
      ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
  ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π
Tactic: conv_lhs => simp only [lintegral_const, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ ∫⁻ (θ : Θ),
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound)
        ((((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ : ℝ≥0∞) ∂π ≤
    ∫⁻ (θ : Θ), (↑C : ℝ≥0∞) * κ.bound * P.bound ∂π
have hfg : ∀ (θ : Θ), (((P : (a : Θ) → Measure 𝓧) θ : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) Set.univ ≤ P.bound
Tactic: gcongr with θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ avgRisk ℓ P κ π ≤ (↑C : ℝ≥0∞)
have refine : HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: refine (avgRisk_le_mul' P κ π hℓC).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have inl : IsEmpty Θ →
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty Θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
inl :
  IsEmpty Θ →
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have inr : Nonempty Θ →
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty Θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
h : Nonempty Θ
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have inr : IsEmpty 𝓧 →
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty 𝓧
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst_1 : IsMarkovKernel κ
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
h : Nonempty Θ
inr :
  IsEmpty 𝓧 →
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have inr₁ : Nonempty 𝓧 →
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * κ.bound * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty 𝓧
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π ≤ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have refine : avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π ≤
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine (bayesRisk_le_avgRisk ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ avgRisk (m𝓨 := m𝓨) ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have refine : HMul.hMul (β := ℝ≥0∞)
    ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
    ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine (avgRisk_le_mul' P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π hℓC).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have inl : IsEmpty 𝓧 →
  HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty 𝓧
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
inl :
  IsEmpty 𝓧 →
    HMul.hMul (β := ℝ≥0∞)
        ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
        ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have inr : Nonempty 𝓧 →
  HMul.hMul (β := ℝ≥0∞)
      ((↑C : ℝ≥0∞) * Kernel.bound (mα := m𝓧) (mβ := m𝓨) (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) * P.bound)
      ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty 𝓧
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π ≤ (↑C : ℝ≥0∞)
have refine : HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: refine (bayesRisk_le_mul' P π hℓC).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have inl : IsEmpty Θ → HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty Θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsMarkovKernel P
π : Measure Θ
inst_2 : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
inl : IsEmpty Θ → HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
have inr : Nonempty Θ → HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞)
Tactic: rcases isEmpty_or_nonempty Θ
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst : Nonempty 𝓨
P : Kernel Θ 𝓧
inst_1 : IsFiniteKernel P
π : Measure Θ
inst_2 : IsFiniteMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ (↑C : ℝ≥0∞)
⊢ bayesRisk ℓ P π < ∞
have refine : HMul.hMul (β := ℝ≥0∞) ((↑C : ℝ≥0∞) * P.bound) ((π : (a : Set Θ) → ℝ≥0∞) Set.univ : ℝ≥0∞) < ∞
Tactic: refine (bayesRisk_le_mul' P π hℓC).trans_lt ?_
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst : SFinite π
⊢ bayesRisk ℓ (Kernel.discard Θ) π = ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π
have rw : bayesRisk (m𝓧 := PUnit.instMeasurableSpace) ℓ (Kernel.const Θ (Measure.dirac PUnit.unit)) π =
  ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π
Tactic: rw [Kernel.discard_eq_const, bayesRisk_const hl]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst : SFinite π
rw :
  bayesRisk (m𝓧 := PUnit.instMeasurableSpace) ℓ (Kernel.const Θ (Measure.dirac PUnit.unit)) π =
    ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π
⊢ bayesRisk ℓ (Kernel.discard Θ) π = ⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π
have rw₁ : Eq (α := ℝ≥0∞) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π) (⨅ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π)
Tactic: rw [Kernel.discard_eq_const, bayesRisk_const hl]
-- Lean 4 proof step from Mathlib.Probability.Decision.Risk.Basic (goal)
Goal:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst : Subsingleton 𝓧
inst_1 : Nonempty 𝓨
⊢ bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
have inl : ∀ (hX : IsEmpty 𝓧),
  bayesRisk ℓ P π = ⨅ (μ : Measure 𝓨), ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
Tactic: rcases isEmpty_or_nonempty 𝓧 with hX | hX