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 η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                    AEStronglyMeasurable.mk f h1f (b, c) = f (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
                      ((η : (a : α × β) → Measure γ) (a, x)) ↔
                    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y))
                      ((η : (a : α × β) → Measure γ) (a, x)))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (x : β)
    (hx :
      ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), AEStronglyMeasurable.mk f h1f (x, c) = f (x, c)),
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x)) ↔
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x)) ↔
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))

Tactic:
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x hx using
      hasFiniteIntegral_congr hx

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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 η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h₂ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖
⊢ @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
      ((κ : (a : α) → Measure β) a) ↔
    @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
      ((κ : (a : α) → Measure β) a)

Tactic:
apply hasFiniteIntegral_congr

Premises used: MeasureTheory.hasFiniteIntegral_congr
-- 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 η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
a_1 : β
hx :
  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ), AEStronglyMeasurable.mk f h1f (a_1, c) = f (a_1, c)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
      ‖AEStronglyMeasurable.mk f h1f (a_1, y)‖)
    (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ ‖f (a_1, y)‖)

Tactic:
integral_congr_ae (EventuallyEq.fun_comp hx _)

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.fun_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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                    AEStronglyMeasurable.mk f h1f (b, c) = f (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
                            ‖AEStronglyMeasurable.mk f h1f (x, y)‖ :
                          ℝ))
                      x)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖ : ℝ))
                      x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (a_1 : β)
    (hx :
      ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ),
        AEStronglyMeasurable.mk f h1f (a_1, c) = f (a_1, c)),
    Eq (α := ℝ)
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
        ‖AEStronglyMeasurable.mk f h1f (a_1, y)‖)
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ ‖f (a_1, y)‖)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖

Tactic:
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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 η
f : β × γ → E
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
simp only [Integrable, hasFiniteIntegral_compProd_iff' hf, hf.norm.integral_kernel_compProd,
    hf, hf.compProd_mk_left, eventually_and, true_and]

Premises used: Filter.eventually_and, MeasureTheory.Integrable, ProbabilityTheory.hasFiniteIntegral_compProd_iff', MeasureTheory.AEStronglyMeasurable.compProd_mk_left, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd, true_and
-- 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 η
f : β × γ → E
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))

Tactic:
((integrable_compProd_iff hf.aestronglyMeasurable).mp hf).1

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, ProbabilityTheory.integrable_compProd_iff, And.left, Iff.mp
-- 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 η
f : β × γ → E
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @Integrable ℝ _ _ _ mβ
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
    ((κ : (a : α) → Measure β) a)

Tactic:
((integrable_compProd_iff hf.aestronglyMeasurable).mp hf).2

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, ProbabilityTheory.integrable_compProd_iff, And.right, Iff.mp
-- 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
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @Integrable.{u_4, u_2} E _ _ _ mβ
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
    ((κ : (a : α) → Measure β) a)

Tactic:
Integrable.mono hf.integral_norm_compProd hf.aestronglyMeasurable.integral_kernel_compProd <|
    Eventually.of_forall fun x =>
      (norm_integral_le_integral_norm _).trans_eq <|
        (norm_of_nonneg <|
            integral_nonneg_of_ae <|
              Eventually.of_forall fun y => (norm_nonneg (f (x, y)) :)).symm

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, LE.le.trans_eq, MeasureTheory.Integrable.mono, MeasureTheory.norm_integral_le_integral_norm, Prod.mk, Filter.Eventually.of_forall, MeasureTheory.Integrable.integral_norm_compProd, MeasureTheory.integral_nonneg_of_ae, MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd, Eq.symm, norm_nonneg, Real.norm_of_nonneg
-- 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))))

Tactic:
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
refine :
  EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
    fun (x : β) ↦
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))))

Tactic:
refine 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β)
    (h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1)))
    (h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))),
    F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) + g (a_1, y)) =
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
    fun (x : β) ↦
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))

Tactic:
filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g

Premises used: MeasureTheory.Integrable.ae_of_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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
a_1 : β
h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))
h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))
⊢ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) + g (a_1, y)) =
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))

Tactic:
simp [integral_add h2f h2g]

Premises used: MeasureTheory.integral_add
-- 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))))

Tactic:
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
refine :
  EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))))

Tactic:
refine 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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β)
    (h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1)))
    (h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))),
    F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) - g (a_1, y)) =
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))

Tactic:
filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g

Premises used: MeasureTheory.Integrable.ae_of_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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
a_1 : β
h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))
h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))
⊢ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) - g (a_1, y)) =
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))

Tactic:
simp [integral_sub h2f h2g]

Premises used: MeasureTheory.integral_sub
-- 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 g : β × γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ ∫⁻ (x : β),
      F
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          f (x, y) - g (x, y)) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            g (x, y))) ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae