/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.Probability.Kernel.Invariance
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

open MeasureTheory ProbabilityTheory
open scoped ENNReal

example {α : Type*} [MeasurableSpace α]
    [Countable α] [MeasurableSingletonClass α] (κ : Kernel α α) (μ : Measure α)
    (h : ∀ x y, μ {x} * κ x {y} = μ {y} * κ y {x}) :
    Kernel.IsReversible κ μ := by
  intro A B _ _
  have hm (ν : Measure α) (s : Set α) : ν s = ∑' y : s, ν {(y : α)} := by
    simpa using (lintegral_countable (μ := ν) (fun _ => 1) (Set.to_countable s))
  rw [lintegral_countable _ (Set.to_countable A),
    lintegral_countable _ (Set.to_countable B)]
  conv_lhs => enter [1, x]; rw [hm (κ x) B, ← ENNReal.tsum_mul_right]
  conv_rhs => enter [1, y]; rw [hm (κ y) A, ← ENNReal.tsum_mul_right]
  rw [ENNReal.tsum_comm]
  apply tsum_congr
  intro y
  apply tsum_congr
  intro x
  simpa only [mul_comm] using h (x : α) (y : α)