awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))

Tactic:
hf
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h_1 : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
h :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
h₁ :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))

Tactic:
convert! hf using 1
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)

Tactic:
integral_congr_ae hfg.symm

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)

Tactic:
exact integral_congr_ae hfg.symm

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h_1 : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
h :
  EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a_1 : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y))
    fun (a_1 : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
x : β
hfgx : ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), f (x, c) = g (x, c)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
    (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))

Tactic:
integral_congr_ae (ae_eq_symm hfgx)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_eq_symm
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h_1 : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦ ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), f (b, c) = g (b, c)) x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (a_3 : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_3)) fun (y : γ) ↦ g (a_3, y) : E))
                      x)
                    ((fun (a_3 : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_3)) fun (y : γ) ↦ f (a_3, y) : E))
                      x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (x : β) (hfgx : ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), f (x, c) = g (x, c)),
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a_1 : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y))
    fun (a_1 : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hfg] with x hfgx using
        integral_congr_ae (ae_eq_symm hfgx)

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.restrict (s := s) hs : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η.restrict (s := t) ht : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
rw₁ :
  @Integrable _ _ _ _ Prod.instMeasurableSpace f
    ((κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))
      fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))

Tactic:
rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht, integral_compProd]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasurableSet.prod, ProbabilityTheory.Kernel.compProd_restrict, ProbabilityTheory.integral_compProd, ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.restrict (s := s) hs : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η.restrict (s := t) ht : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))

Tactic:
simp_rw [Kernel.restrict_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
rw : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f
    ((κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a)

Tactic:
rw [compProd_restrict, Kernel.restrict_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply, ProbabilityTheory.Kernel.compProd_restrict
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))

Tactic:
hf

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))

Tactic:
exact hf
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
s : Set β
hs : MeasurableSet s
hf :
  IntegrableOn (mα := Prod.instMeasurableSpace) f (SProd.sprod (β := Set γ) s univ)
    ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
simp_rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) univ) fun (y : γ) ↦ f (x, y))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (SProd.sprod (β := Set γ) s univ)) fun (z : β × γ) ↦
      f z)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))

Tactic:
simp_rw [setIntegral_compProd hs MeasurableSet.univ hf, Measure.restrict_univ]

Premises used: ProbabilityTheory.setIntegral_compProd, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
t : Set γ
ht : MeasurableSet t
hf :
  IntegrableOn (mα := Prod.instMeasurableSpace) f (SProd.sprod (α := Set β) univ t)
    ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
simp_rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) univ) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (SProd.sprod (α := Set β) univ t)) fun (z : β × γ) ↦
      f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))

Tactic:
simp_rw [setIntegral_compProd MeasurableSet.univ ht hf, Measure.restrict_univ]

Premises used: ProbabilityTheory.setIntegral_compProd, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
a_1 : β
hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), f z = AEStronglyMeasurable.mk f hf z
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y)
    (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y)

Tactic:
integral_congr_ae hx

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (y : β) ↦
                  ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = AEStronglyMeasurable.mk f hf z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (x : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y : E)) x)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
                            AEStronglyMeasurable.mk f hf y :
                          E))
                      x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (a_1 : β) (hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), f z = AEStronglyMeasurable.mk f hf z),
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y)
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y

Tactic:
filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with _ hx using integral_congr_ae hx

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp, MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel β γ
δ : Type u_5
inst : TopologicalSpace δ
f : γ → δ
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
x : β
hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) x : Measure γ), f z = AEStronglyMeasurable.mk f hf z
⊢ AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)

Tactic:
⟨hf.mk f, hf.stronglyMeasurable_mk, hx⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel β γ
δ : Type u_5
inst : TopologicalSpace δ
f : γ → δ
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (y : β) ↦
                  ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = AEStronglyMeasurable.mk f hf z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β | (fun (x : β) ↦ AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)) x} x}
      a_1
h₁ h₂ :
  ∀ (x : β) (hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) x : Measure γ), f z = AEStronglyMeasurable.mk f hf z),
    AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)

Tactic:
filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with x hx using
    ⟨hf.mk f, hf.stronglyMeasurable_mk, hx⟩

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp, MeasureTheory.AEStronglyMeasurable.ae_eq_mk