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
g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))
⊢ 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)
have simp_rw : Tendsto (β := ℝ≥0∞)
  (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      enorm.{u_4} (E := E)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
          (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
  (𝓝 g) (𝓝 0)
Tactic: simp_rw [← lintegral_fn_integral_sub_comp (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn 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))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
have refine_1 : Tendsto (β := ℝ≥0∞)
  (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
              y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a)
  (𝓝 g) (𝓝 0)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le
    (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a)
    tendsto_const_nhds ?_ (fun _ ↦ zero_le) ?_
-- 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))
refine_1 :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        ∫⁻ (y : γ),
          ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
                y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
have refine_2 : LE.le (α := ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)) → ℝ≥0∞)
  (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      enorm.{u_4} (E := E)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
          (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
  fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
  ∫⁻ (x : β),
    ∫⁻ (y : γ),
      ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
          (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
            y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le
    (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a)
    tendsto_const_nhds ?_ (fun _ ↦ zero_le) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        ∫⁻ (y : γ),
          ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
                y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
have this : ∀ (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))),
  Measurable (β := ℝ≥0∞) fun (z : γ) ↦
    ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z -
        (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z‖ₑ
Tactic: have (i : γ →₁[(η ∘ₖ κ) a] E) : Measurable fun z ↦ ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))
this :
  ∀ (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))),
    Measurable (β := ℝ≥0∞) fun (z : γ) ↦
      ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z -
          (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z‖ₑ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        ∫⁻ (y : γ),
          ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
                y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
have refine_1 : Tendsto (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
Tactic: simp_rw [← lintegral_comp _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
-- 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},
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      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)
have pos : ∀ {f : γ → E} (hE : CompleteSpace E),
  @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
    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)
Tactic: by_cases hE : CompleteSpace E
-- 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
pos :
  ∀ {f : γ → E} (hE : CompleteSpace E),
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      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)
⊢ ∀ {f : γ → E},
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      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)
have neg : ∀ {f : γ → E} (hE : ¬CompleteSpace E),
  @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
    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)
Tactic: by_cases hE : CompleteSpace E
-- 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
hE : CompleteSpace E
⊢ @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
    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)
have 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 _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ s.indicator (fun (x : γ) ↦ c) z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ s.indicator (fun (x : γ) ↦ c) 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 α β
η : Kernel β γ
inst_1 : 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 _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ s.indicator (fun (x : γ) ↦ c) z)
          (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
            @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ s.indicator (fun (x : γ) ↦ c) y)
⊢ @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
    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)
have pos₁ : ∀ ⦃f g : γ → E⦄,
  Disjoint (support f) (support g) →
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a) →
        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) →
            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)
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 α β
η : Kernel β γ
inst_1 : 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 _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ s.indicator (fun (x : γ) ↦ c) z)
          (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
            @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ s.indicator (fun (x : γ) ↦ c) y)
pos₁ :
  ∀ ⦃f g : γ → E⦄,
    Disjoint (support f) (support g) →
      @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
        @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a) →
          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) →
              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)
⊢ @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
    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)
have pos₂ : IsClosed (X := ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)))
  {f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a)) |
    Eq.{u_4 + 1} (α := E)
      (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦
        (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) z)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ s.indicator (fun (x : γ) ↦ c) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ s.indicator (fun (x : γ) ↦ c) 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s))
    c
Tactic: simp_rw [integral_indicator 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
Tactic: 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 β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
have pos : AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
  ((κ : (a : α) → Measure β) a)
Tactic: rw [integral_toReal, Kernel.comp_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
have pos₁ : ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [integral_toReal, Kernel.comp_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 α β
η : 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)
⊢ 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 (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
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
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
⊢ 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 (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]