awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X Y : Stoch
κ : X ⟶ Y
⊢ Eq.{u_1 + 1} (α :=
    X ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom)
        ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom)) ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom)))
    (ε ≫ Δ) (Δ ≫ (ε ⊗ₘ ε))
have h : Eq.{u_1 + 1} (α :=
  X.obj (_P := StochHom) ⟶
    (MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom)
          ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom))
          ((𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom))).obj
      (_P := StochHom))
  (InducedWideCategory.Hom.hom (P := StochHom) (ε ≫ Δ)) (InducedWideCategory.Hom.hom (P := StochHom) (Δ ≫ (ε ⊗ₘ ε)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X_1 Y_1 : Stoch
κ_1 : X_1 ⟶ Y_1
X Y : Stoch
κ : Kernel X.obj (_P := StochHom).carrier Y.obj (_P := StochHom).carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Eq.{u_1 + 1} (α := X ⟶ MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom) Y Y)
    (InducedWideCategory.Hom.mk (P := StochHom) { hom := κ, property := ⋯ } ⋯ ≫ Δ)
    (Δ ≫
      (InducedWideCategory.Hom.mk (P := StochHom)
          { hom := κ, property := ⋯ : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } ⋯ ⊗ₘ
        InducedWideCategory.Hom.mk (P := StochHom)
          { hom := κ, property := ⋯ : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } ⋯))
have h : Eq.{u_1 + 1} (α :=
  X.obj (_P := StochHom) ⟶
    (MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom) Y Y).obj (_P := StochHom))
  (InducedWideCategory.Hom.hom (P := StochHom)
    (InducedWideCategory.Hom.mk (P := StochHom) { hom := κ, property := sorry } sorry ≫ Δ))
  (InducedWideCategory.Hom.hom (P := StochHom)
    (Δ ≫
      (InducedWideCategory.Hom.mk (P := StochHom)
          { hom := κ, property := sorry : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } sorry ⊗ₘ
        InducedWideCategory.Hom.mk (P := StochHom)
          { hom := κ, property := sorry : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } sorry)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X_1 Y_1 : Stoch
κ_1 : X_1 ⟶ Y_1
X Y : Stoch
κ : Kernel X.obj (_P := StochHom).carrier Y.obj (_P := StochHom).carrier
inst : IsDeterministic κ
inst_1 : IsMarkovKernel κ
⊢ Eq.{u_1 + 1} (α :=
    X.obj (_P := StochHom) ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := WideSubcategory.category StochHom) Y Y).obj (_P := StochHom))
    (InducedWideCategory.Hom.hom (P := StochHom)
      (InducedWideCategory.Hom.mk (P := StochHom) { hom := κ, property := ⋯ } ⋯ ≫ Δ))
    (InducedWideCategory.Hom.hom (P := StochHom)
      (Δ ≫
        (InducedWideCategory.Hom.mk (P := StochHom)
            { hom := κ, property := ⋯ : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } ⋯ ⊗ₘ
          InducedWideCategory.Hom.mk (P := StochHom)
            { hom := κ, property := ⋯ : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } ⋯)))
have h : Eq.{u_1 + 1} (α :=
  X.obj (_P := StochHom) ⟶
    MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) (Y.obj (_P := StochHom)) (Y.obj (_P := StochHom)))
  ({ hom := κ, property := sorry : X.obj (_P := StochHom).Hom (Y.obj (_P := StochHom)) } ≫ Δ)
  (CategoryStruct.comp (Y :=
    MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) (X.obj (_P := StochHom)) (X.obj (_P := StochHom)))
    Δ
    (CategoryStruct.comp (Y :=
      { carrier := Y.obj (_P := StochHom).carrier × X.obj (_P := StochHom).carrier, str := Prod.instMeasurableSpace })
      { hom := κ ∥ₖ Kernel.id, property := sorry } { hom := Kernel.id ∥ₖ κ, property := sorry }))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (hypothesis)
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
⊢ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ copy X.obj (_P := StochHom).carrier =
    copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom
have this : κ.hom (P := StochHom) ≫ Δ = Δ ≫ (κ.hom (P := StochHom) ⊗ₘ κ.hom (P := StochHom))
Tactic: have := Deterministic.copy_natural κ.hom
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (hypothesis)
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
this : κ.hom (P := StochHom) ≫ Δ = Δ ≫ (κ.hom (P := StochHom) ⊗ₘ κ.hom (P := StochHom))
⊢ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ copy X.obj (_P := StochHom).carrier =
    copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom
have this₁ : SFinKer.Hom.hom (κ.hom (P := StochHom) ≫ Δ) = SFinKer.Hom.hom (Δ ≫ (κ.hom (P := StochHom) ⊗ₘ κ.hom (P := StochHom)))
Tactic: rw [SFinKer.Hom.ext_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (hypothesis)
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
this :
  copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom =
    Kernel.id ∥ₖ κ.hom (P := StochHom).hom ∘ₖ (κ.hom (P := StochHom).hom ∥ₖ Kernel.id) ∘ₖ
      copy X.obj (_P := StochHom).carrier
⊢ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ copy X.obj (_P := StochHom).carrier =
    copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom
have this₁ : copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom =
  κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ copy X.obj (_P := StochHom).carrier
Tactic: rw [id_parallelComp_comp_parallelComp_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 : Stoch
κ : X_1 ⟶ Y_1
⊢ κ ≫ ε = ε
have h : Eq (α :=
  Kernel X_1.obj (_P := StochHom).carrier
    (𝟙_ Stoch) (𝒞 := WideSubcategory.category StochHom).obj (_P := StochHom).carrier)
  (SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (κ ≫ ε)))
  (SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) ε))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
⊢ κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y_1) = Δ ≫ (κ ≫ η ⊗ₘ κ)
have h : SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y_1))) =
  SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (Δ ≫ (κ ≫ η ⊗ₘ κ)))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
⊢ SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y_1))) =
    SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (Δ ≫ (κ ≫ η ⊗ₘ κ)))
have h : Kernel.id ∥ₖ Kernel.id ∘ₖ (η.hom (P := StochHom).hom ∥ₖ Kernel.id) ∘ₖ copy Y_1.obj (_P := StochHom).carrier ∘ₖ
    κ.hom (P := StochHom).hom =
  Kernel.id ∥ₖ κ.hom (P := StochHom).hom ∘ₖ (η.hom (P := StochHom).hom ∘ₖ κ.hom (P := StochHom).hom ∥ₖ Kernel.id) ∘ₖ
    copy X_1.obj (_P := StochHom).carrier
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (goal)
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
⊢ Kernel.id ∥ₖ Kernel.id ∘ₖ (η.hom (P := StochHom).hom ∥ₖ Kernel.id) ∘ₖ copy Y_1.obj (_P := StochHom).carrier ∘ₖ
      κ.hom (P := StochHom).hom =
    Kernel.id ∥ₖ κ.hom (P := StochHom).hom ∘ₖ (η.hom (P := StochHom).hom ∘ₖ κ.hom (P := StochHom).hom ∥ₖ Kernel.id) ∘ₖ
      copy X_1.obj (_P := StochHom).carrier
have h : η.hom (P := StochHom).hom ∥ₖ Kernel.id ∘ₖ copy Y_1.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom =
  η.hom (P := StochHom).hom ∘ₖ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ
    copy X_1.obj (_P := StochHom).carrier
Tactic: simp only [id_parallelComp_id, id_comp, id_parallelComp_comp_parallelComp_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.Stoch (hypothesis)
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
⊢ η.hom (P := StochHom).hom ∥ₖ Kernel.id ∘ₖ copy Y_1.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom =
    η.hom (P := StochHom).hom ∘ₖ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ
      copy X_1.obj (_P := StochHom).carrier
have this : IsDeterministic (κ ≫ η).hom (P := StochHom).hom
Tactic: have : IsDeterministic (κ ≫ η).hom.hom := inferInstance
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
⊢ μ ⊗ₘ κ.withDensity f = (μ ⊗ₘ κ).withDensity fun (p : α × β) ↦ f p.1 p.2
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ.withDensity f : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ ⊗ₘ κ).withDensity fun (p : α × β) ↦ f p.1 p.2 : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ.withDensity f : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ ⊗ₘ κ).withDensity fun (p : α × β) ↦ f p.1 p.2 : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α), (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
  ∫⁻ (a : α), ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
Tactic: rw [compProd_apply hs, withDensity_apply _ hs, ← lintegral_indicator hs,
    lintegral_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
h :
  ∫⁻ (a : α), (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ.withDensity f : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ ⊗ₘ κ).withDensity fun (p : α × β) ↦ f p.1 p.2 : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Measurable (β := ℝ≥0∞) (s.indicator fun (a : α × β) ↦ f a.1 a.2)
Tactic: rw [compProd_apply hs, withDensity_apply _ hs, ← lintegral_indicator hs,
    lintegral_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
have h : ∀ (a : α),
  (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) =
    ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
f : α → β → ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
s : Set (α × β)
hs : MeasurableSet s
a : α
⊢ (((κ.withDensity f : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) =
    ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a
have h : ∫⁻ (a_1 : β), (Prod.mk a ⁻¹' s).indicator (f a) a_1 ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.withDensity_apply' _ hf, ← lintegral_indicator (measurable_prodMk_left hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
have h_ac : ∀ᵐ (a : α) ∂μ,
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
Tactic: have h_ac : ∀ᵐ a ∂μ, κ a ≪ η a := (Measure.absolutelyContinuous_of_eq h).kernel_of_compProd
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (a : α) ↦
                Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                  ((η : (a : α) → Measure β) a))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (a : α) ↦
                Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
                  ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β))
              x}
          x}
    a
Tactic: filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                    ((η : (a : α) → Measure β) a))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
                    ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β))
                x}
            x}
      a
⊢ ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
have h₂ : ∀ (a : α),
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a) →
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
Tactic: filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
have hκ_eq : ∀ᵐ (a : α) ∂μ,
  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
Tactic: have hκ_eq : ∀ᵐ a ∂μ, κ a = η.withDensity (κ.rnDeriv η) a := by
    filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
this : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (a : α) ↦
                Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                  ((η : (a : α) → Measure β) a))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α)
                {x : α | (fun (a : α) ↦ ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1) x}
                x →
              Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦
                      Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
                        ((η : (a : α) → Measure β) x : Measure β))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [h_ac, this] with a h_ac h using (rnDeriv_eq_one_iff_eq h_ac).mp h
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
this : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                    ((η : (a : α) → Measure β) a))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α | (fun (a : α) ↦ ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1) x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) x : Measure β)
                          ((η : (a : α) → Measure β) x : Measure β))
                      x}
                  x}
            x}
      a
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
have h₂ : ∀ (a : α),
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a) →
    (∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1) →
      Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((η : (a : α) → Measure β) a : Measure β)
Tactic: filter_upwards [h_ac, this] with a h_ac h using (rnDeriv_eq_one_iff_eq h_ac).mp h
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
have suffices : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1
Tactic: suffices ∀ᵐ a ∂μ, ∀ᵐ b ∂(η a), κ.rnDeriv η a b = 1 by
    filter_upwards [h_ac, this] with a h_ac h using (rnDeriv_eq_one_iff_eq h_ac).mp h
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1
have refine : ∀ᵐ (x : α × β) ∂μ ⊗ₘ η, (fun (x : α × β) ↦ κ.rnDeriv η x.1 x.2 = 1) x
Tactic: refine Measure.ae_ae_of_ae_compProd (p := fun x ↦ κ.rnDeriv η x.1 x.2 = 1) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.CompProdEqIff (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
⊢ ∀ᵐ (x : α × β) ∂μ ⊗ₘ η, (fun (x : α × β) ↦ κ.rnDeriv η x.1 x.2 = 1) x
have refine : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = ∫⁻ (x : α × β) in s, 1 ∂μ ⊗ₘ η
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (by fun_prop) fun s hs _ ↦ ?_