Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in s, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in s, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ s hs

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : α × β) in ∅, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in ∅, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∀ t ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t},
    ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∀ (t : Set (α × β)),
    MeasurableSet t →
      ∫⁻ (x : α × β) in t, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ →
        ∫⁻ (x : α × β) in tᶜ, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in tᶜ, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∀ (f : ℕ → Set (α × β)),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ),
            ∫⁻ (x : α × β) in f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
              ∫⁻ (x : α × β) in f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ) →
          ∫⁻ (x : α × β) in ⋃ i, f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
            ∫⁻ (x : α × β) in ⋃ i, f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ