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

/-! # Standalone extraction for `measurable_sigma_of_measurable_comp_mk`
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 γ]

/-- A function on a sigma type is measurable if all its restrictions to the fibers are. -/
lemma measurable_sigma_of_measurable_comp_mk {f : (Σ a, β a) → γ}
    (h : ∀ a, Measurable (f ∘ Sigma.mk a)) : Measurable f := sorry

end

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