چرا مسئله‌ها سخت‌اند

-- LeanTest/HardProblems/InformationOrder.lean
/-- States are indistinguishable under an observation map when they produce
the same report. -/
def Indist {S : Type u} {O : Type v} (observe : S → O) (x y : S) : Prop :=
  observe x = observe y

-- LeanTest/HardProblems/InformationOrder.lean
/-- Equality of reports induces an equivalence relation on states. -/
theorem indist_equivalence {S : Type u} {O : Type v} (observe : S → O) :
    Equivalence (Indist observe) where
  refl _ := rfl
  symm h := h.symm
  trans hxy hyz := hxy.trans hyz

-- LeanTest/HardProblems/InformationOrder.lean
/-- `fine` refines `coarse` when the coarse report is obtained by deterministic
post-processing of the fine report. This orients the existing
`HardProblems.FactorsThrough` relation as an information preorder; it does not
introduce a second notion of factorization. -/
def ExperimentRefines {S : Type u} {F : Type v} {C : Type w}
    (fine : S → F) (coarse : S → C) : Prop :=
  FactorsThrough coarse fine

-- LeanTest/HardProblems/InformationOrder.lean
/-- Every experiment refines itself. -/
theorem experimentRefines_refl {S : Type u} {O : Type v}
    (observe : S → O) : ExperimentRefines observe observe := by
  exact ⟨id, by funext x; rfl⟩

-- LeanTest/HardProblems/InformationOrder.lean
/-- Deterministic experiment refinement is transitive. -/
theorem experimentRefines_trans {S : Type u} {A : Type v} {B : Type w}
    {C : Type z} {first : S → A} {second : S → B} {third : S → C}
    (h₁ : ExperimentRefines first second)
    (h₂ : ExperimentRefines second third) :
    ExperimentRefines first third := by
  rcases h₁ with ⟨post₁, rfl⟩
  rcases h₂ with ⟨post₂, rfl⟩
  exact ⟨post₂ ∘ post₁, by funext x; rfl⟩

-- LeanTest/HardProblems/InformationOrder.lean
/-- Refinement reverses inclusion of indistinguishability classes: equality of
fine reports forces equality of coarse reports. -/
theorem ExperimentRefines.indist {S : Type u} {F : Type v} {C : Type w}
    {fine : S → F} {coarse : S → C}
    (h : ExperimentRefines fine coarse) {x y : S}
    (hxy : Indist fine x y) : Indist coarse x y := by
  exact (show FactorsThrough coarse fine from h).eq_of_eq hxy

-- LeanTest/HardProblems/InformationOrder.lean
/-- Actions acceptable at every state compatible with the current report.
The acceptable-action predicate is part of the task, rather than part of the
observation alone. -/
def RobustActions {S : Type u} {O : Type v} {A : Type w}
    (observe : S → O) (Acceptable : S → A → Prop) (x : S) : Set A :=
  {a | ∀ y, Indist observe x y → Acceptable y a}

-- LeanTest/HardProblems/InformationOrder.lean
/-- A finer experiment weakly enlarges the set of robust acceptable actions.
The result is task-relevant but deterministic: it compares compatibility
classes, not probabilities or average information. -/
theorem ExperimentRefines.robustActions_mono
    {S : Type u} {F : Type v} {C : Type w} {A : Type z}
    {fine : S → F} {coarse : S → C}
    (h : ExperimentRefines fine coarse) (Acceptable : S → A → Prop) (x : S) :
    RobustActions coarse Acceptable x ⊆ RobustActions fine Acceptable x := by
  intro a ha y hxy
  exact ha y (h.indist hxy)

-- LeanTest/HardProblems/InformationOrder.lean
/-- Mutual deterministic factorization gives exactly the same induced
indistinguishability relation. The report types and report values themselves
need not be equal. -/
theorem indist_iff_of_mutual_refinement
    {S : Type u} {O₁ : Type v} {O₂ : Type w}
    {first : S → O₁} {second : S → O₂}
    (h₁₂ : ExperimentRefines first second)
    (h₂₁ : ExperimentRefines second first) (x y : S) :
    Indist first x y ↔ Indist second x y :=
  ⟨h₁₂.indist, h₂₁.indist⟩

-- LeanTest/HardProblems/InformationOrder.lean
/-- Mutual deterministic factorization preserves every robust action set for
every task predicate. -/
theorem robustActions_eq_of_mutual_refinement
    {S : Type u} {O₁ : Type v} {O₂ : Type w} {A : Type z}
    {first : S → O₁} {second : S → O₂}
    (h₁₂ : ExperimentRefines first second)
    (h₂₁ : ExperimentRefines second first)
    (Acceptable : S → A → Prop) (x : S) :
    RobustActions first Acceptable x = RobustActions second Acceptable x := by
  apply Set.Subset.antisymm
  · exact h₂₁.robustActions_mono Acceptable x
  · exact h₁₂.robustActions_mono Acceptable x

-- LeanTest/HardProblems/InformationOrder.lean
/-- A strict finite decision loss. The identity experiment separates the two
Bool states, while the quotient to `Unit` merges them. An action is acceptable
exactly when it names the true state. At state `false`, the fine report permits
the robust action `false`; the coarse report permits no robust action. -/
theorem quotient_strict_decision_loss :
    let fine : Bool → Bool := id
    let coarse : Bool → Unit := fun _ ↦ ()
    let Acceptable : Bool → Bool → Prop := fun state action ↦ state = action
    ExperimentRefines fine coarse ∧
      ¬ Indist fine false true ∧ Indist coarse false true ∧
      RobustActions coarse Acceptable false = ∅ ∧
      RobustActions fine Acceptable false = {false} ∧
      RobustActions coarse Acceptable false ⊂
        RobustActions fine Acceptable false := by
  dsimp
  refine ⟨⟨fun _ ↦ (), rfl⟩, by simp [Indist], by simp [Indist], ?_⟩
  have hCoarse : RobustActions (fun _ : Bool ↦ ())
      (fun state action : Bool ↦ state = action) false = ∅ := by
    ext action
    constructor
    · intro ha
      have hFalse := ha false (by rfl)
      have hTrue := ha true (by rfl)
      simp only [Set.mem_empty_iff_false]
      cases action <;> simp_all
    · simp
  have hFine : RobustActions id
      (fun state action : Bool ↦ state = action) false = {false} := by
    ext action
    simp [RobustActions, Indist]
  refine ⟨hCoarse, hFine, ?_⟩
  rw [hCoarse, hFine]
  exact Set.empty_ssubset.mpr (Set.singleton_nonempty false)

-- LeanTest/HardProblems/SystemsTheory.lean
/-- The statistic-factorization obstruction with an arbitrary statistic
codomain; nothing in the argument uses the real numbers. -/
theorem statistic_based_rule_fails' {Y : Type*} {m : S → Y} (Astar : S → Set A)
    {s s' : S} (hm : m s = m s') (hdisj : Disjoint (Astar s) (Astar s'))
    (α : Y → A) :
    α (m s) ∉ Astar s ∨ α (m s') ∉ Astar s' := by
  by_contra hc
  push Not at hc
  obtain ⟨h1, h2⟩ := hc
  rw [hm] at h1
  exact Set.disjoint_left.mp hdisj h1 h2

-- LeanTest/HardProblems/InformationBudget.lean
/-- An accumulated real-valued quantity with initial upper bound `I₀` and
one-round increment bounded above by `C` is at most `I₀ + n * C` after `n`
rounds.

No nonnegativity hypothesis is needed for this arithmetic statement.  An
information-theoretic application must separately establish that its chosen
quantities and bounds have the intended meaning. -/
theorem accumulated_le_initial_add_rounds_mul
    (accumulated : ℕ → ℝ) (I₀ C : ℝ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ n, accumulated (n + 1) ≤ accumulated n + C) :
    ∀ n, accumulated n ≤ I₀ + (n : ℝ) * C := by
  intro n
  induction n with
  | zero => simpa using hinitial
  | succ n ih =>
      calc
        accumulated (n + 1) ≤ accumulated n + C := hstep n
        _ ≤ (I₀ + (n : ℝ) * C) + C := add_le_add_left ih C
        _ = I₀ + ((n + 1 : ℕ) : ℝ) * C := by
          push_cast
          ring

-- LeanTest/HardProblems/InformationBudget.lean
/-- If reaching the target requires at least `R` units of the accumulated
quantity, and the target has been reached at round `n`, then the required
amount above the initial budget is no larger than `n * C`.

This conclusion is conditional on `hrequired`: the lemma does not prove that a
distortion level really requires `R`, nor that the accumulated scalar is
mutual information. -/
theorem required_excess_le_rounds_mul
    (accumulated : ℕ → ℝ) (I₀ C R : ℝ) (n : ℕ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ k, accumulated (k + 1) ≤ accumulated k + C)
    (hrequired : R ≤ accumulated n) :
    R - I₀ ≤ (n : ℝ) * C := by
  have hbudget :=
    accumulated_le_initial_add_rounds_mul accumulated I₀ C hinitial hstep n
  linarith

-- LeanTest/HardProblems/InformationBudget.lean
/-- With positive per-round capacity, the real-valued required excess divided
by that capacity is a lower bound on the number of rounds.

This is only division of the preceding scalar inequality.  In particular, it
does not identify `R` with a rate-distortion function or `C` with Shannon
capacity. -/
theorem required_excess_div_capacity_le_rounds
    (accumulated : ℕ → ℝ) (I₀ C R : ℝ) (n : ℕ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ k, accumulated (k + 1) ≤ accumulated k + C)
    (hrequired : R ≤ accumulated n) (hC : 0 < C) :
    (R - I₀) / C ≤ (n : ℝ) := by
  apply (div_le_iff₀ hC).2
  exact required_excess_le_rounds_mul accumulated I₀ C R n
    hinitial hstep hrequired

-- LeanTest/HardProblems/InformationBudget.lean
/-- Since rounds are natural numbers, the natural ceiling of the real-valued
ratio is also a lower bound on the round count.

If `R ≤ I₀`, the ratio may be nonpositive and the ceiling is zero; the theorem
then correctly gives only the vacuous lower bound `0 ≤ n`. -/
theorem required_rounds_ceiling_le
    (accumulated : ℕ → ℝ) (I₀ C R : ℝ) (n : ℕ)
    (hinitial : accumulated 0 ≤ I₀)
    (hstep : ∀ k, accumulated (k + 1) ≤ accumulated k + C)
    (hrequired : R ≤ accumulated n) (hC : 0 < C) :
    Nat.ceil ((R - I₀) / C) ≤ n := by
  apply Nat.ceil_le.mpr
  exact required_excess_div_capacity_le_rounds accumulated I₀ C R n
    hinitial hstep hrequired hC

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Algebraic posterior variance for a scalar Gaussian prior of variance `P₀`
after `n` independent measurements with noise variance `R`.

This definition packages the standard conjugate-Gaussian calculation. It does
not itself prove that a physical measurement process is Gaussian, independent,
or correctly modeled. -/
noncomputable def posteriorVariance (P₀ R : ℝ) (n : ℕ) : ℝ :=
  1 / (1 / P₀ + (n : ℝ) / R)

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Positive prior and measurement variances give positive posterior variance. -/
theorem posteriorVariance_pos {P₀ R : ℝ} (hP₀ : 0 < P₀) (hR : 0 < R)
    (n : ℕ) : 0 < posteriorVariance P₀ R n := by
  unfold posteriorVariance
  positivity

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Reaching target variance `D` under the scalar posterior formula requires
at least `R * (1 / D - 1 / P₀)` measurements. The right side is real-valued;
an integer ceiling would be needed for a sharp natural-number statement.

This is an algebraic consequence of the displayed variance formula. It is not
a general Kalman-filter theorem and says nothing about model mismatch, process
noise, correlated measurements, or unobservable state directions. -/
theorem target_accuracy_requires_observations {P₀ R D : ℝ} {n : ℕ}
    (hP₀ : 0 < P₀) (hR : 0 < R) (hD : 0 < D)
    (hacc : posteriorVariance P₀ R n ≤ D) :
    R * (1 / D - 1 / P₀) ≤ (n : ℝ) := by
  have hden : 0 < 1 / P₀ + (n : ℝ) / R := by positivity
  have hcross : 1 ≤ D * (1 / P₀ + (n : ℝ) / R) := by
    exact (div_le_iff₀ hden).mp hacc
  have hprecision : 1 / D ≤ 1 / P₀ + (n : ℝ) / R := by
    apply (div_le_iff₀ hD).2
    nlinarith
  have hremaining : 1 / D - 1 / P₀ ≤ (n : ℝ) / R := by
    linarith
  simpa [mul_comm] using (le_div_iff₀ hR).mp hremaining

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- If the target variance is strictly smaller than the prior variance, the
observation-count lower bound above is strictly positive rather than vacuous. -/
theorem target_accuracy_nontrivial_bound {P₀ R D : ℝ} {n : ℕ}
    (hP₀ : 0 < P₀) (hR : 0 < R) (hD : 0 < D) (hDlt : D < P₀)
    (hacc : posteriorVariance P₀ R n ≤ D) :
    0 < R * (1 / D - 1 / P₀) ∧
      R * (1 / D - 1 / P₀) ≤ (n : ℝ) := by
  constructor
  · exact mul_pos hR (sub_pos.mpr (one_div_lt_one_div_of_lt hD hDlt))
  · exact target_accuracy_requires_observations hP₀ hR hD hacc

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Iterating a scalar robust contraction gives a geometric finite-time bound.
The error need not be generated by any particular observer, but nonnegativity
of `q` is needed to propagate the upper inequality. -/
theorem error_le_geometric_sum (e : ℕ → ℝ) (q d : ℝ)
    (hq : 0 ≤ q) (hstep : ∀ n, e (n + 1) ≤ q * e n + d) (n : ℕ) :
    e n ≤ q ^ n * e 0 + d * ∑ k ∈ Finset.range n, q ^ k := by
  induction n with
  | zero => simp
  | succ n ih =>
      calc
        e (n + 1) ≤ q * e n + d := hstep n
        _ ≤ q * (q ^ n * e 0 + d * ∑ k ∈ Finset.range n, q ^ k) + d :=
          add_le_add (mul_le_mul_of_nonneg_left ih hq) le_rfl
        _ = q ^ (n + 1) * e 0 + d * ∑ k ∈ Finset.range (n + 1), q ^ k := by
          rw [geom_sum_succ]
          ring

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- With a strict contraction, the geometric sum can be written using the
disturbance tube `d / (1 - q)`. This is a finite-time statement, not an
asymptotic optimality claim. -/
theorem error_le_tube_transient (e : ℕ → ℝ) (q d : ℝ)
    (hq0 : 0 ≤ q) (hq1 : q < 1)
    (hstep : ∀ n, e (n + 1) ≤ q * e n + d) (n : ℕ) :
    e n ≤ q ^ n * (e 0 - d / (1 - q)) + d / (1 - q) := by
  have hqne : q ≠ 1 := ne_of_lt hq1
  have hbound := error_le_geometric_sum e q d hq0 hstep n
  rw [geom_sum_eq hqne n] at hbound
  calc
    e n ≤ q ^ n * e 0 + d * ((q ^ n - 1) / (q - 1)) := hbound
    _ = q ^ n * (e 0 - d / (1 - q)) + d / (1 - q) := by
      field_simp [sub_ne_zero.mpr hqne, sub_ne_zero.mpr hqne.symm]
      ring

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- The disturbance tube is forward invariant: if the initial error is below
`d / (1 - q)`, every later error remains below it. The assumption `0 ≤ d`
makes the displayed radius nonnegative; it is not needed merely for the upper
inequality but records its intended error-bound interpretation. -/
theorem error_le_tube (e : ℕ → ℝ) (q d : ℝ)
    (hq0 : 0 ≤ q) (hq1 : q < 1) (hd : 0 ≤ d)
    (hstep : ∀ n, e (n + 1) ≤ q * e n + d)
    (hinit : e 0 ≤ d / (1 - q)) (n : ℕ) :
    0 ≤ d / (1 - q) ∧ e n ≤ d / (1 - q) := by
  constructor
  · exact div_nonneg hd (sub_nonneg.mpr (le_of_lt hq1))
  · have hpow : 0 ≤ q ^ n := pow_nonneg hq0 n
    have htransient := error_le_tube_transient e q d hq0 hq1 hstep n
    have hdiff : e 0 - d / (1 - q) ≤ 0 := sub_nonpos.mpr hinit
    have hnonpos : q ^ n * (e 0 - d / (1 - q)) ≤ 0 :=
      mul_nonpos_of_nonneg_of_nonpos hpow hdiff
    linarith

-- LeanTest/HardProblems/FeedbackBounds.lean
/-- Writing the effective contraction factor as `q₀ + μ` makes the robustness
margin explicit. A certified mismatch `μ` must remain below `1 - q₀`; under
that hypothesis the same finite-time disturbance-tube bound applies.

The result does not say that `μ` is a universal metric on model difference.
An observer analysis must first justify that the actual mismatch contributes
at most `μ` to this scalar one-step estimate. -/
theorem mismatch_le_margin_and_error_bound (e : ℕ → ℝ) (q₀ μ d : ℝ)
    (hq₀ : 0 ≤ q₀) (hμ : 0 ≤ μ) (hmargin : q₀ + μ < 1)
    (hstep : ∀ n, e (n + 1) ≤ (q₀ + μ) * e n + d) (n : ℕ) :
    μ < 1 - q₀ ∧
      e n ≤ (q₀ + μ) ^ n * (e 0 - d / (1 - q₀ - μ)) +
        d / (1 - q₀ - μ) := by
  constructor
  · linarith
  · have hq : 0 ≤ q₀ + μ := add_nonneg hq₀ hμ
    simpa [sub_sub] using
      error_le_tube_transient e (q₀ + μ) d hq hmargin hstep n

-- LeanTest/HardProblems/FaultMargins.lean
/-- A strict deterministic threshold test on a residual. Equality with the
threshold does not raise an alarm. -/
def Alarm (η : ℝ) (residual : E) : Prop :=
  η < ‖residual‖

-- LeanTest/HardProblems/FaultMargins.lean
/-- A residual certified inside the healthy radius cannot cross a threshold
that is at least that radius. This is a pointwise deterministic statement, not
a probabilistic false-alarm guarantee. -/
theorem healthy_residual_not_alarm {healthy : E} {ρ η : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) (hthreshold : ρ ≤ η) :
    ¬ Alarm η healthy := by
  exact not_lt_of_ge (hhealthy.trans hthreshold)

-- LeanTest/HardProblems/FaultMargins.lean
/-- Reverse-triangle geometry for an additive fault: if the fault norm exceeds
the threshold plus the healthy-radius allowance, every admitted healthy
residual forces an alarm. The condition is sufficient, not necessary. -/
theorem alarm_of_fault_norm_gt_threshold_add_radius
    {healthy fault : E} {ρ η : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) (hfault : η + ρ < ‖fault‖) :
    Alarm η (healthy + fault) := by
  have hreverse : ‖fault‖ ≤ ‖healthy + fault‖ + ‖healthy‖ := by
    calc
      ‖fault‖ = ‖(healthy + fault) - healthy‖ := by
        congr 1
        abel
      _ ≤ ‖healthy + fault‖ + ‖healthy‖ := norm_sub_le _ _
  unfold Alarm
  linarith

-- LeanTest/HardProblems/FaultMargins.lean
/-- At the smallest threshold certified from the declared healthy-radius bound
alone, `η = ρ`, the familiar separation condition is
`2 * ρ < ‖fault‖`. It still asserts only guaranteed detection under that
deterministic radius. -/
theorem alarm_of_fault_norm_gt_two_mul_radius
    {healthy fault : E} {ρ : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) (hfault : 2 * ρ < ‖fault‖) :
    Alarm ρ (healthy + fault) := by
  apply alarm_of_fault_norm_gt_threshold_add_radius hhealthy
  simpa [two_mul] using hfault

-- LeanTest/HardProblems/FaultMargins.lean
/-- An additive faulted residual lies in the closed residual ball centered at
its fault signature whenever the healthy component lies inside the declared
radius. -/
theorem faulted_residual_mem_closedBall {healthy fault : E} {ρ : ℝ}
    (hhealthy : ‖healthy‖ ≤ ρ) :
    healthy + fault ∈ Metric.closedBall fault ρ := by
  rw [Metric.mem_closedBall, dist_eq_norm]
  simpa [add_sub_cancel_right]

-- LeanTest/HardProblems/FaultMargins.lean
/-- Closed candidate residual balls of common radius are disjoint when their
fault centers are separated by more than twice that radius. This supplies a
deterministic isolation margin for these two declared candidates; it does not
show that the candidate list is exhaustive or statistically identifiable.
The explicit nonnegativity hypothesis rules out vacuous negative-radius
balls. -/
theorem closedBall_disjoint_of_norm_sub_gt_two_mul_radius
    {fault₁ fault₂ : E} {ρ : ℝ}
    (hρ : 0 ≤ ρ) (hseparated : 2 * ρ < ‖fault₁ - fault₂‖) :
    Disjoint (Metric.closedBall fault₁ ρ) (Metric.closedBall fault₂ ρ) := by
  rw [Set.disjoint_left]
  intro residual hmem₁ hmem₂
  have h₁ : dist fault₁ residual ≤ ρ := by
    simpa [dist_comm] using (Metric.mem_closedBall.mp hmem₁)
  have h₂ : dist residual fault₂ ≤ ρ :=
    Metric.mem_closedBall.mp hmem₂
  have htriangle : dist fault₁ fault₂ ≤ dist fault₁ residual + dist residual fault₂ :=
    dist_triangle _ _ _
  have h₁max : dist fault₁ residual ≤ max ρ 0 :=
    h₁.trans (le_max_left _ _)
  have h₂max : dist residual fault₂ ≤ max ρ 0 :=
    h₂.trans (le_max_left _ _)
  have hcentersMax : ‖fault₁ - fault₂‖ ≤ 2 * max ρ 0 := by
    rw [← dist_eq_norm]
    linarith
  have hcenters : ‖fault₁ - fault₂‖ ≤ 2 * ρ := by
    simpa [max_eq_left hρ] using hcentersMax
  linarith

-- LeanTest/HardProblems/FaultMargins.lean
/-- A scalar recurrence may switch its nonnegative contraction factor at every
step and still obey the constant geometric bound for a declared uniform upper
factor. Nonnegativity of the error is what permits replacing each active factor
by the uniform upper bound.

This extends the constant-factor recurrence in `RobustFeedback`; it does not
establish that a switched observer or plant satisfies the scalar hypotheses. -/
theorem error_le_uniform_geometric_sum
    (e q : ℕ → ℝ) (qMax d : ℝ)
    (hqMax : 0 ≤ qMax)
    (hq : ∀ n, 0 ≤ q n ∧ q n ≤ qMax)
    (he : ∀ n, 0 ≤ e n)
    (hstep : ∀ n, e (n + 1) ≤ q n * e n + d)
    (n : ℕ) :
    e n ≤ qMax ^ n * e 0 + d * ∑ k ∈ Finset.range n, qMax ^ k := by
  apply RobustFeedback.error_le_geometric_sum e qMax d hqMax
  intro k
  calc
    e (k + 1) ≤ q k * e k + d := hstep k
    _ ≤ qMax * e k + d :=
      add_le_add (mul_le_mul_of_nonneg_right (hq k).2 (he k)) le_rfl

-- LeanTest/HardProblems/FaultMargins.lean
/-- Under a strict uniform contraction bound, arbitrary switching obeys the
same closed-form disturbance-tube transient as the constant-factor recurrence.
The theorem gives an upper certificate under uniform scalar hypotheses; it
does not establish those hypotheses for a particular switched system. -/
theorem error_le_uniform_tube_transient
    (e q : ℕ → ℝ) (qMax d : ℝ)
    (hqMax0 : 0 ≤ qMax) (hqMax1 : qMax < 1)
    (hq : ∀ n, 0 ≤ q n ∧ q n ≤ qMax)
    (he : ∀ n, 0 ≤ e n)
    (hstep : ∀ n, e (n + 1) ≤ q n * e n + d)
    (n : ℕ) :
    e n ≤ qMax ^ n * (e 0 - d / (1 - qMax)) + d / (1 - qMax) := by
  apply RobustFeedback.error_le_tube_transient e qMax d hqMax0 hqMax1
  intro k
  calc
    e (k + 1) ≤ q k * e k + d := hstep k
    _ ≤ qMax * e k + d :=
      add_le_add (mul_le_mul_of_nonneg_right (hq k).2 (he k)) le_rfl

-- LeanTest/HardProblems/SystemsTheory.lean
/-- Two models are distinguishable from `s` under the constant action `a₀`
when their observation-history laws differ at some horizon. The type does not
assert that `a₀` is inert; that interpretation is supplied by an application. -/
def PassivelyDistinguishable (M₁ M₂ : POSystem S A O) (a₀ : A) (s : S) : Prop :=
  ∃ n, obsProcess M₁ (fun _ => PMF.pure a₀) n s [] ≠
        obsProcess M₂ (fun _ => PMF.pure a₀) n s []

-- LeanTest/HardProblems/SystemsTheory.lean
/-- Two models are probe distinguishable from `s` when some policy of the
declared function type separates their observation-history laws. -/
def ProbeDistinguishable (M₁ M₂ : POSystem S A O) (s : S) : Prop :=
  ∃ (π : List O → PMF A) (n : ℕ),
    obsProcess M₁ π n s [] ≠ obsProcess M₂ π n s []

-- LeanTest/HardProblems/SystemsTheory.lean
/-- A constant-action policy is a special case of an observation-dependent
policy. -/
theorem passively_imp_probe {M₁ M₂ : POSystem S A O} {a₀ : A} {s : S}
    (h : PassivelyDistinguishable M₁ M₂ a₀ s) : ProbeDistinguishable M₁ M₂ s :=
  let ⟨n, hn⟩ := h
  ⟨fun _ => PMF.pure a₀, n, hn⟩

-- LeanTest/HardProblems/SystemsTheory.lean
/-- There are two Boolean models whose laws agree under the constant action
`false` at every horizon but differ under the constant action `true`. In these
witness models, `false` is inert and `true` changes one model only. -/
theorem exists_probe_only_distinguishable :
    ∃ (M₁ M₂ : POSystem Bool Bool Bool) (s : Bool),
      ¬ PassivelyDistinguishable M₁ M₂ false s ∧ ProbeDistinguishable M₁ M₂ s := by
  refine ⟨flipModel, inertModel, false, ?_, ?_⟩
  · rintro ⟨n, hn⟩
    exact hn (obsProcess_congr_null flipModel inertModel false rfl
      (fun s => by simp [flipModel, inertModel]) n false [])
  · refine ⟨fun _ => PMF.pure true, 2, ?_⟩
    have h₁ : obsProcess flipModel (fun _ => PMF.pure true) 2 false [] =
        PMF.pure [false, true] := by
      simp [obsProcess, flipModel, PMF.pure_bind]
    have h₂ : obsProcess inertModel (fun _ => PMF.pure true) 2 false [] =
        PMF.pure [false, false] := by
      simp [obsProcess, inertModel, PMF.pure_bind]
    rw [h₁, h₂]
    intro hcontra
    have := congrArg (fun p => p [false, true]) hcontra
    simp [PMF.pure_apply] at this

-- LeanTest/HardProblems/Observability.lean
/-- Observational equivalence: no policy of the declared function type
distinguishes the two states at any finite horizon. -/
def ObsEquiv (M : POSystem S A O) (s s' : S) : Prop :=
  ∀ (π : List O → PMF A) (n : ℕ), obsProcess M π n s [] = obsProcess M π n s' []

-- LeanTest/HardProblems/Observability.lean
/-- Observational equivalence is an equivalence relation, as the notation
`≡` silently promises. -/
theorem obsEquiv_equivalence (M : POSystem S A O) : Equivalence (ObsEquiv M) where
  refl _ := fun _ _ => rfl
  symm h := fun π n => (h π n).symm
  trans h₁ h₂ := fun π n => (h₁ π n).trans (h₂ π n)

-- LeanTest/HardProblems/Observability.lean
/-- A necessary metric condition for asymptotic reconstruction: if the same
estimate converges to each of two state trajectories, their mutual distance
converges to zero. To turn this into a detectability theorem, a system-specific
argument must show that observationally indistinguishable trajectories really
feed the same estimate. -/
theorem common_estimate_forces_pairwise_convergence
    {X : Type*} [PseudoMetricSpace X] (x₁ x₂ xhat : ℕ → X)
    (h₁ : Tendsto (fun t => dist (x₁ t) (xhat t)) atTop (𝓝 0))
    (h₂ : Tendsto (fun t => dist (x₂ t) (xhat t)) atTop (𝓝 0)) :
    Tendsto (fun t => dist (x₁ t) (x₂ t)) atTop (𝓝 0) := by
  refine squeeze_zero (fun _ => dist_nonneg) (fun t => dist_triangle _ (xhat t) _) ?_
  have h₂' : Tendsto (fun t => dist (xhat t) (x₂ t)) atTop (𝓝 0) :=
    h₂.congr' (Eventually.of_forall fun t => dist_comm (x₂ t) (xhat t))
  simpa only [zero_add] using h₁.add h₂'

-- LeanTest/HardProblems/Observability.lean
/-- Decision-critical ambiguity: two observationally equivalent states whose
acceptable-action sets `A*_M` are disjoint. -/
def DecisionCritical (M : POSystem S A O) (Astar : S → Set A) (s s' : S) : Prop :=
  ObsEquiv M s s' ∧ Disjoint (Astar s) (Astar s')

-- LeanTest/HardProblems/Observability.lean
/-- An action is robust at `s` when it is acceptable in every state
observationally equivalent to `s`. -/
def RobustAcceptable (M : POSystem S A O) (Astar : S → Set A) (s : S) (a : A) : Prop :=
  ∀ s', ObsEquiv M s s' → a ∈ Astar s'

-- LeanTest/HardProblems/Observability.lean
/-- Robust actions are exactly the intersection of the acceptable sets over
the equivalence class of `s`. -/
theorem robustSet_eq_iInter (M : POSystem S A O) (Astar : S → Set A) (s : S) :
    {a | RobustAcceptable M Astar s a} = ⋂ s' ∈ {s' | ObsEquiv M s s'}, Astar s' := by
  ext a
  simp [RobustAcceptable]

-- LeanTest/HardProblems/Observability.lean
/-- Robust choice is infeasible when no action is acceptable throughout the
observational equivalence class. -/
def RobustlyInfeasible (M : POSystem S A O) (Astar : S → Set A) (s : S) : Prop :=
  ¬ ∃ a, RobustAcceptable M Astar s a

-- LeanTest/HardProblems/Observability.lean
/-- The exact criterion for robust infeasibility is emptiness of the total
intersection of acceptable-action sets over the observational class. Pairwise
disjointness is sufficient but not necessary for this intersection to be empty. -/
theorem robustlyInfeasible_iff_iInter_eq_empty
    (M : POSystem S A O) (Astar : S → Set A) (s : S) :
    RobustlyInfeasible M Astar s ↔
      ⋂ s' ∈ {s' | ObsEquiv M s s'}, Astar s' = ∅ := by
  rw [← robustSet_eq_iInter]
  change (¬ ({a | RobustAcceptable M Astar s a} : Set A).Nonempty) ↔ _
  exact Set.not_nonempty_iff_eq_empty

-- LeanTest/HardProblems/Observability.lean
/-- A disjoint observationally equivalent pair certifies that no robust action
exists at the first state. -/
theorem DecisionCritical.no_robust_action
    {M : POSystem S A O} {Astar : S → Set A} {s s' : S}
    (h : DecisionCritical M Astar s s') :
    ¬∃ a, RobustAcceptable M Astar s a := by
  rintro ⟨a, ha⟩
  have h₁ : a ∈ Astar s := ha s ((obsEquiv_equivalence M).refl s)
  have h₂ : a ∈ Astar s' := ha s' h.1
  exact Set.disjoint_left.mp h.2 h₁ h₂

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Finite-composition reachability: `y` is reachable from `x` by
applying effectors drawn from `G`. -/
inductive Reach (G : Set (X → X)) (x : X) : X → Prop
  | refl : Reach G x x
  | tail : ∀ {y z : X} {g : X → X}, Reach G x y → g ∈ G → z = g y → Reach G x z

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Any admissible trajectory stays inside the reachable set: at each
step some effector in `G` was applied, chosen by an arbitrary policy,
and no choice rule ever escapes the orbit. -/
theorem traj_mem_reach (G : Set (X → X)) (σ : ℕ → X)
    (hstep : ∀ n, ∃ g ∈ G, σ (n + 1) = g (σ n)) (n : ℕ) :
    Reach G (σ 0) (σ n) := by
  induction n with
  | zero => exact Reach.refl
  | succ n ih =>
      obtain ⟨g, hg, heq⟩ := hstep n
      exact Reach.tail ih hg heq

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Pointwise realizability over `G`: from every state, the image under `g` is
already reachable with `G`. The definition supplies neither a uniform generator
word nor a computable dispatcher for the witnessing paths. -/
def Programmed (G : Set (X → X)) (g : X → X) : Prop :=
  ∀ y : X, Reach G y (g y)

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Inserting a pointwise realizable transformation as a primitive leaves every
reachability orbit unchanged. -/
theorem reach_insert_programmed (G : Set (X → X)) {g : X → X}
    (hg : Programmed G g) (x z : X) :
    Reach (insert g G) x z ↔ Reach G x z := by
  constructor
  · intro h
    induction h with
    | refl => exact Reach.refl
    | @tail y z f hy hmem heq ih =>
        rcases hmem with (rfl | hmem)
        · rw [heq]
          exact Reach.trans ih (hg y)
        · exact Reach.tail ih hmem heq
  · intro h
    induction h with
    | refl => exact Reach.refl
    | tail hy hmem heq ih =>
        exact Reach.tail ih (Set.mem_insert_of_mem g hmem) heq

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A transformation outside the prior reachability closure can strictly
enlarge reach in an explicit two-state example. -/
theorem exists_new_effector_enlarges_reach :
    ∃ (G : Set (Bool → Bool)) (g : Bool → Bool) (x z : Bool),
      Reach (insert g G) x z ∧ ¬ Reach G x z := by
  refine ⟨∅, Bool.not, false, true, ?_, ?_⟩
  · exact Reach.tail Reach.refl (Set.mem_insert _ _) rfl
  · intro h
    cases h with
    | tail hy hmem heq => exact hmem.elim

-- LeanTest/HardProblems/Ruggedness.lean
/-- An admissible path in the configuration graph `Adj`, from `x` to `y`,
recorded as its list of visited configurations. -/
structure PathBetween (Adj : X → X → Prop) (x y : X) where
  points : List X
  head_eq : points.head? = some x
  last_eq : points.getLast? = some y
  admissible : points.IsChain Adj

-- LeanTest/HardProblems/Ruggedness.lean
/-- Barrier height from `x` to `y`: the infimum, over admissible paths, of the
deepest dip below `J x` along the path (dips measured in `ℝ≥0∞`, so paths
that never dip contribute `0`). Empty infimum is `⊤`: no path, infinite
barrier. -/
noncomputable def barrier (Adj : X → X → Prop) (J : X → ℝ) (x y : X) : ℝ≥0∞ :=
  ⨅ γ : PathBetween Adj x y, ⨆ z ∈ γ.points, ENNReal.ofReal (J x - J z)

-- LeanTest/HardProblems/Ruggedness.lean
/-- A positive barrier means every admissible route to `y` contains a
configuration strictly worse than the start. No hypothesis here says that `y`
is better than the start or that the dip occurs before first reaching `y`. -/
theorem exists_dip_of_barrier_pos {Adj : X → X → Prop} {J : X → ℝ} {x y : X}
    (h : 0 < barrier Adj J x y) (γ : PathBetween Adj x y) :
    ∃ z ∈ γ.points, J z < J x := by
  have hγ : 0 < ⨆ z ∈ γ.points, ENNReal.ofReal (J x - J z) :=
    lt_of_lt_of_le h (iInf_le _ γ)
  obtain ⟨z, hz⟩ := lt_iSup_iff.mp hγ
  obtain ⟨hmem, hpos⟩ := lt_iSup_iff.mp hz
  refine ⟨z, hmem, ?_⟩
  have := ENNReal.ofReal_pos.mp hpos
  linarith

-- LeanTest/HardProblems/Ruggedness.lean
/-- No admissible path at all makes the barrier infinite. -/
theorem barrier_eq_top_of_no_path {Adj : X → X → Prop} {J : X → ℝ} {x y : X}
    (h : IsEmpty (PathBetween Adj x y)) :
    barrier Adj J x y = ⊤ :=
  iInf_of_empty _

-- LeanTest/HardProblems/Ruggedness.lean
/-- If some admissible path never dips below the start value, the barrier
vanishes: the converse companion to `exists_dip_of_barrier_pos`. (Also
proved independently by Harmonic's Aristotle prover; see `aristotle/`.) -/
theorem barrier_eq_zero_of_monotone_path {Adj : X → X → Prop} {J : X → ℝ}
    {x y : X} (γ : PathBetween Adj x y) (hγ : ∀ z ∈ γ.points, J x ≤ J z) :
    barrier Adj J x y = 0 := by
  refine le_antisymm ?_ zero_le
  refine le_trans (iInf_le _ γ) ?_
  refine iSup_le fun z => iSup_le fun hz => ?_
  simp [ENNReal.ofReal_eq_zero, hγ z hz]

-- LeanTest/HardProblems/Ruggedness.lean
/-- The barrier sits strictly below `d` exactly when some admissible path
keeps every dip strictly below `d`. The backward direction uses the
finiteness of a path's point list: finitely many quantities each below `d`
have supremum below `d`. -/
theorem barrier_lt_iff {Adj : X → X → Prop} {J : X → ℝ} {x y : X}
    {d : ℝ≥0∞} :
    barrier Adj J x y < d ↔
      ∃ γ : PathBetween Adj x y, ∀ z ∈ γ.points,
        ENNReal.ofReal (J x - J z) < d := by
  constructor
  · intro h
    obtain ⟨γ, hγ⟩ := iInf_lt_iff.1 h
    exact ⟨γ, fun z hz =>
      lt_of_le_of_lt (le_biSup (fun z => ENNReal.ofReal (J x - J z)) hz) hγ⟩
  · rintro ⟨γ, hγ⟩
    have hx : x ∈ γ.points := List.mem_of_mem_head? γ.head_eq
    have hd : 0 < d := lt_of_le_of_lt zero_le (hγ x hx)
    exact lt_of_le_of_lt (iInf_le _ γ) (biSup_list_lt _ hd γ.points hγ)

-- LeanTest/HardProblems/Ruggedness.lean
/-- Reachability form: shortcuts backed by mere admissible paths do not
change what is reachable. -/
theorem pathBetween_shortcut_nonempty_iff {Adj S : X → X → Prop}
    (hback : ∀ u w, S u w → Nonempty (PathBetween Adj u w)) (x y : X) :
    Nonempty (PathBetween (fun a b => Adj a b ∨ S a b) x y) ↔
      Nonempty (PathBetween Adj x y) := by
  constructor
  · rintro ⟨γ⟩
    have hback' : ∀ u w, S u w → ∃ δ : PathBetween Adj u w,
        ∀ z ∈ δ.points, min ((fun _ : X => (0 : ℝ)) u) ((fun _ : X => (0 : ℝ)) w)
          ≤ (fun _ : X => (0 : ℝ)) z := by
      intro u w h
      obtain ⟨δ⟩ := hback u w h
      exact ⟨δ, fun _ _ => by simp⟩
    obtain ⟨γ', -⟩ := exists_splice hback' γ
    exact ⟨γ'⟩
  · rintro ⟨γ⟩
    exact ⟨γ.inl⟩

-- LeanTest/HardProblems/Ruggedness.lean
/-- Sufficient barrier certificate: shortcuts whose witnesses never dip below
the lower of their endpoints leave every barrier height unchanged. The theorem
does not claim that this certificate is necessary. -/
theorem barrier_shortcut_eq {Adj S : X → X → Prop} {J : X → ℝ}
    (hback : ∀ u w, S u w → ∃ γ : PathBetween Adj u w,
      ∀ z ∈ γ.points, min (J u) (J w) ≤ J z) (x y : X) :
    barrier (fun a b => Adj a b ∨ S a b) J x y = barrier Adj J x y := by
  refine le_antisymm (le_iInf fun γ => ?_) (le_iInf fun γ => ?_)
  · exact iInf_le_of_le γ.inl le_rfl
  · obtain ⟨γ', hγ'⟩ := exists_splice hback γ
    refine iInf_le_of_le γ' (iSup_le fun z => iSup_le fun hz => ?_)
    obtain ⟨p, hp, hple⟩ := hγ' z hz
    have key : ENNReal.ofReal (J x - J z) ≤ ENNReal.ofReal (J x - J p) :=
      ENNReal.ofReal_le_ofReal (by linarith)
    exact key.trans (le_biSup (fun p => ENNReal.ofReal (J x - J p)) hp)

-- LeanTest/HardProblems/Ruggedness.lean
/-- Mere `Nonempty` backing is insufficient for barrier preservation: a
shortcut can hide a valley. On the
two-step chain with a dip in the middle, admitting the backed shortcut
`0 → 2` drops the barrier from `ENNReal.ofReal 1` to `0`. This does not show
that the sufficient depth condition of `barrier_shortcut_eq` is necessary. -/
theorem exists_shortcut_hiding_valley :
    ∃ (Adj S : Fin 3 → Fin 3 → Prop) (J : Fin 3 → ℝ),
      (∀ u w, S u w → Nonempty (PathBetween Adj u w)) ∧
      ∃ x y : Fin 3,
        barrier (fun a b => Adj a b ∨ S a b) J x y < barrier Adj J x y := by
  refine ⟨hideAdj, hideS, hideJ, ?_, 0, 2, ?_⟩
  · intro u w huw
    obtain ⟨rfl, rfl⟩ : u = 0 ∧ w = 2 := huw
    refine ⟨⟨[0, 1, 2], rfl, rfl, ?_⟩⟩
    refine List.isChain_cons_cons.2 ⟨Or.inl ⟨rfl, rfl⟩, ?_⟩
    exact List.isChain_cons_cons.2 ⟨Or.inr ⟨rfl, rfl⟩, List.isChain_singleton _⟩
  · have hunion : barrier (fun a b => hideAdj a b ∨ hideS a b) hideJ 0 2 = 0 := by
      refine barrier_eq_zero_of_monotone_path ⟨[0, 2], rfl, rfl, ?_⟩ ?_
      · exact List.isChain_cons_cons.2 ⟨Or.inr ⟨rfl, rfl⟩, List.isChain_singleton _⟩
      · intro z hz
        have hz' : z = 0 ∨ z = 2 := by simpa using hz
        rcases hz' with rfl | rfl
        · exact le_rfl
        · rw [hideJ_zero, hideJ_two]
    have hlow : ENNReal.ofReal 1 ≤ barrier hideAdj hideJ 0 2 := by
      refine le_iInf fun γ => ?_
      have hmem : (1 : Fin 3) ∈ γ.points := one_mem_of_path γ
      have hval : ENNReal.ofReal 1 = ENNReal.ofReal (hideJ 0 - hideJ 1) := by
        rw [hideJ_zero, hideJ_one]; norm_num
      rw [hval]
      exact le_biSup (fun z => ENNReal.ofReal (hideJ 0 - hideJ z)) hmem
    rw [hunion]
    exact lt_of_lt_of_le (ENNReal.ofReal_pos.mpr one_pos) hlow

-- LeanTest/HardProblems/Behavioral.lean
/-- A complete signal trajectory on time domain `T`. -/
abbrev Trajectory (T : Type u) (W : Type v) := T → W

-- LeanTest/HardProblems/Behavioral.lean
/-- A behavior is the set of trajectories admitted by a system model. -/
abbrev Behavior (T : Type u) (W : Type v) := Set (Trajectory T W)

-- LeanTest/HardProblems/Behavioral.lean
/-- Apply a signal map pointwise to a trajectory. -/
def mapTrajectory {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (x : Trajectory T W) : Trajectory T V :=
  f ∘ x

-- LeanTest/HardProblems/Behavioral.lean
/-- Hide or relabel signal coordinates by taking the direct image of a
behavior under the pointwise signal map. -/
def hide {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B : Behavior T W) : Behavior T V :=
  mapTrajectory f '' B

-- LeanTest/HardProblems/Behavioral.lean
/-- On one already aligned signal boundary, behavioral interconnection imposes
both component constraints. -/
def interconnect {T : Type u} {W : Type v}
    (B₁ B₂ : Behavior T W) : Behavior T W :=
  B₁ ∩ B₂

-- LeanTest/HardProblems/Behavioral.lean
/-- Hiding after interconnection is contained in interconnecting after hiding.
The reverse inclusion can fail because the two projected witnesses need not be
the same hidden trajectory. -/
theorem hide_interconnect_subset {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B₁ B₂ : Behavior T W) :
    hide f (interconnect B₁ B₂) ⊆
      interconnect (hide f B₁) (hide f B₂) := by
  rintro _ ⟨x, ⟨hx₁, hx₂⟩, rfl⟩
  exact ⟨⟨x, hx₁, rfl⟩, ⟨x, hx₂, rfl⟩⟩

-- LeanTest/HardProblems/Behavioral.lean
/-- Explicit strictness witness: each component admits a different hidden Bool
trajectory with the same visible projection. The components are individually
viable, their interconnection is empty, but their visible projections have a
nonempty interconnection. -/
theorem hide_interconnect_strict_counterexample :
    let f : Bool × Bool → Bool := Prod.fst
    let x₀ : Trajectory Unit (Bool × Bool) := fun _ ↦ (false, false)
    let x₁ : Trajectory Unit (Bool × Bool) := fun _ ↦ (false, true)
    let B₀ : Behavior Unit (Bool × Bool) := {x₀}
    let B₁ : Behavior Unit (Bool × Bool) := {x₁}
    B₀.Nonempty ∧ B₁.Nonempty ∧ interconnect B₀ B₁ = ∅ ∧
      hide f (interconnect B₀ B₁) ⊂
        interconnect (hide f B₀) (hide f B₁) := by
  dsimp
  refine ⟨Set.singleton_nonempty _, Set.singleton_nonempty _, ?_⟩
  have hEmpty :
      interconnect ({fun _ : Unit ↦ (false, false)} :
        Behavior Unit (Bool × Bool)) {fun _ : Unit ↦ (false, true)} = ∅ := by
    apply Set.eq_empty_iff_forall_notMem.mpr
    rintro z ⟨hz₀, hz₁⟩
    rw [Set.mem_singleton_iff] at hz₀ hz₁
    have hEq : (fun _ : Unit ↦ (false, false)) =
        fun _ : Unit ↦ (false, true) := hz₀.symm.trans hz₁
    have := congrFun hEq ()
    simp at this
  refine ⟨hEmpty, ?_⟩
  refine Set.ssubset_iff_subset_ne.mpr
    ⟨hide_interconnect_subset _ _ _, ?_⟩
  intro hEq
  have hVisible : (fun _ : Unit ↦ false) ∈
      interconnect
        (hide Prod.fst ({fun _ : Unit ↦ (false, false)} :
          Behavior Unit (Bool × Bool)))
        (hide Prod.fst ({fun _ : Unit ↦ (false, true)} :
          Behavior Unit (Bool × Bool))) := by
    exact ⟨⟨_, rfl, rfl⟩, ⟨_, rfl, rfl⟩⟩
  have hImpossible : (fun _ : Unit ↦ false) ∈
      hide Prod.fst
        (interconnect ({fun _ : Unit ↦ (false, false)} :
          Behavior Unit (Bool × Bool)) {fun _ : Unit ↦ (false, true)}) := by
    rw [hEq]
    exact hVisible
  rw [hEmpty] at hImpossible
  rcases hImpossible with ⟨_, hmem, _⟩
  exact hmem

-- LeanTest/HardProblems/Behavioral.lean
/-- Exact relabeling by an equivalence loses no behavior. -/
theorem hide_equiv_symm {T : Type u} {W : Type v} {V : Type w}
    (e : W ≃ V) (B : Behavior T W) :
    hide e.symm (hide e B) = B := by
  ext x
  constructor
  · rintro ⟨_, ⟨z, hz, rfl⟩, hzx⟩
    have hzx' : z = x := by
      simpa [mapTrajectory, Function.comp_def] using hzx
    simpa [← hzx'] using hz
  · intro hx
    refine ⟨mapTrajectory e x, ⟨x, hx, rfl⟩, ?_⟩
    funext t
    simp [mapTrajectory, Function.comp_def]

-- LeanTest/HardProblems/Behavioral.lean
/-- A temporal safety predicate holds at every time on every admitted
trajectory. -/
def IsSafe {T : Type u} {W : Type v}
    (B : Behavior T W) (Safe : W → Prop) : Prop :=
  ∀ x ∈ B, ∀ t, Safe (x t)

-- LeanTest/HardProblems/Behavioral.lean
/-- A behavior is viable when it admits at least one trajectory. -/
def IsViable {T : Type u} {W : Type v} (B : Behavior T W) : Prop :=
  B.Nonempty

-- LeanTest/HardProblems/Behavioral.lean
/-- Universal safety is vacuous on the empty behavior. -/
theorem empty_behavior_safe {T : Type u} {W : Type v} {Safe : W → Prop} :
    IsSafe (∅ : Behavior T W) Safe := by
  simp [IsSafe]

-- LeanTest/HardProblems/Behavioral.lean
/-- The empty behavior is not viable. -/
theorem empty_behavior_not_viable {T : Type u} {W : Type v} :
    ¬ IsViable (∅ : Behavior T W) := by
  simp [IsViable]

-- LeanTest/HardProblems/Behavioral.lean
/-- Refining a behavior preserves every universal safety property. -/
theorem isSafe_mono {T : Type u} {W : Type v}
    {B B' : Behavior T W} {Safe : W → Prop}
    (hsub : B' ⊆ B) (h : IsSafe B Safe) : IsSafe B' Safe := by
  intro x hx t
  exact h x (hsub hx) t

-- LeanTest/HardProblems/Behavioral.lean
/-- Direct-image hiding has an exact safety semantics: a visible predicate
holds on every projected trajectory exactly when its pullback holds on every
original trajectory. This says nothing about predicates on discarded signal
coordinates. -/
theorem isSafe_hide_iff {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B : Behavior T W) (SafeV : V → Prop) :
    IsSafe (hide f B) SafeV ↔ IsSafe B (SafeV ∘ f) := by
  constructor
  · intro h x hx t
    simpa [mapTrajectory, Function.comp_def] using
      h (mapTrajectory f x) ⟨x, hx, rfl⟩ t
  · rintro h _ ⟨x, hx, rfl⟩ t
    simpa [mapTrajectory, Function.comp_def] using h x hx t

-- LeanTest/HardProblems/Behavioral.lean
/-- Hiding preserves a safety property only when the signal map carries the
declared internal safe set into the external one. -/
theorem isSafe_hide {T : Type u} {W : Type v} {V : Type w}
    {B : Behavior T W} {SafeW : W → Prop} {SafeV : V → Prop}
    (f : W → V) (hB : IsSafe B SafeW)
    (hmap : ∀ w, SafeW w → SafeV (f w)) :
    IsSafe (hide f B) SafeV := by
  rintro _ ⟨x, hx, rfl⟩ t
  exact hmap (x t) (hB x hx t)

-- LeanTest/HardProblems/Behavioral.lean
/-- A discrete trajectory follows `step` at every successor time. -/
def IsRun {S : Type u} (step : S → S) (x : Trajectory ℕ S) : Prop :=
  ∀ n, x (n + 1) = step (x n)

-- LeanTest/HardProblems/Behavioral.lean
/-- All runs whose initial state lies in `Init`. -/
def generatedBehavior {S : Type u} (step : S → S) (Init : Set S) :
    Behavior ℕ S :=
  {x | x 0 ∈ Init ∧ IsRun step x}

-- LeanTest/HardProblems/Behavioral.lean
/-- Forward invariance gives all-time safety for every generated run. -/
theorem generatedBehavior_safe_of_invariant {S : Type u}
    {step : S → S} {Init Safe : Set S}
    (hInit : Init ⊆ Safe) (hInv : Set.MapsTo step Safe Safe) :
    IsSafe (generatedBehavior step Init) Safe := by
  rintro x ⟨hx₀, hrun⟩ n
  induction n with
  | zero => exact hInit hx₀
  | succ n ih =>
      rw [hrun n]
      exact hInv ih

-- LeanTest/HardProblems/Behavioral.lean
/-- For the behavior generated from every state in `Safe`, temporal safety is
equivalent to one-step forward invariance. -/
theorem generatedBehavior_safe_iff_invariant {S : Type u}
    (step : S → S) (Safe : Set S) :
    IsSafe (generatedBehavior step Safe) Safe ↔
      Set.MapsTo step Safe Safe := by
  constructor
  · intro h s hs
    let x : Trajectory ℕ S := fun n ↦ Nat.rec s (fun _ current ↦ step current) n
    have hrun : IsRun step x := by
      intro n
      simp [x]
    have hx : x ∈ generatedBehavior step Safe := by
      exact ⟨by simpa [x] using hs, hrun⟩
    have hs₁ := h x hx 1
    change x 1 ∈ Safe at hs₁
    simpa [x] using hs₁
  · intro hInv
    exact generatedBehavior_safe_of_invariant (by exact fun _ h ↦ h) hInv

-- LeanTest/HardProblems/Behavioral.lean
/-- Restrict a local trajectory from `I` to a smaller time domain `J`. -/
def restrict {T : Type u} {W : Type v} {I J : Set T}
    (hJI : J ⊆ I) (x : I → W) : J → W :=
  fun t ↦ x ⟨t.1, hJI t.2⟩

-- LeanTest/HardProblems/Behavioral.lean
/-- Two local trajectories agree wherever their time domains overlap. -/
def Compatible {T : Type u} {W : Type v} {I J : Set T}
    (x : I → W) (y : J → W) : Prop :=
  ∀ (t : T) (htI : t ∈ I) (htJ : t ∈ J),
    x ⟨t, htI⟩ = y ⟨t, htJ⟩

-- LeanTest/HardProblems/Behavioral.lean
/-- Compatible functions on two time domains have a unique global function on
their union with the prescribed restrictions. -/
theorem existsUnique_glue {T : Type u} {W : Type v} {I J : Set T}
    (x : I → W) (y : J → W) (hxy : Compatible x y) :
    ∃! z : ↥(I ∪ J) → W,
      restrict Set.subset_union_left z = x ∧
      restrict Set.subset_union_right z = y := by
  classical
  let z : ↥(I ∪ J) → W := fun t ↦
    if htI : (t : T) ∈ I then x ⟨t, htI⟩
    else y ⟨t, t.property.resolve_left htI⟩
  have hzI : restrict Set.subset_union_left z = x := by
    funext t
    simp [restrict, z]
  have hzJ : restrict Set.subset_union_right z = y := by
    funext t
    by_cases htI : (t : T) ∈ I
    · simpa [restrict, z, htI] using hxy t htI t.property
    · simp [restrict, z, htI]
  refine ⟨z, ⟨hzI, hzJ⟩, ?_⟩
  intro z' hz'
  funext t
  by_cases htI : (t : T) ∈ I
  · have h := congrFun hz'.1 (⟨t, htI⟩ : I)
    simpa [restrict, z, htI] using h
  · have htJ : (t : T) ∈ J := t.property.resolve_left htI
    have h := congrFun hz'.2 (⟨t, htJ⟩ : J)
    simpa [restrict, z, htI] using h

-- LeanTest/HardProblems/Behavioral.lean
/-- Raw compatible functions glue, but a nonempty declared set of admissible
global trajectories need not contain that glue. Thus arbitrary local/global
admissibility data do not acquire the sheaf property for free. -/
theorem admissible_glue_counterexample :
    let I : Set Bool := {false}
    let J : Set Bool := {true}
    let x : I → Bool := fun _ ↦ false
    let y : J → Bool := fun _ ↦ true
    let G : Set (↥(I ∪ J) → Bool) := {fun _ ↦ false}
    Compatible x y ∧ G.Nonempty ∧
      ¬ ∃ z ∈ G,
        restrict Set.subset_union_left z = x ∧
        restrict Set.subset_union_right z = y := by
  dsimp
  refine ⟨?_, Set.singleton_nonempty _, ?_⟩
  · intro t htI htJ
    rw [Set.mem_singleton_iff] at htI htJ
    exact Bool.noConfusion (htI.symm.trans htJ)
  · rintro ⟨z, hz, ⟨_, hzJ⟩⟩
    subst z
    have h := congrFun hzJ (⟨true, by simp⟩ : (↑({true} : Set Bool)))
    simp [restrict] at h

-- LeanTest/HardProblems/Representation.lean
/-- Drive deterministic dynamics with a finite input word, applying its
leftmost input first. -/
def run {U X : Type*} (step : U → X → X) : List U → X → X
  | [], x => x
  | u :: us, x => run step us (step u x)

-- LeanTest/HardProblems/Representation.lean
/-- Two states have identical outputs after every finite input word. -/
def Indist (step : U → X → X) (out : X → Y) (x x' : X) : Prop :=
  ∀ us : List U, out (run step us x) = out (run step us x')

-- LeanTest/HardProblems/Representation.lean
/-- A conjugating equivalence commutes with every finite run. -/
theorem run_conj (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'}
    (hstep : ∀ u x, e (step u x) = step' u (e x)) (us : List U) (x : X) :
    e (run step us x) = run step' us (e x) := by
  induction us generalizing x with
  | nil => rfl
  | cons u us ih =>
    simp only [run]
    rw [ih, hstep]

-- LeanTest/HardProblems/Representation.lean
/-- Coordinate change preserves finite-word indistinguishability in both
directions when it conjugates transitions and preserves outputs. -/
theorem indist_conj_iff (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'} {out : X → Y} {out' : X' → Y}
    (hstep : ∀ u x, e (step u x) = step' u (e x))
    (hout : ∀ x, out x = out' (e x)) (x y : X) :
    Indist step out x y ↔ Indist step' out' (e x) (e y) := by
  constructor
  · intro h us
    rw [← run_conj e hstep, ← run_conj e hstep]
    rw [← hout, ← hout]
    exact h us
  · intro h us
    rw [hout, hout]
    rw [run_conj e hstep, run_conj e hstep]
    exact h us

-- LeanTest/HardProblems/Representation.lean
/-- States reachable from `x` by some finite input word. -/
def reachableSet (step : U → X → X) (x : X) : Set X :=
  {z | ∃ us : List U, run step us x = z}

-- LeanTest/HardProblems/Representation.lean
/-- A conjugating equivalence commutes with every finite run. -/
theorem run_conj (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'}
    (hstep : ∀ u x, e (step u x) = step' u (e x)) (us : List U) (x : X) :
    e (run step us x) = run step' us (e x) := by
  induction us generalizing x with
  | nil => rfl
  | cons u us ih =>
    simp only [run]
    calc
      e (run step us (step u x)) = run step' us (e (step u x)) := ih _
      _ = run step' us (step' u (e x)) := congrArg (run step' us) (hstep u x)

-- LeanTest/HardProblems/Representation.lean
/-- Coordinate change carries the concrete reachable set exactly onto the
reachable set in the conjugate coordinates. -/
theorem image_reachableSet_conj (e : X ≃ X') {step : U → X → X}
    {step' : U → X' → X'}
    (hstep : ∀ u x, e (step u x) = step' u (e x)) (x : X) :
    e '' reachableSet step x = reachableSet step' (e x) := by
  ext z
  constructor
  · rintro ⟨y, ⟨us, hus⟩, rfl⟩
    exact ⟨us, (run_conj e hstep us x).symm.trans (congrArg e hus)⟩
  · rintro ⟨us, hus⟩
    refine ⟨run step us x, ⟨us, rfl⟩, ?_⟩
    exact (run_conj e hstep us x).trans hus

-- LeanTest/HardProblems/Representation.lean
/-- A finite path including both endpoints. -/
structure PathBetween {X : Type u} (Adj : X → X → Prop) (x y : X) where
  points : List X
  head_eq : points.head? = some x
  last_eq : points.getLast? = some y
  admissible : points.IsChain Adj

-- LeanTest/HardProblems/Representation.lean
/-- Relabel a graph along a state-space equivalence. -/
def Relabel {X : Type u} {Y : Type v} (e : X ≃ Y)
    (Adj : X → X → Prop) : Y → Y → Prop :=
  fun a b => Adj (e.symm a) (e.symm b)

-- LeanTest/HardProblems/Representation.lean
/-- Map a path through any edge-preserving function. -/
def PathBetween.map {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    (f : X → Y) (hstep : ∀ {a b}, Adj a b → Adj' (f a) (f b))
    {x y : X} (γ : PathBetween Adj x y) : PathBetween Adj' (f x) (f y) where
  points := γ.points.map f
  head_eq := by rw [List.head?_map, γ.head_eq]; rfl
  last_eq := by rw [List.getLast?_map, γ.last_eq]; rfl
  admissible := (List.isChain_map f).mpr
    (γ.admissible.imp fun _ _ h => hstep h)

-- LeanTest/HardProblems/Representation.lean
/-- Transport a path through a coordinate equivalence. -/
def PathBetween.relabel {X : Type u} {Y : Type v} {Adj : X → X → Prop}
    (e : X ≃ Y) {x y : X} (γ : PathBetween Adj x y) :
    PathBetween (Relabel e Adj) (e x) (e y) :=
  γ.map e (by intro a b h; simpa [Relabel] using h)

-- LeanTest/HardProblems/Representation.lean
/-- Return a transported path to the original coordinates. -/
def PathBetween.unrelabel {X : Type u} {Y : Type v} {Adj : X → X → Prop}
    (e : X ≃ Y) {x y : X}
    (γ : PathBetween (Relabel e Adj) (e x) (e y)) : PathBetween Adj x y := by
  simpa [Relabel] using
    γ.map e.symm (by intro a b h; simpa [Relabel] using h)

-- LeanTest/HardProblems/Representation.lean
/-- The deepest dip below the score of the starting vertex along one path. -/
noncomputable def pathDepth {X : Type u} {Adj : X → X → Prop}
    (J : X → ℝ) (x : X) {y : X} (γ : PathBetween Adj x y) : ℝ≥0∞ :=
  ⨆ z ∈ γ.points, ENNReal.ofReal (J x - J z)

-- LeanTest/HardProblems/Representation.lean
/-- The least path depth; the empty infimum is `⊤`. -/
noncomputable def barrier {X : Type u} (Adj : X → X → Prop)
    (J : X → ℝ) (x y : X) : ℝ≥0∞ :=
  ⨅ γ : PathBetween Adj x y, pathDepth J x γ

-- LeanTest/HardProblems/Representation.lean
/-- Relabeling a path and objective preserves that path's depth exactly. -/
theorem pathDepth_relabel {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} (e : X ≃ Y) (J : X → ℝ)
    {x y : X} (γ : PathBetween Adj x y) :
    pathDepth (fun z => J (e.symm z)) (e x) (γ.relabel e) =
      pathDepth J x γ := by
  simp only [pathDepth, PathBetween.relabel, PathBetween.map,
    Equiv.symm_apply_apply]
  apply le_antisymm
  · refine iSup_le fun z => iSup_le fun hz => ?_
    obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hz
    simpa using
      (le_iSup_of_le a
        (le_iSup_of_le ha (le_refl (ENNReal.ofReal (J x - J a)))))
  · refine iSup_le fun a => iSup_le fun ha => ?_
    refine le_iSup_of_le (e a) (le_iSup_of_le ?_ ?_)
    · exact List.mem_map.mpr ⟨a, ha, rfl⟩
    · simp

-- LeanTest/HardProblems/Representation.lean
/-- Returning a relabeled path to the source coordinates also preserves its
depth exactly. -/
theorem pathDepth_unrelabel {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} (e : X ≃ Y) (J : X → ℝ)
    {x y : X} (γ : PathBetween (Relabel e Adj) (e x) (e y)) :
    pathDepth J x (γ.unrelabel e) =
      pathDepth (fun z => J (e.symm z)) (e x) γ := by
  simp only [pathDepth, unrelabel_points, Equiv.symm_apply_apply]
  apply le_antisymm
  · refine iSup_le fun a => iSup_le fun ha => ?_
    obtain ⟨z, hz, rfl⟩ := List.mem_map.mp ha
    exact le_iSup_of_le z (le_iSup_of_le hz (le_refl _))
  · refine iSup_le fun z => iSup_le fun hz => ?_
    refine le_iSup_of_le (e.symm z) (le_iSup_of_le ?_ ?_)
    · exact List.mem_map.mpr ⟨z, hz, rfl⟩
    · rfl

-- LeanTest/HardProblems/Representation.lean
/-- Exact coordinate changes preserve the existence of a path. -/
theorem path_nonempty_relabel_iff {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} (e : X ≃ Y) {x y : X} :
    Nonempty (PathBetween (Relabel e Adj) (e x) (e y)) ↔
      Nonempty (PathBetween Adj x y) := by
  constructor
  · rintro ⟨γ⟩
    exact ⟨γ.unrelabel e⟩
  · rintro ⟨γ⟩
    exact ⟨γ.relabel e⟩

-- LeanTest/HardProblems/Representation.lean
/-- Exact coordinate changes preserve every barrier height, including the
infinite value caused by unreachability. -/
theorem barrier_relabel_eq {X : Type u} {Y : Type v}
    (Adj : X → X → Prop) (e : X ≃ Y) (J : X → ℝ) (x y : X) :
    barrier (Relabel e Adj) (fun z => J (e.symm z)) (e x) (e y) =
      barrier Adj J x y := by
  apply le_antisymm
  · refine le_iInf fun γ => ?_
    exact iInf_le_of_le (γ.relabel e)
      (le_of_eq (pathDepth_relabel e J γ))
  · refine le_iInf fun γ => ?_
    exact iInf_le_of_le (γ.unrelabel e)
      (le_of_eq (pathDepth_unrelabel e J γ))

-- LeanTest/HardProblems/Representation.lean
/-- Finite reflexive-transitive reachability generated by `Adj`. -/
inductive Reach {X : Type u} (Adj : X → X → Prop) (x : X) : X → Prop
  | refl : Reach Adj x x
  | tail {y z : X} : Reach Adj x y → Adj y z → Reach Adj x z

-- LeanTest/HardProblems/Representation.lean
/-- A map that preserves single steps preserves finite reachability. -/
theorem map {X : Type u} {Y : Type v} {Adj : X → X → Prop}
    {Adj' : Y → Y → Prop} {f : X → Y} {x y : X}
    (hstep : ∀ {a b}, Adj a b → Adj' (f a) (f b))
    (h : Reach Adj x y) : Reach Adj' (f x) (f y) := by
  induction h with
  | refl => exact Reach.refl
  | tail hxy hyz ih => exact Reach.tail ih (hstep hyz)

-- LeanTest/HardProblems/Representation.lean
/-- Some state in `G` is reachable from `x`. -/
def ReachTo {X : Type u} (Adj : X → X → Prop) (G : Set X) (x : X) : Prop :=
  ∃ y, Reach Adj x y ∧ y ∈ G

-- LeanTest/HardProblems/Representation.lean
/-- Every concrete step has a corresponding abstract step. -/
def ForwardSimulation {X : Type u} {Y : Type v} (f : X → Y)
    (Adj : X → X → Prop) (Adj' : Y → Y → Prop) : Prop :=
  ∀ {x y}, Adj x y → Adj' (f x) (f y)

-- LeanTest/HardProblems/Representation.lean
/-- Every abstract step offered at `f x` can be implemented from that actual
concrete representative `x`. This is stronger than requiring some member of
the fibre to implement the step. -/
def StepLifting {X : Type u} {Y : Type v} (f : X → Y)
    (Adj : X → X → Prop) (Adj' : Y → Y → Prop) : Prop :=
  ∀ (x : X) (y' : Y), Adj' (f x) y' →
    ∃ y : X, Adj x y ∧ f y = y'

-- LeanTest/HardProblems/Representation.lean
/-- Forward simulation sends a concrete solution to the image of its concrete
goal set. -/
theorem concrete_reach_maps {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {f : X → Y} {G : Set X} {x₀ : X}
    (hmap : ForwardSimulation f Adj Adj') :
    ReachTo Adj G x₀ → ReachTo Adj' (f '' G) (f x₀) := by
  rintro ⟨y, hxy, hyG⟩
  exact ⟨f y, Reach.map hmap hxy, ⟨y, hyG, rfl⟩⟩

-- LeanTest/HardProblems/Representation.lean
/-- Local step lifting extends to a lift of every finite abstract path, with
the endpoint lying in the required fibre. -/
theorem lift_reach {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {f : X → Y} (hlift : StepLifting f Adj Adj')
    {x : X} {y' : Y} (h : Reach Adj' (f x) y') :
    ∃ y : X, Reach Adj x y ∧ f y = y' := by
  induction h with
  | refl => exact ⟨x, Reach.refl, rfl⟩
  | @tail y' z' hxy hyz ih =>
      rcases ih with ⟨y, hxy', hy⟩
      rcases hlift y z' (hy ▸ hyz) with ⟨z, hyz', hz⟩
      exact ⟨z, Reach.tail hxy' hyz', hz⟩

-- LeanTest/HardProblems/Representation.lean
/-- An abstract solution descends when paths lift and abstract goal membership
reflects concrete success. -/
theorem abstract_reach_lifts {X : Type u} {Y : Type v}
    {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {f : X → Y} {G : Set X} {G' : Set Y} {x₀ : X}
    (hlift : StepLifting f Adj Adj')
    (hreflect : ∀ x, f x ∈ G' → x ∈ G) :
    ReachTo Adj' G' (f x₀) → ReachTo Adj G x₀ := by
  rintro ⟨y', hxy, hyG⟩
  rcases lift_reach hlift hxy with ⟨y, hxy', hy⟩
  exact ⟨y, hxy', hreflect y (hy.symm ▸ hyG)⟩

-- LeanTest/HardProblems/Representation.lean
/-- The hypotheses for exact reachability transfer. -/
structure ExactAbstraction {X : Type u} {Y : Type v} (f : X → Y)
    (Adj : X → X → Prop) (Adj' : Y → Y → Prop)
    (G : Set X) (G' : Set Y) : Prop where
  mapStep : ForwardSimulation f Adj Adj'
  liftStep : StepLifting f Adj Adj'
  goalExact : ∀ x, x ∈ G ↔ f x ∈ G'

-- LeanTest/HardProblems/Representation.lean
/-- Under the exact hypotheses, concrete and abstract goal reachability agree. -/
theorem ExactAbstraction.reachTo_iff {X : Type u} {Y : Type v}
    {f : X → Y} {Adj : X → X → Prop} {Adj' : Y → Y → Prop}
    {G : Set X} {G' : Set Y} (h : ExactAbstraction f Adj Adj' G G') (x : X) :
    ReachTo Adj G x ↔ ReachTo Adj' G' (f x) := by
  constructor
  · rintro ⟨y, hxy, hyG⟩
    exact ⟨f y, Reach.map h.mapStep hxy, h.goalExact y |>.mp hyG⟩
  · exact abstract_reach_lifts h.liftStep (fun y => (h.goalExact y).mpr)

-- LeanTest/HardProblems/Representation.lean
/-- Exact abstractions compose. -/
theorem ExactAbstraction.comp {X : Type u} {Y : Type v} {Z : Type w}
    {f : X → Y} {g : Y → Z}
    {AdjX : X → X → Prop} {AdjY : Y → Y → Prop}
    {AdjZ : Z → Z → Prop} {GX : Set X} {GY : Set Y} {GZ : Set Z}
    (h₁ : ExactAbstraction f AdjX AdjY GX GY)
    (h₂ : ExactAbstraction g AdjY AdjZ GY GZ) :
    ExactAbstraction (g ∘ f) AdjX AdjZ GX GZ := by
  constructor
  · intro x y hxy
    exact h₂.mapStep (h₁.mapStep hxy)
  · intro x z hz
    rcases h₂.liftStep (f x) z hz with ⟨y, hxy, hy⟩
    rcases h₁.liftStep x y hxy with ⟨x', hxx', hx'⟩
    exact ⟨x', hxx', by simp only [Function.comp_apply, hx', hy]⟩
  · intro x
    exact (h₁.goalExact x).trans (h₂.goalExact (f x))

-- LeanTest/HardProblems/Representation.lean
/-- A forward simulation can have a reachable abstract goal with no concrete
representative. This explicit finite example isolates the missing lifting
condition. -/
theorem forward_without_lifting_counterexample :
    let f : Unit → Bool := fun _ => false
    let Adj : Unit → Unit → Prop := fun _ _ => False
    let Adj' : Bool → Bool → Prop := fun a b => a = false ∧ b = true
    ForwardSimulation f Adj Adj' ∧
      ReachTo Adj' ({true} : Set Bool) (f ()) ∧
      ¬ ReachTo Adj {x | f x = true} () := by
  dsimp
  constructor
  · intro x y h
    exact False.elim h
  constructor
  · exact ⟨true, Reach.tail Reach.refl ⟨rfl, rfl⟩, by simp⟩
  · rintro ⟨y, _, hy⟩
    simp at hy

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A deterministic machine with inputs `I`, outputs `O`, and state
space `S`: a step function and an output map. -/
structure Machine (I O S : Type*) where
  step : S → I → S
  out : S → O

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Run a machine from state `s` on an input word `w`. -/
def Machine.run (M : Machine I O S) (s : S) (w : List I) : S :=
  w.foldl M.step s

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A machine is output-separated when any two states that agree on the
outputs along every input word are equal. -/
def Machine.Separated (M : Machine I O S) : Prop :=
  ∀ s t : S, (∀ w : List I, M.out (M.run s w) = M.out (M.run t w)) → s = t

-- LeanTest/HardProblems/BoundedMachines.lean
/-- `f` tracks machine `B` inside machine `A`: the encoding intertwines
the dynamics and reproduces the outputs. This is what it means for `A`
to maintain a faithful copy of `B`. -/
structure Tracks (A : Machine I O S) (B : Machine I O T) (f : T → S) : Prop where
  step_eq : ∀ t i, f (B.step t i) = A.step (f t) i
  out_eq : ∀ t, A.out (f t) = B.out t

-- LeanTest/HardProblems/BoundedMachines.lean
/-- A tracking map intertwines whole runs, not just single steps. -/
theorem Tracks.run_eq {A : Machine I O S} {B : Machine I O T} {f : T → S}
    (h : Tracks A B f) (t : T) (w : List I) :
    f (B.run t w) = A.run (f t) w := by
  induction w generalizing t with
  | nil => rfl
  | cons i w ih =>
    simp [Machine.run]
    rw [← h.step_eq]
    exact ih (B.step t i)

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Tracking an output-separated machine is injective: the tracker must
hold distinct internal states for distinct tracked states. -/
theorem Tracks.injective {A : Machine I O S} {B : Machine I O T} {f : T → S}
    (h : Tracks A B f) (hB : B.Separated) : Function.Injective f := by
  intro t₁ t₂ hft
  apply hB t₁ t₂
  intro w
  have eq1 : f (B.run t₁ w) = A.run (f t₁) w := h.run_eq t₁ w
  have eq2 : f (B.run t₂ w) = A.run (f t₂) w := h.run_eq t₂ w
  rw [← h.out_eq (B.run t₁ w), ← h.out_eq (B.run t₂ w), eq1, eq2, hft]

-- LeanTest/HardProblems/BoundedMachines.lean
/-- The pigeonhole bound: a finite machine can exactly track an
output-separated machine only if it has at least as many states. This is a
capacity bound for the stated exact tracking relation. -/
theorem card_le_of_tracks [Fintype S] [Fintype T]
    {A : Machine I O S} {B : Machine I O T} {f : T → S}
    (h : Tracks A B f) (hB : B.Separated) :
    Fintype.card T ≤ Fintype.card S := by
  exact Fintype.card_le_of_injective _ (Tracks.injective h hB)

-- LeanTest/HardProblems/BoundedMachines.lean
/-- Mutual exact tracking forces cardinality parity for finite
output-separated machines. It does not by itself give an isomorphism between
their transition systems. -/
theorem card_eq_of_mutual_tracks [Fintype S] [Fintype T]
    {A : Machine I O S} {B : Machine I O T} {f : T → S} {g : S → T}
    (hf : Tracks A B f) (hg : Tracks B A g)
    (hA : A.Separated) (hB : B.Separated) :
    Fintype.card S = Fintype.card T := by
  exact le_antisymm (card_le_of_tracks hg hA) (card_le_of_tracks hf hB)

-- LeanTest/HardProblems/Positional.lean
/-- A streaming machine with `k` finite-range registers. -/
structure RegisterMachine (base range k : ℕ) where
  init : Fin k → Fin range
  step : (Fin k → Fin range) → Fin base → (Fin k → Fin range)
  output : (Fin k → Fin range) → ℕ

-- LeanTest/HardProblems/Positional.lean
/-- Run a register machine over a finite input stream. -/
def run {base range k : ℕ} (M : RegisterMachine base range k) :
    List (Fin base) → (Fin k → Fin range) :=
  List.foldl M.step M.init

-- LeanTest/HardProblems/Positional.lean
/-- The fixed-width input stream for multiplying `x` and `y`. -/
def multiplicationInput (base n x y : ℕ) [NeZero base] : List (Fin base) :=
  fixedDigits base n x ++ fixedDigits base n y

-- LeanTest/HardProblems/Positional.lean
/-- The machine computes `n`-digit multiplication when its final-state output
is the product for every pair in the full fixed-width range `[0, base^n)`.
In particular, this quantifies over the actual transition-based execution; it
is not the mere existence of an unconstrained function on inputs. -/
def ComputesMultiplicationAt {base range k : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (n : ℕ) : Prop :=
  ∀ x y, x < base ^ n → y < base ^ n →
    M.output (M.run (multiplicationInput base n x y)) = x * y

-- LeanTest/HardProblems/Positional.lean
/-- If a machine computes multiplication at width `n`, fixing the second
operand to one makes final configurations for distinct first operands distinct. -/
theorem finalState_injective {base range k n : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (hbase : 2 ≤ base) (hn : 0 < n)
    (hM : M.ComputesMultiplicationAt n) :
    Function.Injective (fun x : Fin (base ^ n) =>
      M.run (multiplicationInput base n x 1)) := by
  intro x y hxy
  have h1 : (1 : ℕ) < base ^ n := one_lt_pow₀ (by omega) (by omega)
  have hx := hM x 1 x.is_lt h1
  have hy := hM y 1 y.is_lt h1
  simp only [mul_one] at hx hy
  simp only at hxy
  rw [hxy] at hx
  exact Fin.ext (hx.symm.trans hy)

-- LeanTest/HardProblems/Positional.lean
/-- The central configuration-count lower bound: a correct width-`n` machine
needs at least `base^n` different register configurations. -/
theorem state_capacity_lower_bound {base range k n : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (hbase : 2 ≤ base) (hn : 0 < n)
    (hM : M.ComputesMultiplicationAt n) :
    base ^ n ≤ range ^ k := by
  have hinj := finalState_injective M hbase hn hM
  simpa using Fintype.card_le_of_injective _ hinj

-- LeanTest/HardProblems/Positional.lean
/-- Quantitative binary form.  If all register configurations can be encoded
in at most `bits` bits, correctness forces at least `n` bits. -/
theorem linear_bit_lower_bound {base range k n bits : ℕ} [NeZero base]
    (M : RegisterMachine base range k) (hbase : 2 ≤ base) (hn : 0 < n)
    (hM : M.ComputesMultiplicationAt n)
    (hbits : range ^ k ≤ 2 ^ bits) :
    n ≤ bits := by
  have h1 : base ^ n ≤ range ^ k := state_capacity_lower_bound M hbase hn hM
  have h2 : base ^ n ≤ 2 ^ bits := h1.trans hbits
  have h3 : 2 ^ n ≤ base ^ n := Nat.pow_le_pow_left hbase _
  have h4 : 2 ^ n ≤ 2 ^ bits := h3.trans h2
  exact (Nat.pow_le_pow_iff_right (by decide : 1 < 2)).mp h4

-- LeanTest/HardProblems/Positional.lean
/-- For every fixed finite register count and fixed finite value range, some
positive digit width cannot be handled under `ComputesMultiplicationAt`. Thus
no fixed finite configuration space satisfies this interface at every width. -/
theorem no_constant_register_budget (base range k : ℕ) (hbase : 2 ≤ base) :
    ∃ n > 0, ∀ M : RegisterMachine base range k,
      letI : NeZero base := ⟨by omega⟩
      ¬ M.ComputesMultiplicationAt n := by
  letI : NeZero base := ⟨by omega⟩
  have hbase1 : 1 < base := hbase
  by_cases hk : k = 0
  · exact ⟨1, by norm_num, fun M hM => by
      have hcap := state_capacity_lower_bound M hbase (by norm_num : 0 < 1) hM
      simp [hk] at hcap
      omega⟩
  · by_cases hr : range = 0
    · exact ⟨1, by norm_num, fun M hM => by
        have hcap := state_capacity_lower_bound M hbase (by norm_num : 0 < 1) hM
        simp [hr, hk] at hcap
        omega⟩
    · have hk0 : k ≠ 0 := hk
      have hpos : 0 < range ^ k := by positivity
      exact ⟨range ^ k, hpos, fun M hM => by
        have hcap := state_capacity_lower_bound M hbase hpos hM
        exact (Nat.lt_pow_self hbase1).not_ge hcap⟩

-- LeanTest/HardProblems/ResourceBounds.lean
/-- A resource envelope specifies which programs are admitted and requires the
admitted set to be finite. -/
structure Envelope (P : Type*) where
  admits : P → Prop
  finite : Set.Finite {p | admits p}

-- LeanTest/HardProblems/ResourceBounds.lean
/-- A real-valued objective attains a maximum on any nonempty finite resource
envelope. This is an existence theorem, not an optimization procedure. -/
theorem exists_bounded_optimum {P : Type*} (E : Envelope P) (V : P → ℝ)
    (hne : ∃ p, E.admits p) :
    ∃ p, E.admits p ∧ ∀ q, E.admits q → V q ≤ V p := by
  obtain ⟨p, hp, hmax⟩ :=
    Set.exists_max_image {p | E.admits p} V E.finite hne
  exact ⟨p, hp, hmax⟩

-- LeanTest/HardProblems/ResourceBounds.lean
/-- If one finite envelope is included in another, the value of an optimum in
the larger envelope is at least that of an optimum in the smaller envelope. -/
theorem bounded_optimum_mono {P : Type*} (E F : Envelope P) (V : P → ℝ)
    (hEF : ∀ p, E.admits p → F.admits p)
    (p : P) (hp : E.admits p) (_hopt : ∀ q, E.admits q → V q ≤ V p)
    (q : P) (_hq : F.admits q) (hqopt : ∀ r, F.admits r → V r ≤ V q) :
    V p ≤ V q := by
  exact hqopt p (hEF p hp)

-- LeanTest/HardProblems/ResourceBounds.lean
/-- There is a nonempty finite envelope whose internal optimum is strictly
dominated by an excluded program. The witness's objective is unbounded, so the
statement deliberately does not claim that the excluded program is a global
optimum. -/
theorem exists_strict_envelope_gap :
    ∃ (E : Envelope ℕ) (V : ℕ → ℝ) (p : ℕ),
      E.admits p ∧ (∀ q, E.admits q → V q ≤ V p) ∧
      ∃ r, V p < V r := by
  use ⟨fun n => n = 0, by simp⟩
  use fun n => n
  use 0
  simp
  exact ⟨1, by norm_num⟩

-- LeanTest/HardProblems/FibredOrder.lean
/-- A strict contravariant family of partial orders over a category.

The pointwise identity and composition equations record a chosen splitting.
They are the only categorical coherence claimed in this file. -/
structure SplitIndexedOrder (C : Type u) [Category.{v} C] where
  /-- The carrier of the ordered fiber over a context. -/
  Fiber : C → Type w
  /-- The partial order in each fiber. -/
  fiberOrder : (c : C) → PartialOrder (Fiber c)
  /-- Contravariant transport along a context morphism. -/
  reindex : {c d : C} → (c ⟶ d) → Fiber d → Fiber c
  /-- Reindexing along an identity is the identity. -/
  reindex_id : ∀ (c : C) (x : Fiber c), reindex (𝟙 c) x = x
  /-- Reindexing reverses categorical composition. -/
  reindex_comp : ∀ {c d e : C} (f : c ⟶ d) (g : d ⟶ e)
    (x : Fiber e), reindex (f ≫ g) x = reindex f (reindex g x)
  /-- Every reindexing map is monotone in the fiber orders. -/
  reindex_mono : ∀ {c d : C} (f : c ⟶ d) {x y : Fiber d},
    (fiberOrder d).le x y → (fiberOrder c).le (reindex f x) (reindex f y)

-- LeanTest/HardProblems/FibredOrder.lean
/-- Reindexing as an order homomorphism. -/
def reindexHom (P : SplitIndexedOrder C) {c d : C} (f : c ⟶ d) :
    P.Fiber d →o P.Fiber c where
  toFun := P.reindex f
  monotone' := by
    intro x y hxy
    exact P.reindex_mono f hxy

-- LeanTest/HardProblems/FibredOrder.lean
@[simp]
theorem reindex_id_apply (P : SplitIndexedOrder C) (c : C) (x : P.Fiber c) :
    P.reindex (𝟙 c) x = x :=
  P.reindex_id c x

-- LeanTest/HardProblems/FibredOrder.lean
@[simp]
theorem reindex_comp_apply (P : SplitIndexedOrder C) {c d e : C}
    (f : c ⟶ d) (g : d ⟶ e) (x : P.Fiber e) :
    P.reindex (f ≫ g) x = P.reindex f (P.reindex g x) :=
  P.reindex_comp f g x

-- LeanTest/HardProblems/FibredOrder.lean
/-- The context-indexed partial order of all candidate performance regions
induced by a functor of performance-coordinate types. Context morphisms act
on points by `Perf.map`; candidate regions move in the opposite direction by
preimage. Realizability by an encounter or program is not part of this data. -/
def performanceRegions {C : Type u} [Category.{v} C] (Perf : C ⥤ Type w) :
    SplitIndexedOrder C where
  Fiber c := Set (Perf.obj c)
  fiberOrder _ := inferInstance
  reindex f A := Perf.map f ⁻¹' A
  reindex_id c A := by
    ext x
    simp
  reindex_comp f g A := by
    ext x
    simp
  reindex_mono := by
    intro c d f A B hAB
    exact Set.preimage_mono hAB

-- LeanTest/HardProblems/FibredOrder.lean
/-- Encounter data sufficient to make realized performance regions stable
under contravariant context change.

No identity or composition equation is imposed on `transport` at the level of
raw encounters. Only its observable effect on regions is stored. That exact
compatibility is enough to induce split reindexing after duplicate encounter
witnesses have been forgotten. -/
structure CompatibleEncounterRegions {C : Type u} [Category.{v} C]
    (Perf : C ⥤ Type w) where
  /-- The type of admitted encounters in each context. -/
  Encounter : C → Type e
  /-- The candidate region actually realized by an encounter. -/
  region : (c : C) → Encounter c → Set (Perf.obj c)
  /-- Contravariant transport of encounters along a context map. -/
  transport : {c d : C} → (c ⟶ d) → Encounter d → Encounter c
  /-- Transport realizes exactly the preimage of the target encounter's
  region. -/
  region_transport : ∀ {c d : C} (f : c ⟶ d) (E : Encounter d),
    region c (transport f E) = Perf.map f ⁻¹' region d E

-- LeanTest/HardProblems/FibredOrder.lean
/-- A region together with the proposition that some admitted encounter
realizes it. Different encounter witnesses with the same region determine the
same element of this subtype. -/
def RealizedRegion (D : CompatibleEncounterRegions Perf) (c : C) :=
  {A : Set (Perf.obj c) // ∃ E : D.Encounter c, D.region c E = A}

-- LeanTest/HardProblems/FibredOrder.lean
/-- Realized regions inherit the antisymmetric subset order from their
underlying sets; encounter witnesses do not participate in equality. -/
instance instPartialOrderRealizedRegion (D : CompatibleEncounterRegions Perf)
    (c : C) : PartialOrder (D.RealizedRegion c) :=
  PartialOrder.lift Subtype.val Subtype.val_injective

-- LeanTest/HardProblems/FibredOrder.lean
/-- Reindex a realized region by preimage. Compatibility supplies a transported
encounter witnessing that the resulting region is realized in the source
context. -/
def reindexRealized (D : CompatibleEncounterRegions Perf) {c d : C}
    (f : c ⟶ d) (A : D.RealizedRegion d) : D.RealizedRegion c :=
  ⟨Perf.map f ⁻¹' A.1, by
    rcases A.2 with ⟨E, hE⟩
    refine ⟨D.transport f E, ?_⟩
    rw [D.region_transport, hE]⟩

-- LeanTest/HardProblems/FibredOrder.lean
/-- The underlying set of a reindexed realized region is transparently the
ambient preimage. -/
@[simp]
theorem reindexRealized_val (D : CompatibleEncounterRegions Perf) {c d : C}
    (f : c ⟶ d) (A : D.RealizedRegion d) :
    (D.reindexRealized f A).1 = Perf.map f ⁻¹' A.1 :=
  rfl

-- LeanTest/HardProblems/FibredOrder.lean
/-- Realized regions form a split context-indexed partial order. The split laws
hold for region values; they do not assert coherent identity or composition
laws for the chosen raw encounter transports. -/
def realizedRegionOrder (D : CompatibleEncounterRegions Perf) :
    SplitIndexedOrder C where
  Fiber c := D.RealizedRegion c
  fiberOrder _ := inferInstance
  reindex := D.reindexRealized
  reindex_id c A := by
    apply Subtype.ext
    ext x
    simp [reindexRealized]
  reindex_comp f g A := by
    apply Subtype.ext
    ext x
    simp [reindexRealized]
  reindex_mono := by
    intro c d f A B hAB
    exact Set.preimage_mono hAB

-- LeanTest/HardProblems/FibredOrder.lean
/-- The reindexing stored in `realizedRegionOrder` has the same transparent
preimage value as `reindexRealized`. -/
@[simp]
theorem realizedRegionOrder_reindex_val
    (D : CompatibleEncounterRegions Perf) {c d : C}
    (f : c ⟶ d) (A : D.RealizedRegion d) :
    ((D.realizedRegionOrder).reindex f A).1 = Perf.map f ⁻¹' A.1 :=
  rfl

-- LeanTest/HardProblems/FibredOrder.lean
/-- Without compatible encounter transport, an ambient preimage need not be
among the regions declared realized in the source context. Both declared
families below are nonempty, yet the preimage of the realized target region is
not a realized source region. -/
theorem ambient_preimage_can_be_unrealized :
    let f : Unit → Bool := fun _ ↦ false
    let sourceRealized : Set (Set Unit) := {∅}
    let targetRegion : Set Bool := {false}
    let targetRealized : Set (Set Bool) := {targetRegion}
    sourceRealized.Nonempty ∧ targetRealized.Nonempty ∧
      targetRegion ∈ targetRealized ∧
      f ⁻¹' targetRegion ∉ sourceRealized := by
  simp

-- LeanTest/HardProblems/FibredOrder.lean
/-- Compare encounters by inclusion of their attainable regions. This is the
pullback of the fiber order along an encounter-to-region map. -/
def EncounterLE {E : Type u} {P : Type w} (region : E → Set P)
    (x y : E) : Prop :=
  region x ⊆ region y

-- LeanTest/HardProblems/FibredOrder.lean
/-- Region comparison pulled back to encounters is reflexive. -/
theorem encounterLE_refl {E : Type u} {P : Type w} (region : E → Set P)
    (x : E) : EncounterLE region x x :=
  Set.Subset.rfl

-- LeanTest/HardProblems/FibredOrder.lean
/-- Region comparison pulled back to encounters is transitive. -/
theorem encounterLE_trans {E : Type u} {P : Type w} (region : E → Set P)
    {x y z : E} (hxy : EncounterLE region x y)
    (hyz : EncounterLE region y z) : EncounterLE region x z :=
  hxy.trans hyz

-- LeanTest/HardProblems/FibredOrder.lean
/-- The pulled-back comparison is antisymmetric exactly when the
encounter-to-region map is injective. Without injectivity it is only a
preorder on encounters; quotienting encounters by equal regions restores a
partial order. -/
theorem encounterLE_antisymmetric_iff_injective {E : Type u} {P : Type w}
    (region : E → Set P) :
    (∀ ⦃x y : E⦄, EncounterLE region x y →
      EncounterLE region y x → x = y) ↔ Function.Injective region := by
  constructor
  · intro h x y hxy
    apply h
    · simp [EncounterLE, hxy]
    · simp [EncounterLE, hxy]
  · intro hinj x y hxy hyx
    exact hinj (Set.Subset.antisymm hxy hyx)

-- LeanTest/HardProblems/FibredOrder.lean
/-- Two distinct encounters assigned the same region witness the failure of
antisymmetry. The failure is in the encounter presentation, not in the subset
order on regions. -/
theorem constant_region_not_antisymmetric :
    let region : Bool → Set Unit := fun _ ↦ ∅
    EncounterLE region false true ∧ EncounterLE region true false ∧
      false ≠ true := by
  simp [EncounterLE]

-- LeanTest/HardProblems/FibredOrder.lean
/-- Preimage along a surjective point map preserves and reflects inclusion.
Bijectivity is therefore sufficient but not necessary for exact comparison
transport at the level of arbitrary candidate regions. -/
theorem surjective_preimage_subset_iff {X : Type u} {Y : Type w}
    (f : X → Y) (hf : Function.Surjective f) (A B : Set Y) :
    f ⁻¹' A ⊆ f ⁻¹' B ↔ A ⊆ B := by
  constructor
  · intro h y hy
    rcases hf y with ⟨x, rfl⟩
    exact h hy
  · exact Set.preimage_mono

-- LeanTest/HardProblems/FibredOrder.lean
/-- A bijective coordinate change preserves and reflects inclusion after
contravariant reindexing. Hence an exact relabeling neither creates nor erases
comparisons between candidate performance regions. -/
theorem equiv_preimage_subset_iff {X : Type u} {Y : Type w}
    (e : X ≃ Y) (A B : Set Y) :
    e ⁻¹' A ⊆ e ⁻¹' B ↔ A ⊆ B :=
  surjective_preimage_subset_iff e e.surjective A B

-- LeanTest/HardProblems/FibredOrder.lean
/-- The preservation direction of exact coordinate invariance. -/
theorem equiv_preimage_preserves_inclusion {X : Type u} {Y : Type w}
    (e : X ≃ Y) {A B : Set Y} (h : A ⊆ B) :
    e ⁻¹' A ⊆ e ⁻¹' B :=
  (equiv_preimage_subset_iff e A B).2 h

-- LeanTest/HardProblems/FibredOrder.lean
/-- The reflection direction of exact coordinate invariance. It depends on
surjectivity and is unavailable for a general non-surjective coordinate map. -/
theorem equiv_preimage_reflects_inclusion {X : Type u} {Y : Type w}
    (e : X ≃ Y) {A B : Set Y} (h : e ⁻¹' A ⊆ e ⁻¹' B) :
    A ⊆ B :=
  (equiv_preimage_subset_iff e A B).1 h

-- LeanTest/HardProblems/FibredOrder.lean
/-- Explicit failure of preimage order reflection for a non-surjective point
map. The injective constant map `Unit → Bool` misses `true`, so the whole Bool
region and `{false}` have equal preimages even though the former is not
contained in the latter. The issue here is failure of surjectivity, not
many-to-one collapse. -/
theorem nonsurjective_preimage_not_order_reflecting :
    let f : Unit → Bool := fun _ ↦ false
    let A : Set Bool := Set.univ
    let B : Set Bool := {false}
    ¬ Function.Surjective f ∧
      f ⁻¹' A = f ⁻¹' B ∧ f ⁻¹' A ⊆ f ⁻¹' B ∧ ¬ A ⊆ B := by
  dsimp
  constructor
  · intro hf
    rcases hf true with ⟨x, hx⟩
    simp at hx
  constructor
  · ext x
    simp
  constructor
  · intro x hx
    simp
  · intro h
    have : true ∈ ({false} : Set Bool) := h (Set.mem_univ true)
    simp at this

-- LeanTest/HardProblems/FibredOrder.lean
/-- Explicit failure of direct-image order reflection for a noninjective point
map. The constant map `Bool → Unit` merges `false` and `true`, so their
singleton regions have equal direct images although neither singleton is
contained in the other. This is the separate many-to-one failure mode. -/
theorem noninjective_image_not_order_reflecting :
    let f : Bool → Unit := fun _ ↦ ()
    let A : Set Bool := {false}
    let B : Set Bool := {true}
    ¬ Function.Injective f ∧
      f '' A = f '' B ∧ f '' A ⊆ f '' B ∧ ¬ A ⊆ B := by
  dsimp
  constructor
  · intro hf
    have h : false = true := hf rfl
    simp at h
  constructor
  · ext x
    simp
  constructor
  · intro x hx
    simp
  · intro h
    have : false ∈ ({true} : Set Bool) := h (by simp)
    simp at this

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Reindexing along one arrow, regarded as a functor between thin categories. -/
def reindexFunctor (P : SplitIndexedOrder C) {c d : C} (f : c ⟶ d) :
    P.Fiber d ⥤ P.Fiber c where
  obj := P.reindex f
  map h := homOfLE (P.reindex_mono f h.le)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Package the indexed poset as a genuine contravariant functor into `Cat`. -/
def toCatFunctor (P : SplitIndexedOrder C) : Cᵒᵖ ⥤ Cat.{w, w} where
  obj c := Cat.of (P.Fiber c.unop)
  map f := (reindexFunctor P f.unop).toCatHom
  map_id c := by
    apply Cat.Hom.ext
    apply CategoryTheory.Functor.ext (fun x => P.reindex_id c.unop x)
  map_comp f g := by
    apply Cat.Hom.ext
    apply CategoryTheory.Functor.ext (fun x => P.reindex_comp g.unop f.unop x)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The strict functor, promoted to the pseudofunctor expected by mathlib's
contravariant Grothendieck construction. -/
abbrev toCatPseudofunctor (P : SplitIndexedOrder C) :
    Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{w, w} :=
  (toCatFunctor P).toPseudoFunctor'

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The total category of the indexed order. -/
abbrev total (P : SplitIndexedOrder C) : Type _ :=
  Pseudofunctor.CoGrothendieck (toCatPseudofunctor P)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Projection of the total category to the original base. -/
abbrev projection (P : SplitIndexedOrder C) : total P ⥤ C :=
  Pseudofunctor.CoGrothendieck.forget (toCatPseudofunctor P)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The total object represented by `x` in the fiber over `c`. -/
abbrev totalObj (P : SplitIndexedOrder C) (c : C) (x : P.Fiber c) : total P :=
  { base := c, fiber := x }

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The canonical arrow from the reindexed object to the original object. -/
def cartesianLift (P : SplitIndexedOrder C) {c d : C} (f : c ⟶ d) (x : P.Fiber d) :
    totalObj P c (P.reindex f x) ⟶ totalObj P d x where
  base := f
  fiber := 𝟙 _

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The canonical reindexing arrow is strongly cartesian. -/
theorem cartesianLift_isStronglyCartesian (P : SplitIndexedOrder C)
    {c d : C} (f : c ⟶ d) (x : P.Fiber d) :
    (projection P).IsStronglyCartesian f (cartesianLift P f x) := by
  change (projection P).IsStronglyCartesian f
    (Pseudofunctor.CoGrothendieck.cartesianLift (F := toCatPseudofunctor P) x f)
  exact Pseudofunctor.CoGrothendieck.isStronglyCartesian_homCartesianLift
    (F := toCatPseudofunctor P) x f

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The projection is a fibration over the original base category. -/
theorem projection_isFibered (P : SplitIndexedOrder C) :
    (projection P).IsFibered := by
  infer_instance

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The chosen transport is exactly the domain of the canonical cartesian lift,
and that lift satisfies mathlib's cartesian universal property. -/
theorem reindex_is_cartesian_lift (P : SplitIndexedOrder C)
    {c d : C} (f : c ⟶ d) (x : P.Fiber d) :
    (projection P).IsCartesian f (cartesianLift P f x) ∧
      Pseudofunctor.CoGrothendieck.domainCartesianLift
        (F := toCatPseudofunctor P) x f = totalObj P c (P.reindex f x) := by
  constructor
  · letI : (projection P).IsStronglyCartesian f (cartesianLift P f x) :=
      cartesianLift_isStronglyCartesian P f x
    exact Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian
      (projection P) f (cartesianLift P f x)
  · rfl

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The original thin category maps to the standard fiber of the projection. -/
abbrev fiberFunctor (P : SplitIndexedOrder C) (c : C) :
    P.Fiber c ⥤ (projection P).Fiber c :=
  CategoryTheory.Functor.Fiber.inducedFunctor
    (Pseudofunctor.CoGrothendieck.comp_const (toCatPseudofunctor P) c)

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- The standard fiber category of the projection is equivalent to the original
partial order regarded as a thin category. -/
theorem fiberFunctor_isEquivalence (P : SplitIndexedOrder C) (c : C) :
    (fiberFunctor P c).IsEquivalence := by
  exact HasFibers.equiv c

-- LeanTest/HardProblems/GrothendieckFibration.lean
/-- Goal 4 in explicit categorical form. -/
noncomputable def fiberEquiv (P : SplitIndexedOrder C) (c : C) :
    P.Fiber c ≌ (projection P).Fiber c := by
  letI : (fiberFunctor P c).IsEquivalence := fiberFunctor_isEquivalence P c
  exact (fiberFunctor P c).asEquivalence

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The set of states reachable from a set of starting states. -/
def reachSet {X : Type u} (G : Set (X → X)) (S : Set X) : Set X :=
  {z | ∃ x ∈ S, Reach G x z}

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 1. `reachSet G` is a closure operator on `Set X`. -/
def reachClosure {X : Type u} (G : Set (X → X)) : ClosureOperator (Set X) where
  toFun := reachSet G
  monotone' := by
    intro S T hST z hz
    rcases hz with ⟨x, hxS, hxz⟩
    exact ⟨x, hST hxS, hxz⟩
  le_closure' := by
    intro S x hx
    exact ⟨x, hx, .refl⟩
  idempotent' := by
    intro S
    apply Set.Subset.antisymm
    · rintro z ⟨y, ⟨x, hx, hxy⟩, hyz⟩
      exact ⟨x, hx, hxy.trans hyz⟩
    · rintro z hz
      exact ⟨z, hz, .refl⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 2. A programmed transformation adds no reachability. -/
theorem reachSet_insert_programmed {X : Type u} (G : Set (X → X))
    {g : X → X} (hg : Programmed G g) (S : Set X) :
    reachSet (insert g G) S = reachSet G S := by
  apply Set.Subset.antisymm
  · rintro z ⟨x, hx, hreach⟩
    exact ⟨x, hx, hreach.insert_programmed hg⟩
  · rintro z ⟨x, hx, hreach⟩
    exact ⟨x, hx, by
      induction hreach with
      | refl => exact .refl
      | tail hstep hmem hz ih => exact .tail ih (Set.mem_insert_of_mem _ hmem) hz⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 3. The concrete two-state system `Bool`, with no old primitives,
initial state `false`, and the new constant-`true` primitive, strictly enlarges
reachable closure. -/
theorem exists_strict_enlargement :
    ∃ (X : Type) (G : Set (X → X)) (g : X → X) (S : Set X),
      reachSet G S ⊂ reachSet (insert g G) S := by
  refine ⟨Bool, ∅, (fun _ => true), {false}, ?_⟩
  constructor
  · rintro z ⟨x, hx, hreach⟩
    exact ⟨x, hx, by
      induction hreach with
      | refl => exact .refl
      | tail hstep hmem hz => exact False.elim hmem⟩
  · intro hreverse
    have htrue : true ∈ reachSet (insert (fun _ : Bool => true) ∅) {false} :=
      ⟨false, by simp,
        Reach.tail (g := fun _ : Bool => true) Reach.refl (by simp) rfl⟩
    have hold : true ∈ reachSet (∅ : Set (Bool → Bool)) {false} := hreverse htrue
    rcases hold with ⟨x, hx, hreach⟩
    have hxfalse : x = false := by simpa using hx
    subst x
    have hempty : ∀ z : Bool, Reach (∅ : Set (Bool → Bool)) false z → z = false := by
      intro z hz
      induction hz with
      | refl => rfl
      | tail hstep hmem heq => exact False.elim hmem
    have : true = false := hempty true hreach
    cases this

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Saturation of states under equality of observations. -/
def indistSaturation {S : Type u} {O : Type v} (observe : S → O)
    (T : Set S) : Set S :=
  {y | ∃ x ∈ T, Indist observe x y}

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 4. Saturation under observational indistinguishability is a closure
operator on `Set S`. -/
def indistClosure {S : Type u} {O : Type v} (observe : S → O) :
    ClosureOperator (Set S) where
  toFun := indistSaturation observe
  monotone' := by
    rintro A B h y ⟨x, hx, hxy⟩
    exact ⟨x, h hx, hxy⟩
  le_closure' := by
    intro A x hx
    exact ⟨x, hx, rfl⟩
  idempotent' := by
    intro A
    apply Set.Subset.antisymm
    · rintro y ⟨x, ⟨z, hz, hzx⟩, hxy⟩
      exact ⟨z, hz, hzx.trans hxy⟩
    · intro y hy
      exact ⟨y, hy, rfl⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 4'. If `coarse = k ∘ fine`, fine observational saturation is contained
in coarse observational saturation: a finer experiment separates at least as
many states. -/
theorem indistClosure_le_of_refines {S : Type u} {F : Type v} {Cc : Type w}
    (fine : S → F) (coarse : S → Cc) (k : F → Cc) (hk : coarse = k ∘ fine) :
    ∀ T : Set S, indistClosure fine T ⊆ indistClosure coarse T := by
  intro T y hy
  rcases hy with ⟨x, hx, hxy⟩
  refine ⟨x, hx, ?_⟩
  show coarse x = coarse y
  rw [hk]
  exact congrArg k hxy

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Pulling a hidden behavior back along the trajectory projection gives a
closure operator on behaviors. -/
def behavioralClosure {T : Type u} {W : Type v} {V : Type w} (f : W → V) :
    ClosureOperator (Behavior T W) where
  toFun B := {w | f ∘ w ∈ hide f B}
  monotone' := by
    rintro B C h w ⟨w', hw', heq⟩
    exact ⟨w', h hw', heq⟩
  le_closure' := by
    intro B w hw
    exact ⟨w, hw, rfl⟩
  idempotent' := by
    intro B
    apply Set.Subset.antisymm
    · rintro w ⟨w', ⟨w'', hw'', heq'⟩, heq⟩
      exact ⟨w'', hw'', heq'.trans heq⟩
    · intro w hw
      exact ⟨w, hw, rfl⟩

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Goal 5. Hiding after interconnection is always contained in interconnecting
after hiding. The displayed `Bool`/`Unit` example makes this inclusion strict,
so hiding is not a meet (lattice) homomorphism. -/
theorem hide_interconnect_subset_and_strict :
    (∀ {T W V : Type} (f : W → V) (B₁ B₂ : Behavior T W),
      hide f (interconnect B₁ B₂) ⊆ interconnect (hide f B₁) (hide f B₂)) ∧
    (let B₁ : Behavior Unit Bool := {w | w () = false}
     let B₂ : Behavior Unit Bool := {w | w () = true}
     hide (fun _ : Bool => ()) (interconnect B₁ B₂) ⊂
       interconnect (hide (fun _ : Bool => ()) B₁)
         (hide (fun _ : Bool => ()) B₂)) := by
  constructor
  · intro T W V f B₁ B₂ v hv
    rcases hv with ⟨w, ⟨hw₁, hw₂⟩, rfl⟩
    exact ⟨⟨w, hw₁, rfl⟩, ⟨w, hw₂, rfl⟩⟩
  · dsimp
    constructor
    · intro v hv
      rcases hv with ⟨w, ⟨hw₁, hw₂⟩, rfl⟩
      exact ⟨⟨w, hw₁, rfl⟩, ⟨w, hw₂, rfl⟩⟩
    · intro hreverse
      let v : Unit → Unit := fun _ => ()
      have hv : v ∈ interconnect
          (hide (fun _ : Bool => ()) {w : Unit → Bool | w () = false})
          (hide (fun _ : Bool => ()) {w : Unit → Bool | w () = true}) := by
        constructor
        · exact ⟨(fun _ => false), rfl, rfl⟩
        · exact ⟨(fun _ => true), rfl, rfl⟩
      have hv' := hreverse hv
      rcases hv' with ⟨w, ⟨hwf, hwt⟩, _⟩
      simp only [Set.mem_setOf_eq] at hwf hwt
      rw [hwf] at hwt
      contradiction

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- A reindexing order homomorphism commutes with two fiberwise closures when
the two possible composites agree pointwise. -/
def ReindexCommutes {P : Type u} {Q : Type v} [Preorder P] [Preorder Q]
    (r : Q →o P) (cQ : ClosureOperator Q) (cP : ClosureOperator P) : Prop :=
  ∀ x, r (cQ x) = cP (r x)

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The closure on `Set Bool` that adjoins `false`. -/
def addFalseClosure : ClosureOperator (Set Bool) where
  toFun S := S ∪ {false}
  monotone' := by
    intro A B h x hx
    exact hx.elim (fun hxA => Or.inl (h hxA)) Or.inr
  le_closure' := by
    intro A x hx
    exact Or.inl hx
  idempotent' := by
    intro A
    ext x
    simp only [Set.mem_union, Set.mem_singleton_iff]
    tauto

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- Reindexing by inverse image along the map `Unit → Bool` selecting `false`
does not commute with `addFalseClosure` and the identity closure on `Set Unit`.
Both carriers are nonempty, nontrivial finite posets. -/
theorem reindex_closure_need_not_commute :
    let r : Set Bool →o Set Unit :=
      { toFun := Set.preimage (fun _ : Unit => false)
        monotone' := by intro A B h; exact Set.preimage_mono h }
    ¬ ReindexCommutes r addFalseClosure (ClosureOperator.id (Set Unit)) := by
  intro r h
  have heq := h (∅ : Set Bool)
  have hunit : () ∈ r (addFalseClosure (∅ : Set Bool)) := Or.inr rfl
  rw [heq] at hunit
  exact hunit

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The strict enlargement of Goal 3, restated with its witness in the
statement rather than behind an existential: adjoining the constant-`true`
move to the empty move set strictly enlarges what is reachable from
`{false}`. -/
theorem reachSet_insert_const_true_strict :
    reachSet (∅ : Set (Bool → Bool)) {false} ⊂
      reachSet (insert (fun _ => true) (∅ : Set (Bool → Bool))) {false} := by
  constructor
  · rintro z ⟨x, hx, h⟩
    refine ⟨x, hx, ?_⟩
    induction h with
    | refl => exact Reach.refl
    | tail _ hg hz ih => exact Reach.tail ih (Set.mem_insert_of_mem _ hg) hz
  · intro hrev
    have htrue : true ∈
        reachSet (insert (fun _ => true) (∅ : Set (Bool → Bool))) {false} :=
      ⟨false, rfl, Reach.tail Reach.refl (Set.mem_insert _ _) rfl⟩
    rcases hrev htrue with ⟨x, hx, h⟩
    cases h with
    | refl => simp at hx
    | tail _ hg _ => simp at hg

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `Reach` is the project's `Reach`, definitionally. -/
theorem reach_agrees {X : Type u} (G : Set (X → X)) (x z : X) :
    ClosureUnification.Reach G x z ↔ HardProblems.Reach G x z := by
  constructor
  · intro h
    induction h with
    | refl => exact HardProblems.Reach.refl
    | tail hxy hg hz ih => exact HardProblems.Reach.tail ih hg hz
  · intro h
    induction h with
    | refl => exact ClosureUnification.Reach.refl
    | tail hxy hg hz ih => exact ClosureUnification.Reach.tail ih hg hz

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `Indist` is `InformationOrder.Indist`, definitionally. -/
theorem indist_agrees {S : Type u} {O : Type v} (observe : S → O) (x y : S) :
    ClosureUnification.Indist observe x y ↔
      InformationOrder.Indist observe x y :=
  Iff.rfl

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `hide` is `Behavioral.hide`, definitionally. -/
theorem hide_agrees {T : Type u} {W : Type v} {V : Type w}
    (f : W → V) (B : ClosureUnification.Behavior T W) :
    ClosureUnification.hide f B = Behavioral.hide f B := by
  rfl

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `Programmed` is the project's `Programmed`: both quantify the
respective `Reach`, and `reach_agrees` bridges those. -/
theorem programmed_agrees {X : Type u} (G : Set (X → X)) (g : X → X) :
    ClosureUnification.Programmed G g ↔ HardProblems.Programmed G g := by
  constructor
  · intro h y
    exact (reach_agrees G y (g y)).mp (h y)
  · intro h y
    exact (reach_agrees G y (g y)).mpr (h y)

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `RobustActions` is `InformationOrder.RobustActions`,
definitionally. -/
theorem robustActions_agrees {S : Type u} {O : Type v} {A : Type w}
    (observe : S → O) (Acceptable : S → A → Prop) (x : S) :
    ClosureUnification.RobustActions observe Acceptable x =
      InformationOrder.RobustActions observe Acceptable x :=
  rfl

-- LeanTest/HardProblems/BoundaryClosures.lean
/-- The local `interconnect` is `Behavioral.interconnect`, definitionally. -/
theorem interconnect_agrees {T : Type u} {W : Type v}
    (B₁ B₂ : ClosureUnification.Behavior T W) :
    ClosureUnification.interconnect B₁ B₂ = Behavioral.interconnect B₁ B₂ :=
  rfl

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Attainable-performance regions over a performance space `P`, composing by
union. -/
abbrev RegionMonoid (P : Type u) := Set P

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 1': the Grothendieck group of every commutative idempotent monoid is
trivial. -/
theorem grothendieckGroup_subsingleton_of_idempotent
    (M : Type u) [CommMonoid M] (hidem : ∀ a : M, a * a = a) :
    Subsingleton (GrothendieckGroup M) := by
  refine ⟨fun x y => ?_⟩
  -- We'll show all elements equal GrothendieckGroup.of 1
  suffices ∀ z : GrothendieckGroup M, z = GrothendieckGroup.of 1 by rw [this x, this y]
  intro z
  -- Use Quot.induction_on to work with representatives
  induction z using Quot.induction_on with
  | h p => 
    -- p : M × ⊤, need to show Quot.mk oreEqv p = 1
    let ⟨a, b⟩ := p
    -- Need to show Quot.mk oreEqv (a, b) = GrothendieckGroup.of 1
    -- First show GrothendieckGroup.of 1 = Quot.mk oreEqv (1, 1)
    have of_one_eq : GrothendieckGroup.of 1 = Quot.mk (OreLocalization.oreEqv ⊤ M) (1, 1) := by
      rfl
    rw [of_one_eq]
    -- Now use Quot.eq
    apply Quot.sound
    unfold OreLocalization.oreEqv
    -- Need ∃ u v, u • (1,1).1 = v • (a,b).1 ∧ u * (1,1).2 = v * (a,b).2
    -- i.e., ∃ u v, u = v * a ∧ u = v * b
    -- Take v = a * b, u = a * b
    refine ⟨⟨a * b, ?_⟩, a * b, ?_⟩
    · simp
    · constructor
      · -- ⟨a * ↑b, _⟩ • 1 = (a * ↑b) • a
        simp only [Submonoid.mk_smul, smul_eq_mul]
        rw [mul_one]
        conv_rhs => rw [mul_assoc, mul_comm, mul_assoc, hidem]
        rw [mul_comm]
      · -- ↑⟨a * ↑b, _⟩ * ↑(1,1).2 = a * ↑b * ↑(a,b).2
        simp [mul_one]
        rw [mul_assoc, hidem]

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 1: the Grothendieck group of the region monoid is trivial, for every
performance type `P` (including the empty type). -/
theorem grothendieckGroup_regionMonoid_subsingleton (P : Type u) :
    Subsingleton (GrothendieckGroup (RegionMonoid P)) := by
  apply grothendieckGroup_subsingleton_of_idempotent
  exact Set.union_self

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 2: canonical images are equal exactly when the two elements become
equal after multiplying by a common slack element. -/
theorem grothendieckGroup_of_eq_iff (M : Type u) [CommMonoid M] (a b : M) :
    GrothendieckGroup.of a = GrothendieckGroup.of b ↔
      ∃ c : M, a * c = b * c := by
  change Localization.mk a 1 = Localization.mk b 1 ↔ _
  rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
  simp only [Submonoid.coe_one, one_mul]
  constructor
  · rintro ⟨c, hc⟩
    exact ⟨c, by simpa [mul_comm] using hc⟩
  · rintro ⟨c, hc⟩
    exact ⟨⟨c, Submonoid.mem_top c⟩, by simpa [mul_comm] using hc⟩

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 3: for a cancellative cost monoid, the canonical map is injective. -/
theorem toGrothendieckGroup_injective_of_cancel
    (M : Type u) [CancelCommMonoid M] :
    Function.Injective (GrothendieckGroup.of : M → GrothendieckGroup M) := by
  exact GrothendieckGroup.of_injective

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 4: the concrete regions `{true}` and `{false}` are distinct but have
the same image in the Grothendieck group. -/
theorem concrete_regions_collapse :
    ({true} : RegionMonoid Bool) ≠ {false} ∧
      GrothendieckGroup.of ({true} : RegionMonoid Bool) =
        GrothendieckGroup.of ({false} : RegionMonoid Bool) := by
  haveI : Subsingleton (GrothendieckGroup (RegionMonoid Bool)) :=
    grothendieckGroup_regionMonoid_subsingleton Bool
  refine ⟨?_, Subsingleton.elim _ _⟩
  simp [Set.eq_singleton_iff_unique_mem]

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 5a: adding any cost to the absorbing overflow value does not change
its canonical image. -/
theorem withTop_cost_top_add_image (a : WithTop ℕ) :
    GrothendieckAddGroup.of (⊤ + a) =
      GrothendieckAddGroup.of (⊤ : WithTop ℕ) := by
  simp

-- LeanTest/HardProblems/KTheoryCollapse.lean
/-- Goal 5: because `⊤` is absorbing, the entire Grothendieck group of
`WithTop ℕ` is trivial, not merely the part at or above the cap. -/
theorem saturating_costs_grothendieckAddGroup_subsingleton :
    Subsingleton (GrothendieckAddGroup (WithTop ℕ)) := by
  have hof : ∀ a : WithTop ℕ, GrothendieckAddGroup.of a = 0 := by
    intro a
    apply add_right_cancel (b := GrothendieckAddGroup.of (⊤ : WithTop ℕ))
    rw [← map_add]
    simp
  constructor
  intro x y
  suffices ∀ z : GrothendieckAddGroup (WithTop ℕ), z = 0 by rw [this x, this y]
  intro z
  induction z using AddLocalization.induction_on with
  | _ p =>
    have h : AddLocalization.mk p.1 p.2 +
        GrothendieckAddGroup.of (p.2 : WithTop ℕ) =
        GrothendieckAddGroup.of p.1 := by
      change AddLocalization.mk p.1 p.2 +
          AddLocalization.mk (p.2 : WithTop ℕ) 0 = AddLocalization.mk p.1 0
      rw [AddLocalization.mk_add, AddLocalization.mk_eq_mk_iff,
        AddLocalization.r_iff_exists]
      use 0
      simp [add_comm]
    rw [hof _, hof _] at h
    simpa using h

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal A1. If every value category of a pseudofunctor from a locally
discrete base is thin and skeletal, then the pseudofunctor preserves
identities on the nose: the underlying functor of `F.map (id)` equals the
identity functor. State with whatever locally-discrete encoding of the base
1-category `C` mathlib's `Pseudofunctor` needs. -/
theorem map_id_eq_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩)) (c : C) :
    F.map (𝟙 ⟨c⟩) = 𝟙 (F.obj ⟨c⟩) := by
  letI := hthin c
  apply Cat.Hom.ext
  exact Functor.eq_of_iso (hskel c) (Cat.Hom.toNatIso (F.mapId ⟨c⟩))

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal A2. Same hypotheses: composition is preserved on the nose. -/
theorem map_comp_eq_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩))
    {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
    F.map (⟨f⟩ ≫ ⟨g⟩ : (⟨a⟩ : LocallyDiscrete C) ⟶ ⟨c⟩) =
      F.map ⟨f⟩ ≫ F.map ⟨g⟩ := by
  letI := hthin c
  apply Cat.Hom.ext
  exact Functor.eq_of_iso (hskel c) (Cat.Hom.toNatIso (F.mapComp ⟨f⟩ ⟨g⟩))

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal A3. The comparison isomorphisms themselves are the identity
2-cells modulo the equalities above: each `mapComp` component is an
`eqToIso`. State the cleanest correct version; if a different phrasing of
"the comparison data is trivial" is more natural in mathlib's API, prove
that and rename. -/
theorem mapComp_eqToIso_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩))
    {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
    F.mapComp ⟨f⟩ ⟨g⟩ =
      eqToIso (map_comp_eq_of_thin_skeletal F hthin hskel f g) := by
  ext X
  have thin := hthin c
  exact Subsingleton.elim _ _

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The cup-product 2-cocycle on `ZMod 2`: `c h h' = h * h'`. Its class
generates the degree-2 cohomology of Z/2 with Z/2 coefficients, and is the
obstruction separating the two extensions of Z/2 by Z/2. -/
def twoCocycle (h h' : ZMod 2) : ZMod 2 := h * h'

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal B1. The cocycle identity, with trivial action:
`c(h',h'') - c(h+h',h'') + c(h,h'+h'') - c(h,h') = 0`. -/
theorem twoCocycle_isCocycle (h h' h'' : ZMod 2) :
    twoCocycle h' h'' - twoCocycle (h + h') h''
      + twoCocycle h (h' + h'') - twoCocycle h h' = 0 := by
  simp only [twoCocycle]
  ring

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal B2. Not a coboundary: no 1-cochain `φ` has
`c(h,h') = φ h' - φ (h+h') + φ h` everywhere. This is the precise sense in
which the comparison data below cannot be normalized away. -/
theorem twoCocycle_not_coboundary :
    ¬ ∃ φ : ZMod 2 → ZMod 2,
      ∀ h h', twoCocycle h h' = φ h' - φ (h + h') + φ h := by
  decide

-- LeanTest/HardProblems/TwistObstruction.lean
def twistElementIso (x : ZMod 2) :
    (SingleObj.star TwistGroup : TwistFibre) ≅ SingleObj.star TwistGroup :=
  Iso.mk (Multiplicative.ofAdd x) (Multiplicative.ofAdd (-x))
    (by change -x + x = 0; exact neg_add_cancel x)
    (by change x + -x = 0; exact add_neg_cancel x)

-- LeanTest/HardProblems/TwistObstruction.lean
def twistNatIso (x : ZMod 2) : 𝟭 TwistFibre ≅ 𝟭 TwistFibre :=
  NatIso.ofComponents (fun _ => twistElementIso x) (by
    intro X Y f
    cases X
    cases Y
    first
      | exact mul_comm f (Multiplicative.ofAdd x)
      | exact mul_comm (Multiplicative.ofAdd x) f)

-- LeanTest/HardProblems/TwistObstruction.lean
def twistIdHom : (Cat.of TwistFibre) ⟶ Cat.of TwistFibre :=
  (𝟭 TwistFibre).toCatHom

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The comparison 2-isomorphism whose distinguished component is literally
`twoCocycle h h'`.  The right-unitor only reconciles the wrapper used by
`Cat` for the composite of two identity functors. -/
def twistComparison (h h' : ZMod 2) :
    twistIdHom ≅ twistIdHom ≫ twistIdHom :=
  Cat.Hom.isoMk
    (twistNatIso (twoCocycle h h') ≪≫ (Functor.rightUnitor (𝟭 TwistFibre)).symm)

-- LeanTest/HardProblems/TwistObstruction.lean
noncomputable def twistedPseudofunctor :
    Pseudofunctor (LocallyDiscrete TwistBase) Cat :=
  LocallyDiscrete.mkPseudofunctor
    (fun _ => Cat.of TwistFibre)
    (fun _ => twistIdHom)
    (fun _ => Cat.Hom.isoMk (Iso.refl _))
    (fun f g => by
      cases ‹TwistBase›
      cases ‹TwistBase›
      cases ‹TwistBase›
      change TwistGroup at f g
      exact twistComparison (Multiplicative.toAdd f) (Multiplicative.toAdd g))
    (by
      intros b₀ b₁ b₂ b₃ f g h
      cases b₀; cases b₁; cases b₂; cases b₃
      show _
      simp only [Cat.of]
      show _
      change Multiplicative (ZMod 2) at f g h
      have hc := twoCocycle_isCocycle
        (Multiplicative.toAdd f) (Multiplicative.toAdd g) (Multiplicative.toAdd h)
      fin_cases f <;> fin_cases g <;> fin_cases h <;> simp_all [twistComparison, twistNatIso,
        twistElementIso, NatIso.ofComponents, Functor.rightUnitor, Bicategory.associator] <;>
        ext <;> simp_all [twistIdHom, twoCocycle] <;> norm_cast
      all_goals rename_i X
      all_goals cases X
      all_goals change (_ : TwistGroup) = _
      all_goals rfl)
    (by
      intros b₀ b₁ f
      cases b₀; cases b₁
      change Multiplicative (ZMod 2) at f
      fin_cases f <;> simp_all [twistComparison, twistNatIso,
        twistElementIso, NatIso.ofComponents] <;>
        ext <;> simp_all [twistIdHom, twoCocycle] <;> norm_cast)
    (by
      intros b₀ b₁ f
      cases b₀; cases b₁
      change Multiplicative (ZMod 2) at f
      fin_cases f <;> simp_all [twistComparison, twistNatIso,
        twistElementIso, NatIso.ofComponents, Functor.rightUnitor] <;>
        ext <;> simp_all [twistIdHom, twoCocycle] <;> norm_cast)

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The comparison of `twistedPseudofunctor` is the cocycle comparison by
construction. -/
theorem twistedPseudofunctor_mapComp (h h' : TwistGroup) :
    twistedPseudofunctor.mapComp
        (⟨h⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶ ⟨SingleObj.star TwistGroup⟩)
        (⟨h'⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶ ⟨SingleObj.star TwistGroup⟩) =
      twistComparison (Multiplicative.toAdd h) (Multiplicative.toAdd h') := by
  rfl

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Goal B4. No re-choice of comparison components has coboundary equal to
(the negative of, equivalently in `ZMod 2`, equal to) the coefficients of the
actual comparison cells of `twistedPseudofunctor`. -/
theorem twist_is_essential :
    (∀ h h' : TwistGroup,
      twistedPseudofunctor.mapComp
          (⟨h⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶
            ⟨SingleObj.star TwistGroup⟩)
          (⟨h'⟩ : (⟨SingleObj.star TwistGroup⟩ : LocallyDiscrete TwistBase) ⟶
            ⟨SingleObj.star TwistGroup⟩) =
        twistComparison (Multiplicative.toAdd h) (Multiplicative.toAdd h')) ∧
    ¬ ∃ φ : ZMod 2 → ZMod 2,
      ∀ h h', twoCocycle h h' = φ h' - φ (h + h') + φ h := by
  exact ⟨twistedPseudofunctor_mapComp, twoCocycle_not_coboundary⟩

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The identity comparison is also equality-induced, completing the pair:
with thin skeletal values, both comparison isomorphisms of a pseudofunctor
are `eqToIso`, which is the full content of "strict on the nose". -/
theorem mapId_eqToIso_of_thin_skeletal
    (F : Pseudofunctor (LocallyDiscrete C) Cat.{w, w})
    (hthin : ∀ c : C, Quiver.IsThin (F.obj ⟨c⟩))
    (hskel : ∀ c : C, Skeletal (F.obj ⟨c⟩)) (c : C) :
    F.mapId ⟨c⟩ = eqToIso (map_id_eq_of_thin_skeletal F hthin hskel c) := by
  ext X
  have thin := hthin c
  exact Subsingleton.elim _ _

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Fibres of the book's indexed order are thin: their homs are proofs. -/
theorem toCatPseudofunctor_fibre_thin (P : SplitIndexedOrder.{v, u, w} C)
    (c : Cᵒᵖ) : Quiver.IsThin ((toCatPseudofunctor P).obj ⟨c⟩) := by
  show Quiver.IsThin (P.Fiber c.unop)
  intro X Y
  exact ⟨fun f g => Subsingleton.elim f g⟩

-- LeanTest/HardProblems/TwistObstruction.lean
/-- Fibres of the book's indexed order are skeletal: an isomorphism gives
inequalities both ways, and antisymmetry finishes. -/
theorem toCatPseudofunctor_fibre_skeletal (P : SplitIndexedOrder.{v, u, w} C)
    (c : Cᵒᵖ) : Skeletal ((toCatPseudofunctor P).obj ⟨c⟩) := by
  show Skeletal (P.Fiber c.unop)
  rintro X Y ⟨i⟩
  exact le_antisymm (leOfHom i.hom) (leOfHom i.inv)

-- LeanTest/HardProblems/TwistObstruction.lean
/-- The splitting of the book's indexed order was forced: its composition
comparison is equality-induced. -/
theorem splitIndexedOrder_mapComp_eqToIso (P : SplitIndexedOrder.{v, u, w} C)
    {a b c : Cᵒᵖ} (f : a ⟶ b) (g : b ⟶ c) :
    (toCatPseudofunctor P).mapComp ⟨f⟩ ⟨g⟩ =
      eqToIso (map_comp_eq_of_thin_skeletal (toCatPseudofunctor P)
        (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P)
        f g) :=
  mapComp_eqToIso_of_thin_skeletal (toCatPseudofunctor P)
    (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P) f g

-- LeanTest/HardProblems/TwistObstruction.lean
/-- And its identity comparison likewise. -/
theorem splitIndexedOrder_mapId_eqToIso (P : SplitIndexedOrder.{v, u, w} C)
    (c : Cᵒᵖ) :
    (toCatPseudofunctor P).mapId ⟨c⟩ =
      eqToIso (map_id_eq_of_thin_skeletal (toCatPseudofunctor P)
        (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P)
        c) :=
  mapId_eqToIso_of_thin_skeletal (toCatPseudofunctor P)
    (toCatPseudofunctor_fibre_thin P) (toCatPseudofunctor_fibre_skeletal P) c