-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
empty :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ∅)
basic :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
compl :
  ∀ (t : Set (α × β)) (htm : MeasurableSet t)
    (iht :
      Measurable (β := ℝ≥0∞) fun (a : α) ↦
        (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' tᶜ)
iUnion :
  ∀ (f : ℕ → Set (α × β)) (h_disj : Pairwise (Disjoint on f)) (hf_meas : ∀ (i : ℕ), MeasurableSet (f i))
    (hf :
      ∀ (i : ℕ),
        Measurable (β := ℝ≥0∞) fun (a : α) ↦
          (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
induction t, ht
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp only [preimage_empty, measure_empty, measurable_const]
  | basic t ht =>
    simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
    obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht
    classical
    simp_rw [mk_preimage_prod_right_eq_if]
    have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
      ext1 a
      split_ifs
      exacts [rfl, measure_empty]
    rw [h_eq_ite]
    exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const
  | compl t htm iht =>
    have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' tᶜ = Set.univ \ Prod.mk a ⁻¹' t := by
      intro a
      ext1 b
      simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]
    simp_rw [h_eq_sdiff]
    have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) =
        fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) := by
      ext1 a
      rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
      · exact (measurable_prodMk_left htm).nullMeasurableSet
      · exact measure_ne_top _ _
    rw [this]
    exact Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht
  | iUnion f h_disj hf_meas hf =>
    have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)
    simpa only [this] using Measurable.tsum hf

Premises used: Compl.compl, Set.mem_image2, Set.mk_preimage_prod_right_eq_if, MeasureTheory.measure_empty, Set.mem_setOf_eq, Set.preimage_empty, measurable_const, Set.iUnion, rfl