awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
b : β
hb :
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal
      (ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))) ≤
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t)
have h : LE.le (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
  ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)
Tactic: rw [ofReal_toReal hb.ne]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ ∫⁻ (a_1 : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (Prod.mk a_1 ⁻¹' s))) ∂(κ : (a : α) → Measure β) a <
    ∞
have b : ∫⁻ (b : β),
    ENNReal.ofReal
      (ENNReal.toReal
        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s))) ∂(κ : (a : α) → Measure β) a ≤
  ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a
Tactic: calc
    ∫⁻ b, ENNReal.ofReal (η (a, b) (Prod.mk b ⁻¹' s)).toReal ∂κ a
    _ ≤ ∫⁻ b, η (a, b) (Prod.mk b ⁻¹' t) ∂κ a := by
      refine lintegral_mono_ae ?_
      filter_upwards [ae_kernel_lt_top a h2s] with b hb
      rw [ofReal_toReal hb.ne]
      exact measure_mono (preimage_mono (subset_toMeasurable _ _))
    _ ≤ (κ ⊗ₖ η) a t := le_compProd_apply _ _ _ _
    _ = (κ ⊗ₖ η) a s := measure_toMeasurable s
    _ < ⊤ := h2s.lt_top
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
have left : AEStronglyMeasurable (β := ℝ) (m₀ := mβ)
  (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
  ((κ : (a : α) → Measure β) a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
left :
  AEStronglyMeasurable (β := ℝ) (m₀ := mβ)
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
have right : @HasFiniteIntegral _ ℝ _ mβ
  (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
  ((κ : (a : α) → Measure β) a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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 : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf (x, y)
have 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 : β) ↦
                Eq.{u_4 + 1} (α := E)
                  ((fun (x : β) ↦
                      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) : E))
                    x)
                  ((fun (x : β) ↦
                      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
                          AEStronglyMeasurable.mk f hf (x, y) :
                        E))
                    x))
              x}
          x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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 : 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 : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) : E))
                      x)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
                            AEStronglyMeasurable.mk f hf (x, y) :
                          E))
                      x))
                x}
            x}
      a_1
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf (x, y)
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ),
      f (a_1, c) = AEStronglyMeasurable.mk f hf (a_1, c)) →
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
        AEStronglyMeasurable.mk f hf (a_1, y))
Tactic: filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
have 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
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⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ),
      f (a_1, c) = AEStronglyMeasurable.mk f hf (a_1, c)) →
    AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (a_1, y))
      ((η : (a : α × β) → Measure γ) (a, a_1))
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⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
⊢ @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)
have 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 <
      ∞
Tactic: simp only [hasFiniteIntegral_iff_enorm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
⊢ ∫⁻ (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 <
        ∞
have 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 <
      ∞
Tactic: rw [lintegral_compProd _ _ _ h1f.enorm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (hypothesis)
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
⊢ ∫⁻ (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 <
        ∞
have this : ∀ (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 _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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)‖
⊢ ∫⁻ (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 <
        ∞
have 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 <
      ∞
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)
have rw : (r ↔ p ∧ q) ↔ (p ∧ r ↔ p ∧ q)
Tactic: rw [← and_congr_right_iff, and_iff_right_of_imp h1]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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)
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)
have rw₁ : (r ↔ p ∧ q) ↔ (r ↔ p ∧ q)
Tactic: rw [← and_congr_right_iff, and_iff_right_of_imp h1]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (hypothesis)
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)‖
⊢ ∫⁻ (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 <
        ∞
have this₁ : ∀ {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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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))
⊢ ∫⁻ (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 <
        ∞
have 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 <
      ∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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 <
        ∞)
⊢ ∫⁻ (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 <
        ∞
have 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) < ∞
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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) < ∞
⊢ ∫⁻ (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 <
      ∞
have 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
Tactic: rw [lintegral_congr_ae]