awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.withDensity ((κ : (a : α) → Measure β) a) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (((Measure.withDensity ((κ : (a : α) → Measure β) a) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.withDensity ((κ : (a : α) → Measure β) a) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg, withDensity_congr_ae (hfg a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
have pos : ∀ (hf : Measurable (Function.uncurry f)),
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
pos :
  ∀ (hf : Measurable (Function.uncurry f)),
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
      ((κ : (a : α) → Measure β) a)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
have neg : ∀ (hf : ¬Measurable (Function.uncurry f)),
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : Measurable (Function.uncurry f)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
have pos : Measure.AbsolutelyContinuous (_m0 := mβ) (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a))
  ((κ : (a : α) → Measure β) a)
Tactic: rw [Kernel.withDensity_apply _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
hf : ¬Measurable (Function.uncurry f)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ.withDensity f : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
have neg : Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) (((0 : Kernel α β) : (a : α) → Measure β) a)
  ((κ : (a : α) → Measure β) a)
Tactic: rw [withDensity_of_not_measurable _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
⊢ κ.withDensity 1 = κ
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ.withDensity 1 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity 1 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((Measure.withDensity ((κ : (a : α) → Measure β) a) (1 a) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.withDensity_apply _ measurable_const]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
⊢ κ.withDensity 0 = 0
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ.withDensity 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((Measure.withDensity ((κ : (a : α) → Measure β) a) (0 a) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.withDensity_apply _ measurable_const]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : β), g b ∂(κ.withDensity f : (a : α) → Measure β) a = ∫⁻ (b : β), f a b * g b ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (a_1 : β), (f a * g) a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f a b * g b ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.withDensity_apply _ hf,
    lintegral_withDensity_eq_lintegral_mul _ (Measurable.of_uncurry_left hf) hg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
inst_2 : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.withDensity fun (a : α) (b : β) ↦ (↑(g a b) : ℝ≥0∞) : (a : α) → Measure β) a)
      fun (b : β) ↦ f b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b • f b)
have f_meas : Measurable (g a)
Tactic: rw [Kernel.withDensity_apply, integral_withDensity_eq_integral_smul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
inst_2 : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
f_meas : Measurable (g a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.withDensity fun (a : α) (b : β) ↦ (↑(g a b) : ℝ≥0∞) : (a : α) → Measure β) a)
      fun (b : β) ↦ f b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b • f b)
have hf : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (b : β) ↦ (↑(g a b) : ℝ≥0∞))
Tactic: rw [Kernel.withDensity_apply, integral_withDensity_eq_integral_smul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f
have pos : ∀ (hf : Measurable (Function.uncurry f)), (κ + η).withDensity f = κ.withDensity f + η.withDensity f
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
pos : ∀ (hf : Measurable (Function.uncurry f)), (κ + η).withDensity f = κ.withDensity f + η.withDensity f
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f
have neg : ∀ (hf : ¬Measurable (Function.uncurry f)), (κ + η).withDensity f = κ.withDensity f + η.withDensity f
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f
have pos : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((((κ + η).withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.withDensity f + η.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f
have neg : 0 = HAdd.hAdd (α := Kernel α β) 0 0
Tactic: simp_rw [withDensity_of_not_measurable _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = HAdd.hAdd (α := Kernel α β) 0 0
have neg : Eq (α := Kernel α β) 0 0
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
have pos : ∀ (hf : Measurable (Function.uncurry f)), (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
pos :
  ∀ (hf : Measurable (Function.uncurry f)), (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
have neg : ∀ (hf : ¬Measurable (Function.uncurry f)), (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
Tactic: by_cases hf : Measurable (Function.uncurry f)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
have pos : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (i : ι) ↦ (κ i).withDensity f : (a : α) → Measure β) a : Measure β)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (i : ι) ↦ (κ i).withDensity f : (a : α) → Measure β) a : Measure β)
have pos : Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
  (Measure.sum fun (n : ι) ↦ ((κ n).withDensity f : (a : α) → Measure β) a : Measure β)
Tactic: simp_rw [sum_apply, Kernel.withDensity_apply _ hf, sum_apply,
      withDensity_sum (fun n => κ n a) (f a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
pos :
  Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ι) ↦ ((κ n).withDensity f : (a : α) → Measure β) a : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (i : ι) ↦ (κ i).withDensity f : (a : α) → Measure β) a : Measure β)
have pos₁ : Eq (α := Measure β) (Measure.withDensity ((Kernel.sum κ : (a : α) → Measure β) a) (f a))
  (Measure.sum fun (n : ι) ↦ Measure.withDensity ((κ n : (a : α) → Measure β) a) (f a))
Tactic: simp_rw [sum_apply, Kernel.withDensity_apply _ hf, sum_apply,
      withDensity_sum (fun n => κ n a) (f a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
pos :
  Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ι) ↦ ((κ n).withDensity f : (a : α) → Measure β) a : Measure β)
pos₁ :
  Eq (α := Measure β) (Measure.withDensity ((Kernel.sum κ : (a : α) → Measure β) a) (f a))
    (Measure.sum fun (n : ι) ↦ Measure.withDensity ((κ n : (a : α) → Measure β) a) (f a))
⊢ Eq.{u_2 + 1} (α := Measure β) (((Kernel.sum κ).withDensity f : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (i : ι) ↦ (κ i).withDensity f : (a : α) → Measure β) a : Measure β)
have pos₂ : Eq (α := Measure β) (Measure.withDensity (Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) (f a))
  (Measure.sum fun (n : ι) ↦ Measure.withDensity ((κ n : (a : α) → Measure β) a) (f a))
Tactic: simp_rw [sum_apply, Kernel.withDensity_apply _ hf, sum_apply,
      withDensity_sum (fun n => κ n a) (f a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
hκ : ∀ (i : ι), IsSFiniteKernel (κ i)
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ (Kernel.sum κ).withDensity f = Kernel.sum fun (i : ι) ↦ (κ i).withDensity f
have neg : Eq (α := Kernel α β) 0 (Kernel.sum fun (i : ι) ↦ 0)
Tactic: simp_rw [withDensity_of_not_measurable _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
⊢ κ.withDensity (f + g) = κ.withDensity f + κ.withDensity g
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ.withDensity (f + g) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.withDensity f + κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity (f + g) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity f + κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Measurable (g a)
Tactic: rw [coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg,
    Kernel.withDensity_apply, Pi.add_apply, MeasureTheory.withDensity_add_right]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s : Set β
h_1 : MeasurableSet s
h : Measurable (g a)
⊢ Eq (α := ℝ≥0∞) ((((κ.withDensity (f + g) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.withDensity f + κ.withDensity g : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Measurable (Function.uncurry (f + g))
Tactic: rw [coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg,
    Kernel.withDensity_apply, Pi.add_apply, MeasureTheory.withDensity_add_right]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
⊢ (κ.withDensity fun (a : α) (x : β) ↦ f a x - g a x) + κ.withDensity g = κ.withDensity f
have rw : κ.withDensity ((fun (a : α) (x : β) ↦ f a x - g a x) + g) = κ.withDensity f
Tactic: rw [← withDensity_add_right _ hg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
rw : κ.withDensity ((fun (a : α) (x : β) ↦ f a x - g a x) + g) = κ.withDensity f
⊢ (κ.withDensity fun (a : α) (x : β) ↦ f a x - g a x) + κ.withDensity g = κ.withDensity f
have rw₁ : Measurable (α := α × β) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : β) ↦ f a x - g a x)
Tactic: rw [← withDensity_add_right _ hg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
⊢ κ.withDensity ((fun (a : α) (x : β) ↦ f a x - g a x) + g) = κ.withDensity f
have refine : ∀ (a : α),
  HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g
      a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)]
    f a
Tactic: refine withDensity_congr_ae κ ((hf.sub hg).add hg) hf (fun a ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
a : α
⊢ HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g
      a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)]
    f a
have h : ∀ (x : β) (hx : g a x ≤ f a x), HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g a x = f a x
Tactic: filter_upwards [hfg a] with x hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
a : α
x : β
hx : g a x ≤ f a x
⊢ HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g a x = f a x
have h : HAdd.hAdd (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ f a x - g a x) (g a) x = f a x
Tactic: rwa [Pi.add_apply, Pi.add_apply, tsub_add_cancel_iff_le]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] f a
a : α
x : β
hx : g a x ≤ f a x
h : HAdd.hAdd (α := (x : β) → ℝ≥0∞) (fun (x : β) ↦ f a x - g a x) (g a) x = f a x
⊢ HAdd.hAdd (α := α → β → ℝ≥0∞) (fun (a : α) (x : β) ↦ f a x - g a x) g a x = f a x
have h₁ : f a x - g a x + g a x = f a x
Tactic: rwa [Pi.add_apply, Pi.add_apply, tsub_add_cancel_iff_le]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun (n : ι) ↦ κ.withDensity (f n)
have h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
Tactic: have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun (n : ι) ↦ κ.withDensity (f n)
have h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
Tactic: have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable.{u_2, u_3} (α := β → ℝ≥0∞) fun (n : ι) ↦ f n a
h_sum : Summable (α := α → β → ℝ≥0∞) fun (n : ι) ↦ f n
⊢ κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun (n : ι) ↦ κ.withDensity (f n)
have h : ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((κ.withDensity (∑' (n : ι), f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (n : ι) ↦ κ.withDensity (f n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
Tactic: ext a s hs