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 : β × γ → E
hE : CompleteSpace E
pos :
  ∀ (c : E) ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞)
          ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
          (∞ : ℝ≥0∞) →
        Eq.{u_4 + 1} (α := E)
          (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
            s.indicator (fun (x : β × γ) ↦ c) z)
          (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
            @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
              s.indicator (fun (x : β × γ) ↦ c) (x, y))
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
    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))
have pos₁ : ∀ ⦃f g : β × γ → E⦄,
  Disjoint (support f) (support g) →
    @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
      @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
        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)) →
          Eq.{u_4 + 1} (α := E)
              (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
                g z)
              (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
                @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)) →
            Eq.{u_4 + 1} (α := E)
              (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
                (f + g) z)
              (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
                @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y))
Tactic: apply Integrable.induction
-- 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
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
      s.indicator (fun (x : β × γ) ↦ c) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
        s.indicator (fun (x : β × γ) ↦ c) (x, y))
have pos : ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) • c =
  HSMul.hSMul (α := ℝ)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)))
    c
Tactic: simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
      integral_indicator (measurable_prodMk_left hs), MeasureTheory.setIntegral_const,
      integral_smul_const, measureReal_def]
-- 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
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) • c =
    HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)))
      c
have pos : ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
  @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
Tactic: congr 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
have pos : ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
  (∫⁻ (a_1 : β),
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
Tactic: rw [integral_toReal]
-- 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
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
pos :
  ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    (∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
have pos₁ : AEMeasurable (β := ℝ≥0∞) (_m := mβ)
  (fun (x : β) ↦ (((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
  ((κ : (a : α) → Measure β) a)
Tactic: rw [integral_toReal]
-- 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
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
pos :
  ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    (∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
pos₁ :
  AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (x : β) ↦ (((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
have pos₂ : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: rw [integral_toReal]
-- 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
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    (∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
have pos : (∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal =
  (∫⁻ (a_1 : β),
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
Tactic: rw [Kernel.compProd_apply hs]
-- 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
h : Disjoint (support f) (support g)
i_f : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
i_g : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (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))
hg :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ (f + g) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y))
have pos : HAdd.hAdd (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (a : β × γ) ↦ f a)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (a : β × γ) ↦ g a) =
  @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y)
Tactic: simp_rw [integral_add' i_f i_g, Kernel.integral_integral_add' 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
h : Disjoint (support f) (support g)
i_f : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
i_g : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (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))
hg :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
pos :
  HAdd.hAdd (α := E)
      (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (a : β × γ) ↦ f a)
      (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (a : β × γ) ↦ g a) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ (f + g) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y))
have pos₁ : HAdd.hAdd (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (a : β × γ) ↦ f a)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (a : β × γ) ↦ g a) =
  HAdd.hAdd (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
Tactic: simp_rw [integral_add' i_f i_g, Kernel.integral_integral_add' 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 α β
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 : @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))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
have h : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
  (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (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 α β
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 :
  Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
have h₁ : Eq.{u_4 + 1} (α := E)
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
  (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, 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 α β
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 : @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))
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
have h : 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)
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 α β
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 : @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))
⊢ 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 : β),
  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
Tactic: filter_upwards [ae_ae_of_ae_compProd hfg] with x hfgx using
        integral_congr_ae (ae_eq_symm hfgx)