-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma comap_prod_swap (κ : Kernel α β) (η : Kernel γ δ) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    comap (prodMkRight α η ×ₖ prodMkLeft γ κ) Prod.swap measurable_swap
      = map (prodMkRight γ κ ×ₖ prodMkLeft α η) Prod.swap

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => f a.swap

Tactic:
swap

Result:
case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => f a.swap

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂κ x.1 ∂η x.2 = ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂η x.2 ∂κ x.1

Tactic:
refine (lintegral_lintegral_swap ?_).symm

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (Function.uncurry fun c b => f (b, c)) ((κ x.1).prod (η x.2))

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∀ (a : α × γ) (f : δ × β → ℝ≥0∞),
    Measurable f →
      ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯) a =
        ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap) a

Tactic:
intro x f hf

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯) x =
    ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap) x

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

Tactic:
simp only [prodMkRight_apply, Prod.fst_swap, Prod.swap_prod_mk, lintegral_prodMkLeft,
  Prod.snd_swap]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂κ x.1 ∂η x.2 = ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂η x.2 ∂κ x.1

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯) x =
    ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap) x

Tactic:
rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf,
  lintegral_prod]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => f a.swap

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ (prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ = (prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap

Tactic:
rw [ext_fun_iff]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∀ (a : α × γ) (f : δ × β → ℝ≥0∞),
    Measurable f →
      ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯) a =
        ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap) a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (Function.uncurry fun c b => f (b, c)) ((κ x.1).prod (η x.2))

Tactic:
fun_prop

Result:
no goals

Proof state:
case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => f a.swap

Tactic:
fun_prop

Result:
no goals