import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Probability.Kernel.Composition.Prod
import Mathlib.Probability.Kernel.Composition.CompProd
import Mathlib.MeasureTheory.MeasurableSpace.Embedding

/-! # Standalone extraction for `getTypesFromMeasurableEquiv`
Definitions are copied verbatim; theorem proofs are replaced by `sorry`.
Auto-generated by Referee. -/

set_option quotPrecheck false

-- Namespace stubs (so later `open`s resolve).
namespace Finset
end Finset
namespace Lean
end Lean
namespace Lean.Meta
end Lean.Meta
namespace ProbabilityTheory
end ProbabilityTheory

-- ═══ ForMathlib.MeasureTheory.Order.Lattice ═══
section
open Finset
variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α]
attribute [to_dual existing] MeasurableInf₂
end

-- ═══ Tactic.EqLift.Tactic.Kernel.Utils ═══
section
public meta section
open Lean Meta ProbabilityTheory Elab Term

/-- Get departure and target types from a `MeasurableEquiv` expression. -/
def getTypesFromMeasurableEquiv (e : Expr) : MetaM (Expr × Expr) := do
  let equivT ← (whnf (← inferType e))
  match equivT.getAppFn with
  | Expr.const ``MeasurableEquiv _ =>
    let args := equivT.getAppArgs
    return (args[0]!, args[1]!)
  | _ => throwError "Expected a MeasurableEquiv, got: {e}."

end
end