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 β γ
f : γ → E
hf : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ @HasFiniteIntegral _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)
have rw : (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x)) ∧
    @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
      ((κ : (a : α) → Measure β) a) ↔
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β), @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
    @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
      ((κ : (a : α) → Measure β) a)
Tactic: rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]
-- 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 : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)
have refine_1 : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
    @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)
Tactic: refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)
-- 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 : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
refine_1 :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)) ∧
      @HasFiniteIntegral _ ℝ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
        ((κ : (a : α) → Measure β) a)
have refine_2 : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
  (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
  fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖
Tactic: refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)
-- 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 : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), AEStronglyMeasurable.mk f hf z = f z)
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
                  @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x))
              x}
          x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      hasFiniteIntegral_congr 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 : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (y : β) ↦
                  ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), AEStronglyMeasurable.mk f hf z = f z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
                    @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x))
                x}
            x}
      a_1
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) x) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) x)
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), AEStronglyMeasurable.mk f hf z = f z) →
    (@HasFiniteIntegral _ _ _ mγ (AEStronglyMeasurable.mk f hf) ((η : (a : β) → Measure γ) a_1) ↔
      @HasFiniteIntegral _ _ _ mγ f ((η : (a : β) → Measure γ) a_1))
Tactic: filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      hasFiniteIntegral_congr 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 : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (y : β) ↦ ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), AEStronglyMeasurable.mk f hf z = f z)
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq (α := ℝ)
                  ((fun (x : β) ↦
                      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
                          ‖AEStronglyMeasurable.mk f hf y‖ :
                        ℝ))
                    x)
                  ((fun (x : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖ : ℝ)) x))
              x}
          x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp 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 : AEStronglyMeasurable (m₀ := mγ) f ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (y : β) ↦
                  ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), AEStronglyMeasurable.mk f hf z = f z)
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
                            ‖AEStronglyMeasurable.mk f hf y‖ :
                          ℝ))
                      x)
                    ((fun (x : β) ↦ (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖ : ℝ)) x))
                x}
            x}
      a_1
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a_1 : Measure γ), AEStronglyMeasurable.mk f hf z = f z) →
    Eq (α := ℝ) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f hf y‖)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ ‖f y‖)
Tactic: filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
⊢ @Integrable _ _ _ _ mβ f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ
have rw : (∀ᵐ (y : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
      @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) y)) ∧
    @Integrable ℝ _ _ _ mα (fun (y : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (z : β) ↦ ‖f z‖)
      ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
  (∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)) ∧
    Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ
Tactic: rw [Measure.comp_eq_comp_const_apply, ProbabilityTheory.integrable_comp_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable (m₀ := mβ) f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
rw :
  (∀ᵐ (y : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
        @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) y)) ∧
      @Integrable ℝ _ _ _ mα (fun (y : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) y) fun (z : β) ↦ ‖f z‖)
        ((Kernel.const Unit μ : (a : Unit) → Measure α) ()) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ
⊢ @Integrable _ _ _ _ mβ f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ↔
    (∀ᵐ (x : α) ∂μ, @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ ‖f y‖) μ
have hf₁ : AEStronglyMeasurable (m₀ := mβ) f ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) ())
Tactic: rw [Measure.comp_eq_comp_const_apply, ProbabilityTheory.integrable_comp_iff]
-- 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
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)))
have refine : EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
  (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y)) fun (x : β) ↦
  F
    (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
Tactic: refine 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
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y)) fun (x : β) ↦
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
have h : ∀ (a : β) (h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a))
  (h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a)),
  F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y + g y) =
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y))
Tactic: filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
-- 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
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)))
have refine : EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
  (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
  F
    (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
Tactic: refine 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
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
have h : ∀ (a : β) (h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a))
  (h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a)),
  F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y - g y) =
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y))
Tactic: filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
-- 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 g : γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ ∫⁻ (x : β),
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)) ∂(κ : (a : α) → Measure β) a
have refine : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
  (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
  F
    (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
Tactic: refine 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 β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
have h : ∀ (a : β) (h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a))
  (h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a)),
  F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y - g y) =
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y))
Tactic: filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
-- 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
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
        (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y
have refine : ∀ (g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))),
  ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
    g
Tactic: refine continuous_iff_continuousAt.2 fun g ↦ ?_
-- 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
g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))
⊢ ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
    g
have refine : Tendsto (β := ℝ≥0∞)
  (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      ‖HSub.hSub (α := E)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)‖ₑ ∂(κ : (a : α) → Measure β) a)
  (𝓝 g) (𝓝 0)
Tactic: refine tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp.aestronglyMeasurable
      (Eventually.of_forall fun h ↦ (L1.integrable_coeFn h).integral_comp) ?_