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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
i_f : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
i_g : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
hg :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
pos :
  HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ g a) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (z : γ) ↦ (f + g) z
pos₁ :
  HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ g a) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ g a)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ (f + g) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ (f + g) y)
have pos₂ : HAdd.hAdd (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ f a)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ g a) =
  HAdd.hAdd (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ f a)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ g a)
Tactic: simp_rw [integral_add' i_f i_g, integral_integral_add'_comp i_f i_g, hf, hg]
-- 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_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
have h : Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
  (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
Tactic: convert! hf using 1
-- 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_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
h :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
have h₁ : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
Tactic: convert! hf using 1
-- 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_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
have h : EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
  (fun (a : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y) fun (a : β) ↦
  @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y
Tactic: apply integral_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 β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y) fun (a : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β | (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = g z) x} x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq.{u_4 + 1} (α := E)
                  ((fun (a : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y : E)) x)
                  ((fun (a : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y : E)) x))
              x}
          x}
    a
Tactic: filter_upwards [ae_ae_of_ae_comp 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β | (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), f z = g z) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (a : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y : E)) x)
                    ((fun (a : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y : E)) x))
                x}
            x}
      a
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (a : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y) fun (a : β) ↦
    @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y
have h₁ : ∀ (a : β),
  (∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a : Measure γ), f z = g z) →
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
Tactic: filter_upwards [ae_ae_of_ae_comp 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ (Measure.restrict ((η ∘ₖ κ : (a : α) → Measure γ) a) s) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)
have rw : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η.restrict (s := s) hs : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)
Tactic: rw [← restrict_apply (η ∘ₖ κ) hs, ← comp_restrict hs, integral_comp]
-- 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
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
rw :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η.restrict (s := s) hs : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ (Measure.restrict ((η ∘ₖ κ : (a : α) → Measure γ) a) s) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((η : (a : β) → Measure γ) x) s) fun (y : γ) ↦ f y)
have rw₁ : @Integrable _ _ _ _ mγ f ((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a)
Tactic: rw [← restrict_apply (η ∘ₖ κ) hs, ← comp_restrict hs, integral_comp]
-- 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
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ @Integrable _ _ _ _ mγ f ((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a)
have rwa : @Integrable _ _ _ _ mγ f (((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a)
Tactic: rwa [comp_restrict, 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn (mα := mγ) f s ((η ∘ₖ κ : (a : α) → Measure γ) a)
rwa : @Integrable _ _ _ _ mγ f (((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a)
⊢ @Integrable _ _ _ _ mγ f ((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a)
have rwa₁ : @Integrable _ _ _ _ mγ f (Measure.restrict ((η ∘ₖ κ : (a : α) → Measure γ) a) s)
Tactic: rwa [comp_restrict, restrict_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
have simp_rw : @Integrable _ _ _ _ Prod.instMeasurableSpace f
    ((Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) ↔
  (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
    Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
Tactic: simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
simp_rw :
  @Integrable _ _ _ _ Prod.instMeasurableSpace f
      ((Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
have simp_rw₁ : (∀ᵐ (x : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y))
        (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x))) ∧
    @Integrable ℝ _ _ _ mα
      (fun (x : α) ↦
        @integral _ _ _ _ mβ
          (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x)) fun (y : β) ↦
          ‖f (x, y)‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
  (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
    Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
Tactic: simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
simp_rw :
  @Integrable _ _ _ _ Prod.instMeasurableSpace f
      ((Kernel.const Unit μ ⊗ₖ prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
simp_rw₁ :
  (∀ᵐ (x : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
        @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y))
          (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x))) ∧
      @Integrable ℝ _ _ _ mα
        (fun (x : α) ↦
          @integral _ _ _ _ mβ
            (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x)) fun (y : β) ↦
            ‖f (x, y)‖)
        ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
have simp_rw₂ : (∀ᵐ (x : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
    @Integrable ℝ _ _ _ mα (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
  (∀ᵐ (x : α) ∂μ, @Integrable.{u_8, u_6} E _ _ _ mβ (fun (y : β) ↦ f (x, y)) ((κ : (a : α) → Measure β) x)) ∧
    Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f (x, y)‖) μ
Tactic: simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : α × β → E
hf : Integrable f (μ ⊗ₘ κ)
⊢ Eq.{u_8 + 1} (α := E) (∫ (x : α × β), f x ∂μ ⊗ₘ κ)
    (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f (a, b) ∂μ)
have rw : Eq.{u_8 + 1} (α := E)
  (@integral _ _ _ _ mα ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) fun (x : α) ↦
    @integral _ _ _ _ mβ (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x))
      fun (y : β) ↦ f (x, y))
  (∫ (a : α), @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ f (a, b) ∂μ)
Tactic: rw [Measure.compProd, ProbabilityTheory.integral_compProd hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
E : Type u_8
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ Eq.{u_8 + 1} (α := E) (∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ)
    (∫ (a : α) in s, @integral _ _ _ _ mβ (restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ f (a, b) ∂μ)
have rw : Eq.{u_8 + 1} (α := E)
  (@integral _ _ _ _ mα (restrict ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) s) fun (x : α) ↦
    @integral _ _ _ _ mβ
      (restrict (((prodMkLeft Unit κ : Kernel.{u_5, u_6} (Unit × α) β) : (a : Unit × α) → Measure β) ((), x)) t)
      fun (y : β) ↦ f (x, y))
  (∫ (a : α) in s, @integral _ _ _ _ mβ (restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ f (a, b) ∂μ)
Tactic: rw [Measure.compProd, ProbabilityTheory.setIntegral_compProd hs ht hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst_1 : SFinite μ
inst_2 : IsSFiniteKernel κ
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ Integrable (ε := E) (fun (p : α × β) ↦ f p.2) (μ ⊗ₘ κ) ↔ @Integrable _ _ _ _ mβ f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have rw : AEStronglyMeasurable (m₀ := mβ) f (map Prod.snd (μ ⊗ₘ κ))
Tactic: rw [← Measure.snd_compProd, Measure.snd, integrable_map_measure _ measurable_snd.aemeasurable,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst_1 : SFinite μ
inst_2 : IsSFiniteKernel κ
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ AEStronglyMeasurable (m₀ := mβ) f (map Prod.snd (μ ⊗ₘ κ))
have rwa : AEStronglyMeasurable f (μ ⊗ₘ κ).snd
Tactic: rwa [← Measure.snd, Measure.snd_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst : IsSFiniteKernel η
κ : Kernel X Y
inst_1 : IsSFiniteKernel κ
⊢ η ∘ₖ κ = (κ ⊗ₖ prodMkLeft X η).snd
have h : ∀ (a : X) (s : Set Z) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ ⊗ₖ prodMkLeft X η).snd : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.KernelLemmas (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
η : Kernel Y Z
inst : IsSFiniteKernel η
κ : Kernel X Y
inst_1 : IsSFiniteKernel κ
a : X
s : Set Z
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ ⊗ₖ prodMkLeft X η).snd : (a : X) → Measure Z) a : Measure Z) : (a : Set Z) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : Y), (((η : (a : Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞) s ∂(κ : (a : X) → Measure Y) a =
  ∫⁻ (b : Y),
    (((prodMkLeft X η : (a : X × Y) → Measure Z) (a, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
      (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : X) → Measure Y) a
Tactic: rw [comp_apply' _ _ _ hs, snd_apply' _ _ hs, compProd_apply (measurable_snd hs)]