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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
⊢ IsClosed (X := ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)))
    {f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)) |
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)}

Tactic:
isClosed_eq continuous_integral Kernel.continuous_integral_integral_comp

Premises used: ProbabilityTheory.Kernel.continuous_integral_integral_comp, isClosed_eq, MeasureTheory.continuous_integral
-- 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
hE : CompleteSpace E
⊢ IsClosed (X := ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)))
    {f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)) |
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)}

Tactic:
exact isClosed_eq continuous_integral Kernel.continuous_integral_integral_comp

Premises used: ProbabilityTheory.Kernel.continuous_integral_integral_comp, isClosed_eq, MeasureTheory.continuous_integral
-- 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_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
h :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
h₁ :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
h :
  EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y) fun (a : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
x : β
hfgx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) x : Measure γ), f z = g z
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
    (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β | (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = g z) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (a : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y : E)) x)
                    ((fun (a : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y : E)) x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (x : β) (hfgx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) x : Measure γ), f z = g z),
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y) fun (a : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y

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

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp
-- 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
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η.restrict (s := s) hs : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)
rw₁ : @Integrable _ _ _ _ mγ f ((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ (Measure.restrict ((η ∘ₖ κ : (a : α) → Measure γ) a) s) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)

Tactic:
rw [← restrict_apply (η ∘ₖ κ) hs, ← comp_restrict hs, integral_comp]

Premises used: ProbabilityTheory.Kernel.comp, ProbabilityTheory.Kernel.restrict_apply, ProbabilityTheory.Kernel.integral_comp, ProbabilityTheory.Kernel.comp_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η.restrict (s := s) hs : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)

Tactic:
simp_rw [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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
rwa : @Integrable _ _ _ _ mγ f (((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a)
rwa₁ rwa₂ rwa₃ rwa₄ : @Integrable _ _ _ _ mγ f (Measure.restrict ((η ∘ₖ κ : (a : α) → Measure γ) a) s)
⊢ @Integrable _ _ _ _ mγ f ((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a)

Tactic:
rwa [comp_restrict, restrict_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply, ProbabilityTheory.Kernel.comp_restrict
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
f : α → β → E
hf : AEStronglyMeasurable (uncurry f) (μ ⊗ₘ κ)
⊢ ∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (m₀ := mβ) (f x) ((κ : (a : α) → Measure β) x)

Tactic:
simpa using hf.compProd_mk_left

Premises used: MeasureTheory.AEStronglyMeasurable.compProd_mk_left
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
simp_rw :
  @Integrable _ _ _ _ Prod.instMeasurableSpace f
      ((Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
simp_rw₁ :
  (∀ᵐ (x : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
        @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y))
          (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x))) ∧
      @Integrable ℝ _ _ _ mα
        (fun (x : α) ↦
          @integral _ _ _ _ mβ
            (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x)) fun (y : β) ↦
            ‖f (x, y)‖)
        ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
simp_rw₂ :
  (∀ᵐ (x : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
        @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      @Integrable ℝ _ _ _ mα (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖)
        ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ

Tactic:
simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply,
    Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.prodMkLeft_apply, ProbabilityTheory.integrable_compProd_iff, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
rw :
  Eq.{u_8 + 1} (α := E)
    (@integral _ _ _ _ mα ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) fun (x : α) ↦
      @integral _ _ _ _ mβ (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x))
        fun (y : β) ↦ f (x, y))
    (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f (a, b) ∂μ)
⊢ Eq.{u_8 + 1} (α := E) (∫ (x : α × β), f x ∂μ ⊗ₘ κ)
    (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f (a, b) ∂μ)

Tactic:
rw [Measure.compProd, ProbabilityTheory.integral_compProd hf]

Premises used: MeasureTheory.Measure.compProd, ProbabilityTheory.integral_compProd
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ Eq.{u_8 + 1} (α := E)
    (@integral _ _ _ _ mα ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) fun (x : α) ↦
      @integral _ _ _ _ mβ (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x))
        fun (y : β) ↦ f (x, y))
    (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f (a, b) ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
rw :
  Eq.{u_8 + 1} (α := E)
    (@integral _ _ _ _ mα (restrict ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) s) fun (x : α) ↦
      @integral _ _ _ _ mβ
        (restrict (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x)) t)
        fun (y : β) ↦ f (x, y))
    (∫ (a : α) in s, @integral _ _ _ _ mβ (restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ f (a, b) ∂μ)
⊢ Eq.{u_8 + 1} (α := E) (∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ)
    (∫ (a : α) in s, @integral _ _ _ _ mβ (restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ f (a, b) ∂μ)

Tactic:
rw [Measure.compProd, ProbabilityTheory.setIntegral_compProd hs ht hf]

Premises used: ProbabilityTheory.setIntegral_compProd, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ Eq.{u_8 + 1} (α := E)
    (@integral _ _ _ _ mα (restrict ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) s) fun (x : α) ↦
      @integral _ _ _ _ mβ
        (restrict (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x)) t)
        fun (y : β) ↦ f (x, y))
    (∫ (a : α) in s, @integral _ _ _ _ mβ (restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ f (a, b) ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst_1 : SFinite μ
inst_2 : IsSFiniteKernel κ
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
rw : AEStronglyMeasurable (m₀ := mβ) f (map Prod.snd (μ ⊗ₘ κ))
⊢ Integrable (ε := E) (fun (p : α × β) ↦ f p.2) (μ ⊗ₘ κ) ↔ @Integrable _ _ _ _ mβ f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [← Measure.snd_compProd, Measure.snd, integrable_map_measure _ measurable_snd.aemeasurable,
    Function.comp_def]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.snd, Function.comp_def, measurable_snd, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst_1 : SFinite μ
inst_2 : IsSFiniteKernel κ
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
rwa : AEStronglyMeasurable f (μ ⊗ₘ κ).snd
rwa₁ rwa₂ rwa₃ rwa₄ : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ AEStronglyMeasurable (m₀ := mβ) f (map Prod.snd (μ ⊗ₘ κ))

Tactic:
rwa [← Measure.snd, Measure.snd_compProd]

Premises used: MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.snd
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int :
  (∀ᵐ (y : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) y)) ∧
    @Integrable ℝ _ _ _ mα (fun (y : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (z : β) ↦ ‖f z‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ())
⊢ ∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)

Tactic:
h_int.1

Premises used: And.left
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int :
  (∀ᵐ (y : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) y)) ∧
    @Integrable ℝ _ _ _ mα (fun (y : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (z : β) ↦ ‖f z‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ())
⊢ ∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)

Tactic:
exact h_int.1

Premises used: And.left
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int :
  (∀ᵐ (y : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) y)) ∧
    @Integrable ℝ _ _ _ mα (fun (y : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (z : β) ↦ ‖f z‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ())
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ

Tactic:
h_int.2

Premises used: And.right