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
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_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
h_1 : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hf :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦ ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ), f (b, c) = g (b, c)) x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (a_3 : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_3)) fun (y : γ) ↦ g (a_3, y) : E))
                      x)
                    ((fun (a_3 : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_3)) fun (y : γ) ↦ f (a_3, y) : E))
                      x))
                x}
            x}
      a_1
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a_1 : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y))
    fun (a_1 : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y)
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ), f (a_1, c) = g (a_1, c)) →
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y))
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
Tactic: filter_upwards [ae_ae_of_ae_compProd hfg] with x hfgx using
        integral_congr_ae (ae_eq_symm hfgx)
-- 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))
      fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
have rw : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ mβ ((κ.restrict (s := s) hs : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η.restrict (s := t) ht : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
    @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
Tactic: rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht, integral_compProd]
-- 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ.restrict (s := s) hs : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η.restrict (s := t) ht : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))
      fun (z : β × γ) ↦ f z)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
have rw₁ : @Integrable _ _ _ _ Prod.instMeasurableSpace f
  ((κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a)
Tactic: rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht, integral_compProd]
-- 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn (mα := Prod.instMeasurableSpace) f (s ×ˢ t) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f
    ((κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a)
have rw : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (s ×ˢ t))
Tactic: rw [compProd_restrict, Kernel.restrict_apply]
-- 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
s : Set β
hs : MeasurableSet s
hf :
  IntegrableOn (mα := Prod.instMeasurableSpace) f (SProd.sprod (β := Set γ) s univ)
    ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (SProd.sprod (β := Set γ) s univ)) fun (z : β × γ) ↦
      f z)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
have simp_rw : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
    @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) univ) fun (y : γ) ↦ f (x, y))
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) s) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
Tactic: simp_rw [setIntegral_compProd hs MeasurableSet.univ hf, Measure.restrict_univ]
-- 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
t : Set γ
ht : MeasurableSet t
hf :
  IntegrableOn (mα := Prod.instMeasurableSpace) f (SProd.sprod (α := Set β) univ t)
    ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) (SProd.sprod (α := Set β) univ t)) fun (z : β × γ) ↦
      f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
have simp_rw : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) univ) fun (x : β) ↦
    @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ (Measure.restrict ((η : (a : α × β) → Measure γ) (a, x)) t) fun (y : γ) ↦ f (x, y))
Tactic: simp_rw [setIntegral_compProd MeasurableSet.univ ht hf, Measure.restrict_univ]
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = AEStronglyMeasurable.mk f hf z)
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq.{u_4 + 1} (α := E)
                  ((fun (x : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y : E)) x)
                  ((fun (x : β) ↦
                      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y :
                        E))
                    x))
              x}
          x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_comp 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
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 γ), f z = AEStronglyMeasurable.mk f hf z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (x : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y : E)) x)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
                            AEStronglyMeasurable.mk f hf 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 γ) x) fun (y : γ) ↦ f y) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), f z = AEStronglyMeasurable.mk f hf z) →
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf y)
Tactic: filter_upwards [ae_ae_of_ae_comp 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 α β
η : Kernel β γ
δ : Type u_5
inst : TopologicalSpace δ
f : γ → δ
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = AEStronglyMeasurable.mk f hf z)
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β | (fun (x : β) ↦ AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)) x} x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with x hx using
    ⟨hf.mk f, hf.stronglyMeasurable_mk, 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 α β
η : Kernel β γ
δ : Type u_5
inst : TopologicalSpace δ
f : γ → δ
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 γ), f z = AEStronglyMeasurable.mk f hf z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β | (fun (x : β) ↦ AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)) x} x}
      a_1
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) x)
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), f z = AEStronglyMeasurable.mk f hf z) →
    AEStronglyMeasurable (m₀ := mγ) f ((η : (a : β) → Measure γ) a_1)
Tactic: filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with x hx using
    ⟨hf.mk f, hf.stronglyMeasurable_mk, 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
⊢ @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)
have 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 <
      ∞
Tactic: simp_rw [hasFiniteIntegral_iff_enorm, lintegral_comp _ _ _ hf.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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
⊢ ∫⁻ (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 <
        ∞
have 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 < ∞
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]
-- 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
p q r : Prop
h : 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 h]
-- 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
p q r : Prop
h : 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 h]
-- 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 α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
⊢ ∫⁻ (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 <
        ∞
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 h ↦ by
    rw [← and_congr_right_iff, and_iff_right_of_imp h]
-- 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 α β
η : 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 < ∞) ∧
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).toReal ∂(κ : (a : α) → Measure β) a <
        ∞
have 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 <
      ∞)
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 α β
η : 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 <
        ∞)
⊢ ∫⁻ (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 <
        ∞
have rw₁ : ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ →
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) 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 α β
η : 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 < ∞
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a < ∞ ↔
    ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) a).toReal ∂(κ : (a : α) → Measure β) a < ∞
have 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
Tactic: rw [lintegral_congr_ae]
-- 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 α β
η : 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 < ∞
⊢ (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
have h₁ : ∀ (x : β) (hx : ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x < ∞),
  ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) x =
    ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x).toReal
Tactic: filter_upwards [h] with x 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 α β
η : 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 < ∞
⊢ ∫⁻ (c : γ), ‖f c‖ₑ ∂(η : (a : β) → Measure γ) x =
    ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x).toReal
have h₁ : ∫⁻ (a : γ), ‖f a‖ₑ ∂(η : (a : β) → Measure γ) x ≠ ∞
Tactic: rw [ofReal_toReal]