awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
⊢ False
have h_lt : ¬Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 c)
Tactic: have h_lt : ¬ (κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c) := not_le.mpr (lt_of_le_of_lt' hξ hc)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
h_lt :
  ¬Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
        (Icc 0 x) ≤
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
        (Icc 0 c)
⊢ False
have h₁ : Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
    (Icc 0 x) ≤
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
    (Icc 0 c)
Tactic: refine h_lt ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
h_lt :
  ¬Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
        (Icc 0 x) ≤
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
        (Icc 0 c)
⊢ Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 c)
have h₁ : autoParam
  (Ne (α := ℝ≥0∞)
    ((((κ : (a : X) → Measure (↑I : Type)) a : Measure (↑I : Type)) : (a : Set (↑I : Type)) → ℝ≥0∞) (Icc 0 c) : ℝ≥0∞)
    (∞ : ℝ≥0∞))
  measureReal_mono._auto_1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
have hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
Tactic: have hg := measurableEmbedding_sigmoid_comp_embeddingReal Y
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
have hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
Tactic: have hκg : IsMarkovKernel (κ.map g) := IsMarkovKernel.map κ hg.measurable
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
⊢ κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
have rw : κ = κ.map (hg.invFun ∘ sigmoid ∘ embeddingReal Y)
Tactic: rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
rw : κ = κ.map (hg.invFun ∘ sigmoid ∘ embeddingReal Y)
⊢ κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
have rw₁ : κ = κ.map id
Tactic: rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
rw : κ = κ.map (hg.invFun ∘ sigmoid ∘ embeddingReal Y)
rw₁ : κ = κ.map id
⊢ κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
have rw₂ : κ = κ
Tactic: rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
have hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
Tactic: have hg'κ : κ = (κ.map g).map hg.invFun := by
    rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
have obtain : ∀ (f' : X → (↑I : Type) → (↑I : Type)) (hf' : Measurable (uncurry f'))
  (hf'κ :
    ∀ (a : X),
      Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
        (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)),
  ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
Tactic: obtain ⟨f', hf', hf'κ⟩ := (κ.map g).exists_measurable_map_eq_unitInterval_aux
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
have refine : ∀ (a : X),
  Eq.{u_2 + 1} (α := Measure Y)
    (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
    ((κ : (a : X) → Measure Y) a)
Tactic: refine ⟨fun a u ↦ hg.invFun (f' a u), by fun_prop, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
a : X
⊢ Eq.{u_2 + 1} (α := Measure Y)
    (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
    ((κ : (a : X) → Measure Y) a)
have rw : Eq (α := Measure Y) (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
  (Measure.map (hg.invFun ∘ f' a) volume)
Tactic: rw [hg'κ, map_apply _ (by fun_prop), ← hf'κ, Measure.map_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
⊢ ∃ (f : (↑I : Type) → Y), Measurable f ∧ map f volume = μ
have obtain : ∀ (f : Unit → (↑I : Type) → Y) (hf_meas : Measurable (uncurry f))
  (hf_map : ∀ (a : Unit), Eq (α := Measure Y) (map (f a) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) a)),
  ∃ (f : (↑I : Type) → Y), Measurable f ∧ map f volume = μ
Tactic: obtain ⟨f, hf_meas, hf_map⟩ := Kernel.exists_measurable_map_eq_unitInterval (Kernel.const Unit μ)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
f : Unit → (↑I : Type) → Y
hf_meas : Measurable (uncurry f)
hf_map : ∀ (a : Unit), Eq (α := Measure Y) (map (f a) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) a)
⊢ ∃ (f : (↑I : Type) → Y), Measurable f ∧ map f volume = μ
have hf_map₁ : Eq (α := Measure Y) (map (f ()) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) ())
Tactic: specialize hf_map ()
Cleared hypotheses: hf_map
-- Lean 4 proof step from Mathlib.Probability.Kernel.SetIntegral (goal)
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
κ : Kernel X Y
μ : Measure X
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (x : X), @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ s.indicator (fun (x : X) ↦ f x y) x ∂μ)
    (∫ (x : X) in s, @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ f x y ∂μ)
have simp_rw : Eq.{u_3 + 1} (α := E)
  (∫ (x : X), @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ s.indicator (fun (x : X) ↦ f x y) x ∂μ)
  (∫ (x : X), s.indicator (fun (x : X) ↦ @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ f x y) x ∂μ)
Tactic: simp_rw [← integral_indicator hs, Kernel.integral_indicator₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a)
have refine : ∀ (s : Set β) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.withDensity ((κ : (a : α) → Measure β) b) (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: refine Measure.measurable_of_measurable_coe _ fun s hs => ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.WithDensity (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.withDensity ((κ : (a : α) → Measure β) b) (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∫⁻ (a : β) in s, f b a ∂(κ : (a : α) → Measure β) b
Tactic: simp_rw [withDensity_apply _ hs]
-- 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 : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
have rw : Eq.{u_2 + 1} (α := Measure β)
  (({ toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := sorry : Kernel α β } :
        (a : α) → Measure β)
      a :
    Measure β)
  (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
Tactic: rw [withDensity, dif_pos hf]
-- 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 : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
have rw : Eq.{u_2 + 1} (α := Measure β)
  (((if hf : Measurable (Function.uncurry f) then
            { toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := sorry }
          else 0 :
          Kernel α β) :
        (a : α) → Measure β)
      a :
    Measure β)
  (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
Tactic: classical
  rw [withDensity, dif_pos hf]
  rfl
-- 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 : α
rw :
  Eq.{u_2 + 1} (α := Measure β)
    (((if hf : Measurable (Function.uncurry f) then
              { toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := ⋯ }
            else 0 :
            Kernel α β) :
          (a : α) → Measure β)
        a :
      Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.withDensity f : (a : α) → Measure β) a : Measure β)
    (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
have rw₁ : Eq.{u_2 + 1} (α := Measure β)
  (({ toFun := fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a), measurable' := sorry : Kernel α β } :
        (a : α) → Measure β)
      a :
    Measure β)
  (Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β)
Tactic: classical
  rw [withDensity, dif_pos hf]
  rfl
-- 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 : α
s : Set β
⊢ (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
have rw : ((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s =
  ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.withDensity_apply κ hf, withDensity_apply' _ s]
-- 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 : α
s : Set β
rw :
  ((Measure.withDensity ((κ : (a : α) → Measure β) a) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
⊢ (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (a_1 : β) in s, f a a_1 ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f a b ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.withDensity_apply κ hf, withDensity_apply' _ 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 κ
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
⊢ κ.withDensity f = κ.withDensity g
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.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)
hfg : ∀ (a : α), f a =ᶠ[ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)] g a
a : α
s : Set β
h : MeasurableSet s
⊢ 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) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ.withDensity g : (a : α) → Measure β) 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 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∞)
⊢ 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) (f 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)]