awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : β), IsMarkovKernel (κ.sectL b)
x : α × β
rw :
  Eq (α := ℝ≥0∞) ((((κ.sectL x.2 : (a : α) → Measure γ) x.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← sectL_apply, measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, ProbabilityTheory.Kernel.sectL_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
h :
  ∀ (d : δ) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((((κ.sectL b).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (κ.sectL b).comap f hf = κ.comap (fun (d : δ) ↦ (f d, b)) ⋯

Tactic:
ext d s
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ.sectL b : (a : α) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.sectL b).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply, sectL_apply, comap_apply]

Premises used: ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.sectL_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
β : Type u_2
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
α : Type u_6
inst : MeasurableSpace α
κ : Kernel β γ
a : α
b : β
⊢ Eq.{u_4 + 1} (α := Measure γ) (((sectL (prodMkLeft α κ) b : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : β) → Measure γ) b : Measure γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
mα : MeasurableSpace α
γ : Type u_4
mγ : MeasurableSpace γ
β : Type u_6
inst : MeasurableSpace β
κ : Kernel α γ
b : β
⊢ sectL (mβ := inst) (prodMkRight β κ) b = κ

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.sectL, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
b : β
a : α
⊢ Eq.{u_4 + 1} (α := Measure γ) ((κ.sectR a : (a : β) → Measure γ) b : Measure γ)
    ((κ : (a : α × β) → Measure γ) (a, b) : Measure γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
a : α
⊢ Eq (α := Kernel β γ) (sectR (mα := mα) 0 a) 0

Tactic:
simp [sectR]

Premises used: ProbabilityTheory.Kernel.sectR
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap (fun (b : β) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap (fun (b : β) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap (fun (b : β) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
inst : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap (fun (b : β) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst rw : NeZero.{u_4} (R := Measure γ) ((κ : (a : α × β) → Measure γ) (a, b) : Measure γ)
⊢ NeZero.{u_4} (R := Measure γ) ((κ.sectR a : (a : β) → Measure γ) b : Measure γ)

Tactic:
rw [sectR_apply]

Premises used: ProbabilityTheory.Kernel.sectR_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : α), IsMarkovKernel (κ.sectR b)
⊢ IsMarkovKernel κ

Tactic:
⟨fun _ ↦ ⟨?_⟩⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : α), IsMarkovKernel (κ.sectR b)
refine :
  ∀ (x : α × β),
    Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsMarkovKernel κ

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : α), IsMarkovKernel (κ.sectR b)
x : α × β
rw :
  Eq (α := ℝ≥0∞) ((((κ.sectR x.1 : (a : β) → Measure γ) x.2 : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← sectR_apply, measure_univ]

Premises used: ProbabilityTheory.Kernel.sectR_apply, MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
h :
  ∀ (d : δ) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((((κ.sectR a).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (κ.sectR a).comap f hf = κ.comap (fun (d : δ) ↦ (a, f d)) ⋯

Tactic:
ext d s
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
d : δ
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ.sectR a : (a : β) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α × β) → Measure γ) (a, f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.sectR a).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (a, f d)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply, sectR_apply, comap_apply]

Premises used: ProbabilityTheory.Kernel.sectR_apply, ProbabilityTheory.Kernel.comap_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
β : Type u_2
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
α : Type u_6
inst : MeasurableSpace α
κ : Kernel β γ
a : α
⊢ sectR (mα := inst) (prodMkLeft α κ) a = κ

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.sectR, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
mα : MeasurableSpace α
γ : Type u_4
mγ : MeasurableSpace γ
β : Type u_6
inst : MeasurableSpace β
κ : Kernel α γ
b : β
a : α
⊢ Eq.{u_4 + 1} (α := Measure γ) (((sectR (prodMkRight β κ) a : Kernel β γ) : (a : β) → Measure γ) b : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
⊢ κ.swapLeft.sectL = κ.sectR

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.sectR, ProbabilityTheory.Kernel.swapLeft, Prod.swap, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
⊢ κ.swapLeft.sectR = κ.sectL

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.sectL, ProbabilityTheory.Kernel.swapLeft, Prod.swap, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabit :
  ∀ (inhabited_h : Inhabited γ), IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ

Tactic:
inhabit γ
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ

Tactic:
⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
refine : ∀ (h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ)), IsSFiniteKernel κ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ) ↔ IsSFiniteKernel κ

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ)
rw : IsSFiniteKernel (sectR (mα := mγ) (prodMkLeft γ κ) default)
⊢ IsSFiniteKernel κ

Tactic:
rw [← sectR_prodMkLeft γ κ default]

Premises used: Inhabited.default, ProbabilityTheory.Kernel.sectR_prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft γ κ)
⊢ IsSFiniteKernel (sectR (mα := mγ) (prodMkLeft γ κ) default)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabit :
  ∀ (inhabited_h : Inhabited γ), IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ

Tactic:
inhabit γ
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ

Tactic:
⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
refine : ∀ (h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ)), IsSFiniteKernel κ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ) ↔ IsSFiniteKernel κ

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ)
rw : IsSFiniteKernel (sectL (mβ := mγ) (prodMkRight γ κ) default)
⊢ IsSFiniteKernel κ

Tactic:
rw [← sectL_prodMkRight γ κ default]

Premises used: Inhabited.default, ProbabilityTheory.Kernel.sectL_prodMkRight
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Nonempty γ
κ : Kernel α β
inhabited_h : Inhabited γ
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight γ κ)
⊢ IsSFiniteKernel (sectL (mβ := mγ) (prodMkRight γ κ) default)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
⊢ Eq.{u_3 + 1} (α := Measure γ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
    ((⇑(η ∘ₖ κ) : (a : α) → Measure γ) ∘ₘ μ)

Tactic:
Measure.bind_bind κ.aemeasurable η.aemeasurable

Premises used: MeasureTheory.Measure.join, ProbabilityTheory.Kernel.aemeasurable, MeasureTheory.Measure.bind, MeasureTheory.Measure.ofMeasurable, MeasureTheory.Measure.bind_bind
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
rw :
  Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    (bind.{u_1, u_2} (α := α) (mα := mα) ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) (⇑κ : (a : α) → Measure β))
rw₁ rw₂ : Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) ())

Tactic:
rw [Kernel.comp_apply, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.comp_apply, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((sum fun (ω : α) ↦
                HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
                  ((κ : (a : α) → Measure β) ω : Measure β) :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
    (sum fun (ω : α) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
        ((κ : (a : α) → Measure β) ω : Measure β))

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ AEMeasurable.{u_1, u_2} (β := Measure β) (⇑κ : (a : α) → Measure β) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
h :
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ =
    ∑' (i : α),
      (HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞)
            ((κ : (a : α) → Measure β) i : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (ω : α) ↦
              HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
                ((κ : (a : α) → Measure β) ω : Measure β) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Measure.sum_apply _ hs, Measure.bind_apply hs (by fun_prop)]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.Measure.sum_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ =
    ∑' (i : α),
      (HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞)
            ((κ : (a : α) → Measure β) i : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s

Tactic:
simp [lintegral_countable', mul_comm]

Premises used: MeasureTheory.lintegral_countable', mul_comm
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ ⊗ₘ κ).snd = (⇑κ : (a : α) → Measure β) ∘ₘ μ

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
h :
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.snd ⁻¹' s) ∂μ =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ
h₁ : MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).snd : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [bind_apply hs κ.aemeasurable, snd_apply hs, compProd_apply]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.aemeasurable, MeasureTheory.Measure.snd_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.snd ⁻¹' s) ∂μ =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ∂μ

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (α := α × β) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
h :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((η : (a : α) → Measure β) a : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)

Tactic:
bind_congr_right h

Premises used: MeasureTheory.Measure.bind_congr_right
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂(⇑κ : (a : α) → Measure β) ∘ₘ μ, p ω
⊢ ∀ᵐ (ω : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p ω

Tactic:
rw [comp_eq_comp_const_apply] at h

Premises used: MeasureTheory.Measure.comp_eq_comp_const_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂((κ : (a : α) → Measure β) ω' : Measure β), p ω

Tactic:
Kernel.ae_ae_of_ae_comp h

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂((κ : (a : α) → Measure β) ω' : Measure β), p ω

Tactic:
exact Kernel.ae_ae_of_ae_comp h

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp