awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this :
  (ρ : (a : α) → Measure (β × Ω)) a =
    Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯
h :
  ∀ᵐ (x : β) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) x : Measure Ω)
      ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) x : Measure Ω)
b : β
hb :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) b : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)
h₁ :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) b : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)
have h₂ : Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
  ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
Tactic: rw [← hb, Kernel.comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst_4 : IsFiniteMeasure ρ
a : α
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae ρ.fst)
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
have h : EventuallyEq.{u_2, u_3} (β := Measure Ω)
  (ae (F := Measure β) (((Kernel.fst (Kernel.const α ρ) : Kernel α β) : (a : α) → Measure β) a : Measure β))
  (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
  (⇑(Measure.condKernel ((Kernel.const α ρ : (a : α) → Measure (β × Ω)) a)) : (a : β) → Measure Ω)
Tactic: have h := Kernel.condKernel_apply_eq_condKernel (Kernel.const α ρ) a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst_4 : IsFiniteMeasure ρ
a : α
h :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map Prod.fst ρ))
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae ρ.fst)
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
have h₁ : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq.{u_3 + 1} (α := Measure Ω)
                  ((fun (b : β) ↦ ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω))
                      x :
                    Measure Ω)
                  ((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq.{u_3 + 1} (α := Measure Ω)
                  ((fun (b : β) ↦ ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω))
                      x :
                    Measure Ω)
                  ((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω))
              x}
          x}
    a_1
Tactic: filter_upwards [h] with b hb using hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst_4 : IsFiniteMeasure ρ
a : α
h :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map Prod.fst ρ))
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_3 + 1} (α := Measure Ω)
                    ((fun (b : β) ↦
                          ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω))
                        x :
                      Measure Ω)
                    ((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_3 + 1} (α := Measure Ω)
                    ((fun (b : β) ↦
                          ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω))
                        x :
                      Measure Ω)
                    ((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω))
                x}
            x}
      a_1
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae ρ.fst)
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
have h₂ : ∀ (a_1 : β),
  Eq.{u_3 + 1} (α := Measure Ω) ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
      ((ρ.condKernel : (a : β) → Measure Ω) a_1 : Measure Ω) →
    Eq.{u_3 + 1} (α := Measure Ω)
      ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
      ((ρ.condKernel : (a : β) → Measure Ω) a_1 : Measure Ω)
Tactic: filter_upwards [h] with b hb using hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_5 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ ∀ᵐ (x : β) ∂((ρ.fst : (a : α) → Measure β) a : Measure β),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, x) : Measure Ω)
      ((ρ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω)
have h : ∀ (a_1 : β)
  (h1 :
    Eq.{u_3 + 1} (α := Measure Ω) ((ρ.condKernel : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
      ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) a_1 : Measure Ω))
  (h2 :
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
      ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) a_1 : Measure Ω)),
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
    ((ρ.condKernel : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
Tactic: filter_upwards [Kernel.condKernel_apply_eq_condKernel ρ a,
    Kernel.apply_eq_measure_condKernel_of_compProd_eq hκ a] with a h1 h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_5 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a_1 : α
a : β
h1 :
  Eq.{u_3 + 1} (α := Measure Ω) ((ρ.condKernel : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
h2 h :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
    ((ρ.condKernel : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
have h₁ : Eq.{u_3 + 1} (α := Measure Ω)
  ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
  ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
Tactic: rw [h1, h2]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s) μ
have refine : ∀ (x : α), ‖Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s‖ ≤ κ.bound.toReal
Tactic: refine Integrable.mono' (integrable_const κ.bound.toReal)
    ((κ.measurable_coe hs).ennreal_toReal.aestronglyMeasurable)
    (ae_of_all μ fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : IsFiniteMeasure μ
κ : Kernel α β
inst_1 : IsFiniteKernel κ
s : Set β
hs : MeasurableSet s
x : α
⊢ ‖Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s‖ ≤ κ.bound.toReal
have rw : Measure.real (m := mβ) ((κ : (a : α) → Measure β) x) s ≤ κ.bound.toReal
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
⊢ Eq.{u_3 + 1} (α := E) (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b ∂μ)
    (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b ∂μ)
have h₁ : Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ)
  (fun (a : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b) fun (a : α) ↦
  @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
⊢ Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ)
    (fun (a : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b) fun (a : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b
have h₁ : ∀ (a : α) (ha : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a),
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f a b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g a b)
Tactic: filter_upwards [h] with _ ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
ha : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
⊢ f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
have h₁ : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x →
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x}
    a_1
Tactic: filter_upwards [ha] with _ hb using hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
ha : f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x}
      a_1
⊢ f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
have h₂ : ∀ (a_1 : β), f a a_1 = g a a_1 → f a a_1 = g a a_1
Tactic: filter_upwards [ha] with _ hb using hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
have pos : ∀ (ha : a ∈ s),
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
pos :
  ∀ (ha : a ∈ s),
    Eq.{u_3 + 1} (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
      (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
have neg : ∀ (ha : a ∉ s),
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (y : β) ↦ s.indicator (fun (x : α) ↦ f x y) a)
    (s.indicator (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y) a)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
⊢ (@integral _ _ _ _ mβ ((deterministic g hg : (a : α) → Measure β) a) fun (x : β) ↦ f x) = f (g a)
have rw : (@integral _ _ _ _ mβ (Measure.dirac (g a)) fun (x : β) ↦ f x) = f (g a)
Tactic: rw [deterministic_apply, integral_dirac' _ _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
rw : (@integral _ _ _ _ mβ (Measure.dirac (g a)) fun (x : β) ↦ f x) = f (g a)
⊢ (@integral _ _ _ _ mβ ((deterministic g hg : (a : α) → Measure β) a) fun (x : β) ↦ f x) = f (g a)
have rw₁ : f (g a) = f (g a)
Tactic: rw [deterministic_apply, integral_dirac' _ _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
inst_3 : MeasurableSingletonClass β
hg : Measurable g
⊢ (@integral _ _ _ _ mβ ((deterministic g hg : (a : α) → Measure β) a) fun (x : β) ↦ f x) = f (g a)
have rw : (@integral _ _ _ _ mβ (Measure.dirac (g a)) fun (x : β) ↦ f x) = f (g a)
Tactic: rw [deterministic_apply, integral_dirac _ (g a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
inst_3 : MeasurableSingletonClass β
hg : Measurable g
rw : (@integral _ _ _ _ mβ (Measure.dirac (g a)) fun (x : β) ↦ f x) = f (g a)
⊢ (@integral _ _ _ _ mβ ((deterministic g hg : (a : α) → Measure β) a) fun (x : β) ↦ f x) = f (g a)
have rw₁ : f (g a) = f (g a)
Tactic: rw [deterministic_apply, integral_dirac _ (g a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
s : Set β
hs : MeasurableSet s
inst_3 : Decidable (g a ∈ s)
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((deterministic g hg : (a : α) → Measure β) a) s) fun (x : β) ↦ f x) =
    if g a ∈ s then f (g a) else 0
have rw : (@integral _ _ _ _ mβ (Measure.restrict (Measure.dirac (g a)) s) fun (x : β) ↦ f x) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setIntegral_dirac' hf _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
s : Set β
hs : MeasurableSet s
inst_3 : Decidable (g a ∈ s)
rw :
  (@integral _ _ _ _ mβ (Measure.restrict (Measure.dirac (g a)) s) fun (x : β) ↦ f x) = if g a ∈ s then f (g a) else 0
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((deterministic g hg : (a : α) → Measure β) a) s) fun (x : β) ↦ f x) =
    if g a ∈ s then f (g a) else 0
have rw₁ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setIntegral_dirac' hf _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
inst_3 : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst_4 : Decidable (g a ∈ s)
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((deterministic g hg : (a : α) → Measure β) a) s) fun (x : β) ↦ f x) =
    if g a ∈ s then f (g a) else 0
have rw : (@integral _ _ _ _ mβ (Measure.restrict (Measure.dirac (g a)) s) fun (x : β) ↦ f x) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setIntegral_dirac f _ s]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
inst_2 : CompleteSpace E
g : α → β
inst_3 : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst_4 : Decidable (g a ∈ s)
rw :
  (@integral _ _ _ _ mβ (Measure.restrict (Measure.dirac (g a)) s) fun (x : β) ↦ f x) = if g a ∈ s then f (g a) else 0
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((deterministic g hg : (a : α) → Measure β) a) s) fun (x : β) ↦ f x) =
    if g a ∈ s then f (g a) else 0
have rw₁ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
Tactic: rw [deterministic_apply, setIntegral_dirac f _ s]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (((const α μ : Kernel α β) : (a : α) → Measure β) a) fun (x : β) ↦ f x)
    (∫ (x : β), f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : β), f x ∂μ) (∫ (x : β), f x ∂μ)
Tactic: rw [const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
s : Set β
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict (((const α μ : Kernel α β) : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
    (∫ (x : β) in s, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) (∫ (x : β) in s, f x ∂μ)
Tactic: rw [const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ.restrict (s := s) hs : (a : α) → Measure β) a) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
have rw : Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦ f x)
Tactic: rw [restrict_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.restrict (s := s) hs : (a : α) → Measure β) a) t) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
have rw : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ mβ (Measure.restrict (Measure.restrict ((κ : (a : α) → Measure β) a) s) t) fun (x : β) ↦ f x)
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
Tactic: rw [restrict_apply, Measure.restrict_restrict' hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
rw :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.restrict ((κ : (a : α) → Measure β) a) s) t) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ.restrict (s := s) hs : (a : α) → Measure β) a) t) fun (x : β) ↦ f x)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
have rw₁ : Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) (t ∩ s)) fun (x : β) ↦ f x)
Tactic: rw [restrict_apply, Measure.restrict_restrict' hs]