-- 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)
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)}
⊢ @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⦄,
  f =ᶠ[ae (F := Measure γ) ((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ)] g →
    @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) →
        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)
Tactic: apply Integrable.induction