awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Category.Stoch
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 κ
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 := ⋯ } ⋯ ≫ Δ))
    (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)) } ⋯)))
⊢ 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)) } ⋯))

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.Stoch
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 κ
h :
  Eq.{u_1 + 1} (α :=
    X.obj (_P := StochHom) ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := SFinKer.instLargeCategory) (Y.obj (_P := StochHom))
        (Y.obj (_P := StochHom)))
    ({ hom := κ, property := ⋯ : 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 := ⋯ } { hom := Kernel.id ∥ₖ κ, property := ⋯ }))
⊢ 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)) } ⋯)))

Tactic:
dsimp
-- Module: Mathlib.Probability.Kernel.Category.Stoch
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 (𝒞 := SFinKer.instLargeCategory) (Y.obj (_P := StochHom))
        (Y.obj (_P := StochHom)))
    ({ hom := κ, property := ⋯ : 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 := ⋯ } { hom := Kernel.id ∥ₖ κ, property := ⋯ }))

Tactic:
exact Deterministic.copy_natural _

Premises used: CategoryTheory.Deterministic.copy_natural
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ : X ⟶ Y
⊢ IsMarkovKernel κ.hom (P := StochHom).hom

Tactic:
κ.2

Premises used: CategoryTheory.InducedWideCategory.Hom.property
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
⊢ κ.hom (P := StochHom) ≫ Δ = Δ ≫ (κ.hom (P := StochHom) ⊗ₘ κ.hom (P := StochHom))

Tactic:
have := Deterministic.copy_natural κ.hom
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
this : κ.hom (P := StochHom) ≫ Δ = Δ ≫ (κ.hom (P := StochHom) ⊗ₘ κ.hom (P := StochHom))
⊢ SFinKer.Hom.hom (κ.hom (P := StochHom) ≫ Δ) = SFinKer.Hom.hom (Δ ≫ (κ.hom (P := StochHom) ⊗ₘ κ.hom (P := StochHom)))

Tactic:
rw [SFinKer.Hom.ext_iff] at this

Premises used: SFinKer.Hom.ext_iff
-- Module: Mathlib.Probability.Kernel.Category.Stoch
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
⊢ 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

Premises used: ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
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
⊢ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ copy X.obj (_P := StochHom).carrier =
    copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ : X ⟶ Y
inst : Deterministic κ
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
⊢ κ.hom (P := StochHom).hom ∥ₖ κ.hom (P := StochHom).hom ∘ₖ copy X.obj (_P := StochHom).carrier =
    copy Y.obj (_P := StochHom).carrier ∘ₖ κ.hom (P := StochHom).hom

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 : Stoch
κ : X_1 ⟶ Y_1
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
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 : Stoch
κ : X_1 ⟶ Y_1
⊢ 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:
simp
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h_1 : Deterministic (κ ≫ η)
h :
  SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y_1))) =
    SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (Δ ≫ (κ ≫ η ⊗ₘ κ)))
⊢ κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y_1) = Δ ≫ (κ ≫ η ⊗ₘ κ)

Tactic:
ext : 2
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h_1 : Deterministic (κ ≫ η)
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
⊢ SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (κ ≫ Δ ≫ (η ⊗ₘ 𝟙 Y_1))) =
    SFinKer.Hom.hom (InducedWideCategory.Hom.hom (P := StochHom) (Δ ≫ (κ ≫ η ⊗ₘ κ)))

Tactic:
dsimp
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h_1 : Deterministic (κ ≫ η)
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
⊢ 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:
simp only [id_parallelComp_id, id_comp, id_parallelComp_comp_parallelComp_id]

Premises used: ProbabilityTheory.Kernel.id_parallelComp_id, ProbabilityTheory.Kernel.id_parallelComp_comp_parallelComp_id, ProbabilityTheory.Kernel.id_comp
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
⊢ IsDeterministic (κ ≫ η).hom (P := StochHom).hom

Tactic:
have : IsDeterministic (κ ≫ η).hom.hom := inferInstance
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
this : IsDeterministic (κ ≫ η).hom (P := StochHom).hom
⊢ η.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:
(comp_parallelComp_comp_copy).symm

Premises used: setOf, ProbabilityTheory.Kernel.comp_parallelComp_comp_copy, Eq.symm
-- Module: Mathlib.Probability.Kernel.Category.Stoch
Goal:
X Y : Stoch
κ_1 : X ⟶ Y
X_1 Y_1 Z : Stoch
κ : X_1 ⟶ Y_1
η : Y_1 ⟶ Z
h : Deterministic (κ ≫ η)
this : IsDeterministic (κ ≫ η).hom (P := StochHom).hom
⊢ η.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:
exact (comp_parallelComp_comp_copy).symm

Premises used: ProbabilityTheory.Kernel.comp_parallelComp_comp_copy, Eq.symm
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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)
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∞)
⊢ μ ⊗ₘ κ.withDensity f = (μ ⊗ₘ κ).withDensity fun (p : α × β) ↦ f p.1 p.2

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 ∂μ
h₁ : Measurable (β := ℝ≥0∞) (s.indicator fun (a : α × β) ↦ f a.1 a.2)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ.withDensity f : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ ⊗ₘ κ).withDensity fun (p : α × β) ↦ f p.1 p.2 : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [compProd_apply hs, withDensity_apply _ hs, ← lintegral_indicator hs,
    lintegral_compProd]

Premises used: MeasureTheory.Measure.compProd_apply, MeasureTheory.lintegral_indicator, MeasureTheory.Measure.lintegral_compProd, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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) =
      ∫⁻ (b : β), s.indicator (fun (a : α × β) ↦ f a.1 a.2) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (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:
congr with a
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 : α
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
⊢ (((κ.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:
rw [Kernel.withDensity_apply' _ hf, ← lintegral_indicator (measurable_prodMk_left hs)]

Premises used: MeasureTheory.lintegral_indicator, ProbabilityTheory.Kernel.withDensity_apply', measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 : α
⊢ ∫⁻ (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:
rfl
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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
⊢ Measurable (β := ℝ≥0∞) (s.indicator fun (a : α × β) ↦ f a.1 a.2)

Tactic:
hf.indicator hs

Premises used: Measurable.indicator
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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
⊢ Measurable (β := ℝ≥0∞) (s.indicator fun (a : α × β) ↦ f a.1 a.2)

Tactic:
exact hf.indicator hs

Premises used: Measurable.indicator
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 : μ ⊗ₘ κ = μ ⊗ₘ η
⊢ ∀ᵐ (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
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 : α
ha : 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:
(Kernel.withDensity_rnDeriv_eq ha).symm

Premises used: ProbabilityTheory.Kernel.withDensity_rnDeriv_eq, Eq.symm
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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
h₂ h₃ :
  ∀ (a : α)
    (ha :
      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 β)
⊢ ∀ᵐ (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
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 β)

Tactic:
have hκ_eq : ∀ᵐ a ∂μ, κ a = η.withDensity (κ.rnDeriv η) a := by
    filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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_1 : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac_1 :
  ∀ᵐ (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
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
h : ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((η : (a : α) → Measure β) a : Measure β)

Tactic:
(rnDeriv_eq_one_iff_eq h_ac).mp h

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_one_iff_eq, Iff.mp
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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
h₂ h₃ :
  ∀ (a : α)
    (h_ac :
      Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
        ((η : (a : α) → Measure β) a))
    (h : ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1),
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((η : (a : α) → Measure β) a : Measure β)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (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
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
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 β)
suffices : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)

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