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 β γ
f : γ → E
hf : StronglyMeasurable f
simp_rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞) ∧
      ∫⁻ (a : β),
          enorm (E := ℝ)
            (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ ‖f y‖) ∂(κ : (a : α) → Measure β) a <
        ∞
⊢ @HasFiniteIntegral _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, lintegral_comp _ _ _ hf.enorm]

Premises used: MeasureTheory.StronglyMeasurable.enorm, ProbabilityTheory.Kernel.lintegral_comp, 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
simp_rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞) ∧
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).toReal ∂(κ : (a : α) → Measure β) a <
        ∞
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞) ∧
      ∫⁻ (a : β),
          enorm (E := ℝ)
            (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ ‖f y‖) ∂(κ : (a : α) → Measure β) a <
        ∞

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun y ↦ norm_nonneg _)
      hf.norm.aestronglyMeasurable, enorm_eq_ofReal toReal_nonneg, ofReal_norm]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, ENNReal.toReal_nonneg, MeasureTheory.ae_of_all, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, MeasureTheory.StronglyMeasurable.norm, ofReal_norm, Real.enorm_eq_ofReal, 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
p q r : Prop
h : 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 h]

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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
⊢ ∀ {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 h ↦ by
    rw [← and_congr_right_iff, and_iff_right_of_imp h]
-- 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 β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
rw :
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞) →
    (∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).toReal ∂(κ : (a : α) → Measure β) a <
        ∞)
rw₁ :
  ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ →
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞) ∧
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞
rw :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b) fun (a : β) ↦
    ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).toReal
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
    ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞
h₁ :
  ∀ (x : β) (hx : ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞),
    ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) x =
      ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x).toReal
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b) fun (a : β) ↦
    ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).toReal

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

Tactic:
fun h ↦ ae_lt_top hf.enorm.lintegral_kernel h.ne

Premises used: MeasureTheory.StronglyMeasurable.enorm, Measurable.lintegral_kernel, 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ →
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞

Tactic:
exact fun h ↦ ae_lt_top hf.enorm.lintegral_kernel h.ne

Premises used: MeasureTheory.StronglyMeasurable.enorm, Measurable.lintegral_kernel, 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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
rw :
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)
⊢ @HasFiniteIntegral _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]

Premises used: MeasureTheory.hasFiniteIntegral_congr, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, ProbabilityTheory.hasFiniteIntegral_comp_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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)

Premises used: MeasureTheory.hasFiniteIntegral_congr, Filter.eventually_congr, 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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
refine_1 :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)
refine_2 :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)

Premises used: MeasureTheory.hasFiniteIntegral_congr, Filter.eventually_congr, 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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
a_1 : β
hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), AEStronglyMeasurable.mk f hf z = f z
⊢ @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) a_1) ↔
    @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) a_1)

Tactic:
hasFiniteIntegral_congr hx

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 α β
η : Kernel β γ
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 γ), AEStronglyMeasurable.mk f hf z = f z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
                    @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (a_1 : β) (hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), AEStronglyMeasurable.mk f hf z = f z),
    @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) a_1) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) a_1)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)

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

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp, 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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
a_1 : β
hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), AEStronglyMeasurable.mk f hf z = f z
⊢ Eq (α := ℝ) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
    (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ ‖f 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 α β
η : Kernel β γ
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 γ), AEStronglyMeasurable.mk f hf z = f z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
                            ‖AEStronglyMeasurable.mk f hf y‖ :
                          ℝ))
                      x)
                    ((fun (x : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖ : ℝ)) x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (a_1 : β) (hx : ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), AEStronglyMeasurable.mk f hf z = f z),
    Eq (α := ℝ) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ ‖f y‖)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖

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

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp, 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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) ↔
    (∀ᵐ (y : β) ∂((κ : (a : α) → Measure β) a : Measure β), @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) y)) ∧
      @Integrable ℝ _ _ _ mβ (fun (y : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) y) fun (z : γ) ↦ ‖f z‖)
        ((κ : (a : α) → Measure β) a)

Tactic:
simp only [Integrable, hf, hasFiniteIntegral_comp_iff' hf, true_and, eventually_and, hf.comp,
    hf.norm.integral_kernel_comp]

Premises used: Filter.eventually_and, MeasureTheory.AEStronglyMeasurable.comp, MeasureTheory.Integrable, MeasureTheory.AEStronglyMeasurable.norm, ProbabilityTheory.hasFiniteIntegral_comp_iff', MeasureTheory.AEStronglyMeasurable.integral_kernel_comp, true_and
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
rw :
  (∀ᵐ (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)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ
hf₁ : AEStronglyMeasurable (m₀ := mβ) f ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) ())
⊢ @Integrable _ _ _ _ mβ f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ

Tactic:
rw [Measure.comp_eq_comp_const_apply, ProbabilityTheory.integrable_comp_iff]

Premises used: MeasureTheory.Measure.comp_eq_comp_const_apply, ProbabilityTheory.integrable_comp_iff
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ (∀ᵐ (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)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ AEStronglyMeasurable (m₀ := mβ) f ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) ())

Tactic:
simpa [Kernel.comp_apply]

Premises used: ProbabilityTheory.Kernel.comp_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 β γ
f : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) x)

Tactic:
((integrable_comp_iff hf.1).1 hf).1

Premises used: And.left, Iff.mp, ProbabilityTheory.integrable_comp_iff