-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
_ :
  HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a
_₁ :
  ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a
_₂ :
  ∫⁻ (b : β),
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a
_₃ :
  ∫⁻ (x : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a =
    (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ
⊢ HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) ≤
    0
have _₄ : Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
Tactic: calc
    _ = ∫⁻ b in t, 1 ∂κ a - ∫⁻ b in t, (η b) s ∂κ a := by
      rw [setLIntegral_one]
    _ = ∫⁻ b in t, 1 - (η b) s ∂κ a := by
      rw [lintegral_sub]
      · exact η.measurable_coe hs
      · exact ne_top_of_le_ne_top (by simp) integral_le_kernel
      · refine ae_of_all _ fun b ↦ ?_
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
    _ ≤ ∫⁻ b, 1 - (η b) s ∂κ a := setLIntegral_le_lintegral _ _
    _ = ∫⁻ x, (η x) sᶜ ∂κ a := by
        congr with x
        rw [measure_compl hs (by simp)]
        simp
    _ = (η ∘ₖ κ) a sᶜ := by
        rw [η.comp_apply' _ _ hs.compl]
    _ = 0 := by
      rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]