import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Mathlib.MeasureTheory.Measure.Map
import Mathlib.MeasureTheory.Order.Lattice

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

set_option quotPrecheck false

-- Namespace stubs (so later `open`s resolve).
namespace MeasurableSpace
end MeasurableSpace
namespace MeasureTheory
end MeasureTheory
namespace Finset
end Finset

-- ═══ ForMathlib.MeasureTheory.MeasurableSpace.Sigma ═══
section
open MeasurableSpace MeasureTheory
variable {α γ : Type*} {β : α → Type*} [∀ a, MeasurableSpace (β a)] [MeasurableSpace γ]

/-- `x ↦ ⟨n x, f (n x) x⟩` is measurable when the index `n x` ranges over a countable type with
measurable singletons and each `f i` is measurable. -/
@[fun_prop]
lemma Measurable.sigmaMk [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α]
    {n : γ → α} (hn : Measurable n) {f : (a : α) → γ → β a} (hf : ∀ a, Measurable (f a)) :
    Measurable fun x ↦ (⟨n x, f (n x) x⟩ : Σ a, β a) := sorry

end

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