awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
δ : Type u_5
inst_2 : TopologicalSpace δ
f : β × γ → δ
hf : 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 γ),
                    f (b, c) = AEStronglyMeasurable.mk f hf (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (x, y))
                    ((η : (a : α × β) → Measure γ) (a, x)))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (x : β)
    (hx :
      ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), f (x, c) = AEStronglyMeasurable.mk f hf (x, c)),
    AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with x hx using
    ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

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

Tactic:
simp only [hasFiniteIntegral_iff_enorm]

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm
-- 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 : StronglyMeasurable f
rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞) ∧
      ∫⁻ (a_1 : β),
          enorm (E := ℝ)
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
              ‖f (a_1, y)‖) ∂(κ : (a : α) → Measure β) a <
        ∞
⊢ ∫⁻ (a : β × γ), ‖f a‖ₑ ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞) ∧
      ∫⁻ (a_1 : β),
          enorm (E := ℝ)
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
              ‖f (a_1, y)‖) ∂(κ : (a : α) → Measure β) a <
        ∞

Tactic:
rw [lintegral_compProd _ _ _ h1f.enorm]

Premises used: MeasureTheory.StronglyMeasurable.enorm, ProbabilityTheory.Kernel.lintegral_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 η
f : β × γ → E
h1f : StronglyMeasurable f
⊢ ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖

Tactic:
have : ∀ x, ∀ᵐ y ∂η (a, x), 0 ≤ ‖f (x, y)‖ := fun x => Eventually.of_forall fun y => norm_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 η
f : β × γ → E
h1f : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
simp_rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞) ∧
      ∫⁻ (a_1 : β),
          ENNReal.ofReal
            (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_1)).toReal ∂(κ : (a : α) → Measure β) a <
        ∞
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞) ∧
      ∫⁻ (a_1 : β),
          enorm (E := ℝ)
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
              ‖f (a_1, y)‖) ∂(κ : (a : α) → Measure β) a <
        ∞

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
      (h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
    enorm_eq_ofReal toReal_nonneg, ofReal_norm]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, ENNReal.toReal_nonneg, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, MeasureTheory.StronglyMeasurable.norm, ofReal_norm, Real.enorm_eq_ofReal, measurable_prodMk_left
-- 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 : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
rw : (r ↔ p ∧ q) ↔ (p ∧ r ↔ p ∧ q)
rw₁ rw₂ : (r ↔ p ∧ q) ↔ (r ↔ p ∧ q)
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)

Tactic:
rw [← and_congr_right_iff, and_iff_right_of_imp h1]

Premises used: and_congr_right_iff, and_iff_right_of_imp
-- 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 : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
⊢ ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))

Tactic:
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
    rw [← and_congr_right_iff, and_iff_right_of_imp h1]
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
rw :
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞) →
    (∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ ↔
      ∫⁻ (a_2 : β),
          ENNReal.ofReal
            (∫⁻ (a : γ), ‖f (a_2, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_2)).toReal ∂(κ : (a : α) → Measure β) a <
        ∞)
rw₁ :
  ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ →
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞) ∧
      ∫⁻ (a_1 : β),
          ENNReal.ofReal
            (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_1)).toReal ∂(κ : (a : α) → Measure β) a <
        ∞

Tactic:
rw [this]
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
rw :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b)) fun (a_1 : β) ↦
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_1)).toReal
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞ ↔
    ∫⁻ (a_1 : β),
        ENNReal.ofReal
          (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_1)).toReal ∂(κ : (a : α) → Measure β) a <
      ∞

Tactic:
rw [lintegral_congr_ae]

Premises used: MeasureTheory.lintegral_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 η
f : β × γ → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
h :
  ∀ (x : β) (hx : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞),
    ∫⁻ (c : γ), ‖f (x, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) =
      ENNReal.ofReal (∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)).toReal
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b)) fun (a_1 : β) ↦
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_1)).toReal

Tactic:
filter_upwards [h2f] with x hx
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
x : β
hx : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
h : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ≠ ∞
⊢ ∫⁻ (c : γ), ‖f (x, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) =
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)).toReal

Tactic:
rw [ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
x : β
hx : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
⊢ ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ≠ ∞

Tactic:
finiteness
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞

Tactic:
ae_lt_top ?_ h2f.ne

Premises used: LT.lt.ne, MeasureTheory.ae_lt_top
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞
refine : Measurable (β := ℝ≥0∞) fun (x : β) ↦ ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞

Tactic:
refine ae_lt_top ?_ h2f.ne

Premises used: LT.lt.ne, MeasureTheory.ae_lt_top
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)

Tactic:
h1f.enorm.lintegral_kernel_prod_right''

Premises used: MeasureTheory.StronglyMeasurable.enorm, Measurable.lintegral_kernel_prod_right''
-- 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 : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)

Tactic:
exact h1f.enorm.lintegral_kernel_prod_right''

Premises used: MeasureTheory.StronglyMeasurable.enorm, Measurable.lintegral_kernel_prod_right''
-- 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)
rw :
  (∀ᵐ (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 _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)
⊢ @HasFiniteIntegral _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
    hasFiniteIntegral_compProd_iff h1f.stronglyMeasurable_mk]

Premises used: MeasureTheory.hasFiniteIntegral_congr, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, ProbabilityTheory.hasFiniteIntegral_compProd_iff
-- 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₁ :
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x))) ↔
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
h₂ :
  @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)
⊢ (∀ᵐ (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 _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
apply and_congr

Premises used: and_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)
h₁ :
  ∀ᵐ (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))
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x))) ↔
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))

Tactic:
apply eventually_congr

Premises used: Filter.eventually_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)
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))

Tactic:
hasFiniteIntegral_congr hx

Premises used: MeasureTheory.hasFiniteIntegral_congr