import Mathlib.MeasureTheory.Order.Lattice
import Lean.Elab.Tactic.Location
import Lean.Meta.DecLevel
import Lean.Meta.Transform
import Lean.Util.Recognizers
import Mathlib.Probability.Kernel.Composition.Prod
import Lean.Meta.Tactic.Replace
import Lean.Meta.Tactic.Rewrite

/-! # Standalone extraction for `EqLift`
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

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

-- ═══ Tactic.EqLift.Tactic.Lift ═══
section
public meta section
open Lean Elab Tactic Meta Parser.Tactic

/-- Transforms an equality expression by lifting both sides to a common universe level.

The tactic supports location specifiers like `rw` or `simp`:
* `lift_eq` — applies to the goal
* `lift_eq at h` — applies to hypothesis `h`
* `lift_eq at h₁ h₂` — applies to multiple hypotheses
* `lift_eq at h ⊢` — applies to hypothesis `h` and the goal
* `lift_eq at *` — applies to all hypotheses and the goal
-/
syntax (name := EqLift) "lift_eq" (ppSpace location)? : tactic

end
end