-- 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))
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))
pos₂ :
  IsClosed (X := ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)))
    {f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) |
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
          (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (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⦄,
  f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g →
    @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)) →
        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))
Tactic: apply Integrable.induction