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 η
f : β × γ → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b)) fun (a_1 : β) ↦
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (a_1, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, a_1)).toReal
have h : ∀ (x : β) (hx : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞),
  ∫⁻ (c : γ), ‖f (x, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) =
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)).toReal
Tactic: filter_upwards [h2f] 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
x : β
hx : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
⊢ ∫⁻ (c : γ), ‖f (x, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) =
    ENNReal.ofReal (∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)).toReal
have h : ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ≠ ∞
Tactic: rw [ofReal_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 η
f : β × γ → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : β), ∀ᵐ (y : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ‖f (b, c)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a < ∞
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) < ∞
have refine : Measurable (β := ℝ≥0∞) fun (x : β) ↦ ∫⁻ (a : γ), ‖f (x, a)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x)
Tactic: refine ae_lt_top ?_ h2f.ne
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @HasFiniteIntegral _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)
have rw : (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x))) ∧
    @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
      ((κ : (a : α) → Measure β) a) ↔
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
    @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
      ((κ : (a : α) → Measure β) a)
Tactic: rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
    hasFiniteIntegral_compProd_iff h1f.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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
          ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)
have h₁ : (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
      ((η : (a : α × β) → Measure γ) (a, x))) ↔
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
Tactic: apply and_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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h₁ :
  (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x))) ↔
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
          ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
        ((κ : (a : α) → Measure β) a) ↔
    (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))) ∧
      @HasFiniteIntegral _ ℝ _ mβ
        (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
        ((κ : (a : α) → Measure β) a)
have h₂ : @HasFiniteIntegral _ ℝ _ mβ
    (fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
    ((κ : (a : α) → Measure β) a) ↔
  @HasFiniteIntegral _ ℝ _ mβ
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
    ((κ : (a : α) → Measure β) a)
Tactic: apply and_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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x))) ↔
    ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
have h₁ : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
      ((η : (a : α × β) → Measure γ) (a, x)) ↔
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
Tactic: apply eventually_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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x)) ↔
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (b : β) ↦
                ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                  AEStronglyMeasurable.mk f h1f (b, c) = f (b, c))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
                    ((η : (a : α × β) → Measure γ) (a, x)) ↔
                  @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y))
                    ((η : (a : α × β) → Measure γ) (a, x)))
              x}
          x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                    AEStronglyMeasurable.mk f h1f (b, c) = f (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
                      ((η : (a : α × β) → Measure γ) (a, x)) ↔
                    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y))
                      ((η : (a : α × β) → Measure γ) (a, x)))
                x}
            x}
      a_1
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (x, y))
        ((η : (a : α × β) → Measure γ) (a, x)) ↔
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ),
      AEStronglyMeasurable.mk f h1f (a_1, c) = f (a_1, c)) →
    (@HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ AEStronglyMeasurable.mk f h1f (a_1, y))
        ((η : (a : α × β) → Measure γ) (a, a_1)) ↔
      @HasFiniteIntegral.{u_3, u_4} _ E _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1)))
Tactic: filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
      ((κ : (a : α) → Measure β) a) ↔
    @HasFiniteIntegral _ ℝ _ mβ
      (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖)
      ((κ : (a : α) → Measure β) a)
have h₂ : (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
  (fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
  fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖
Tactic: apply 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (b : β) ↦
                ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                  AEStronglyMeasurable.mk f h1f (b, c) = f (b, c))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq (α := ℝ)
                  ((fun (x : β) ↦
                      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
                          ‖AEStronglyMeasurable.mk f h1f (x, y)‖ :
                        ℝ))
                    x)
                  ((fun (x : β) ↦
                      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖ : ℝ))
                    x))
              x}
          x}
    a_1
Tactic: filter_upwards [ae_ae_of_ae_compProd h1f.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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                    AEStronglyMeasurable.mk f h1f (b, c) = f (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
                            ‖AEStronglyMeasurable.mk f h1f (x, y)‖ :
                          ℝ))
                      x)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖ : ℝ))
                      x))
                x}
            x}
      a_1
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖AEStronglyMeasurable.mk f h1f (x, y)‖)
    fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ ‖f (x, y)‖
have h₁ : ∀ (a_1 : β),
  (∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ),
      AEStronglyMeasurable.mk f h1f (a_1, c) = f (a_1, c)) →
    Eq (α := ℝ)
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
        ‖AEStronglyMeasurable.mk f h1f (a_1, y)‖)
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ ‖f (a_1, y)‖)
Tactic: filter_upwards [ae_ae_of_ae_compProd h1f.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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))))
have refine : EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
  (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
  fun (x : β) ↦
  F
    (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)))
    fun (x : β) ↦
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))
have h : ∀ (a_1 : β)
  (h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1)))
  (h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))),
  F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) + g (a_1, y)) =
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))
Tactic: filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] 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 α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))))
have refine : EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
  (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
  fun (x : β) ↦
  F
    (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))
Tactic: refine integral_congr_ae ?_