Convex Analysis (Rockafellar, 1970) -- Chapter 04 -- Section 22 -- Part 6

section Chap04section Section22

Helper for Text 22.3.6: rewrite the transpose multiplier equation as the corresponding weighted sum of the rows of Unknown identifier `A`A.

lemma helperForText_22_3_6_transposeMulVec_eq_rowCombination
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (l : Fin m → ℝ) :
    A.transpose.mulVec l = ∑ i : Fin m, l i • A i := by
  -- Compare both sides coordinatewise so each component becomes the same finite sum.
  ext j
  simp [Matrix.mulVec, dotProduct, Pi.smul_apply, smul_eq_mul, mul_comm]

Helper for Text 22.3.6: unpack the matrix inequality system into the rowwise dot-product inequalities used in Theorem 22.1.

lemma helperForText_22_3_6_primalSystem_iff_rowForm
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    (∃ x : Fin n → ℝ, A.mulVec x ≤ a) ↔
      (∃ x : Fin n → ℝ, ∀ i : Fin m, dotProduct (A i) x ≤ a i) := by
  constructor
  · rintro ⟨x, hx⟩
    -- Evaluate the pointwise inequality at each row index.
    refine ⟨x, ?_⟩
    intro i
    simpa [Matrix.mulVec, dotProduct] using hx i
  · rintro ⟨x, hx⟩
    -- Repackage the rowwise inequalities as the pointwise vector inequality.
    refine ⟨x, ?_⟩
    intro i
    simpa [Matrix.mulVec, dotProduct] using hx i

Helper for Text 22.3.6: identify the matrix dual certificate with the row-combination certificate from Theorem 22.1.

lemma helperForText_22_3_6_dualCertificate_iff
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    (∃ l : Fin m → ℝ, 0 ≤ l ∧ A.transpose.mulVec l = 0 ∧ dotProduct a l < 0) ↔
      (∃ l : Fin m → ℝ, 0 ≤ l ∧ (∑ i, l i • A i) = 0 ∧ (∑ i, l i * a i) < 0) := by
  constructor
  · rintro ⟨l, hl, htranspose, hdot⟩
    -- Rewrite the matrix equation and scalar pairing into the row-family form.
    refine ⟨l, hl, ?_, ?_⟩
    · simpa [helperForText_22_3_6_transposeMulVec_eq_rowCombination] using htranspose
    · simpa [dotProduct, mul_comm] using hdot
  · rintro ⟨l, hl, hrows, hsum⟩
    -- The same rewrites convert the row-family certificate back to matrix notation.
    refine ⟨l, hl, ?_, ?_⟩
    · simpa [helperForText_22_3_6_transposeMulVec_eq_rowCombination] using hrows
    · simpa [dotProduct, mul_comm] using hsum

-- Proof sketch: this is the matrix form of the basic Farkas alternative. A solution `x`
-- of `A x ≤ a` and a nonnegative multiplier vector `λ` with `Aᵀ λ = 0` cannot coexist,
-- because multiplying the inequalities by `λ` and summing gives
-- `0 = ⟪x, Aᵀ λ⟫ ≤ ⟪a, λ⟫`, contradicting `⟪a, λ⟫ < 0`. Existence of one alternative
-- follows by rewriting Theorem 22.1 in matrix notation using the rows of `A`.

Text 22.3.6: Given failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `A`A ∈ ℝ^{Unknown identifier `m`m × Unknown identifier `n`n} and failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `a`a ∈ ℝ^Unknown identifier `m`m, exactly one of the following two systems has a solution: (Unknown identifier `P`P) Unknown identifier `A`sorry * sorry ≤ sorry : PropA * Unknown identifier `x`x ≤ Unknown identifier `a`a; (Unknown identifier `D`D) there exists with and .

theorem farkasAlternative_matrix_linearInequalities
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    ((∃ x : Fin n → ℝ, A.mulVec x ≤ a) ∨
        ∃ l : Fin m → ℝ, 0 ≤ l ∧ A.transpose.mulVec l = 0 ∧ dotProduct a l < 0) ∧
      ¬((∃ x : Fin n → ℝ, A.mulVec x ≤ a) ∧
        ∃ l : Fin m → ℝ, 0 ≤ l ∧ A.transpose.mulVec l = 0 ∧ dotProduct a l < 0) := by
  -- Route correction: do not reprove Farkas' lemma here; translate the matrix statement
  -- into the row-family statement already established in Theorem 22.1.
  simpa [helperForText_22_3_6_primalSystem_iff_rowForm,
    helperForText_22_3_6_dualCertificate_iff] using
    farkasAlternative_linearInequalities (a := fun i => A i) (α := a)

-- Proof sketch: this is Farkas' alternative; show the primal and dual systems
-- cannot both be solvable, then use the separating-hyperplane result for the cone
-- generated by the columns of `A` and the vector `a` to prove one of them is.

Helper for Text 22.3.8: the column family of a matrix Unknown identifier `A`A, viewed as vectors in ℝ ^ sorry : Typeℝ^Unknown identifier `m`m.

abbrev helperForText_22_3_8_columnFamily
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : Fin n → (Fin m → ℝ) :=
  fun j i => A i j

Helper for Text 22.3.8: rewrite Unknown identifier `A.mulVec`A.mulVec x as the nonnegative combination of the columns of Unknown identifier `A`A with coefficients Unknown identifier `x`x.

lemma helperForText_22_3_8_mulVec_eq_columnCombination
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (x : Fin n → ℝ) :
    A.mulVec x = ∑ j : Fin n, x j • helperForText_22_3_8_columnFamily A j := by
  -- Compare coordinates so both sides reduce to the same finite sum.
  ext i
  simp [helperForText_22_3_8_columnFamily, Matrix.mulVec, dotProduct, Pi.smul_apply,
    smul_eq_mul, mul_comm]

Helper for Text 22.3.8: the primal matrix system is exactly the homogeneous consequence statement for the column family of Unknown identifier `A`A.

lemma helperForText_22_3_8_primal_iff_homogeneousConsequence
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    (∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x = a) ↔
      IsConsequenceOfLinearInequalitySystem a 0
        (helperForText_22_3_8_columnFamily A) (fun _ : Fin n => (0 : ℝ)) := by
  -- Route correction: prove the primal branch by reusing Corollary 22.3.1 on the columns
  -- of `A`, rather than starting a fresh separation argument in matrix notation.
  rw [homogeneousLinearInequality_isConsequence_iff_nonnegative_combination]
  constructor
  · rintro ⟨x, hx_nonneg, hx_eq⟩
    -- Rewrite the matrix product as a column combination matching the consequence theorem.
    refine ⟨x, hx_nonneg, ?_⟩
    calc
      ∑ j : Fin n, x j • helperForText_22_3_8_columnFamily A j = A.mulVec x := by
        symm
        exact helperForText_22_3_8_mulVec_eq_columnCombination A x
      _ = a := hx_eq
  · rintro ⟨x, hx_nonneg, hx_eq⟩
    -- The same rewrite converts the consequence certificate back to the matrix equation.
    refine ⟨x, hx_nonneg, ?_⟩
    calc
      A.mulVec x = ∑ j : Fin n, x j • helperForText_22_3_8_columnFamily A j := by
        exact helperForText_22_3_8_mulVec_eq_columnCombination A x
      _ = a := hx_eq

Helper for Text 22.3.8: the dual witness is exactly the negation of the homogeneous consequence statement for the columns of Unknown identifier `A`A.

lemma helperForText_22_3_8_dual_iff_not_homogeneousConsequence
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    (∃ w : Fin m → ℝ, A.transpose.mulVec w ≤ 0 ∧ 0 < dotProduct a w) ↔
      ¬ IsConsequenceOfLinearInequalitySystem a 0
        (helperForText_22_3_8_columnFamily A) (fun _ : Fin n => (0 : ℝ)) := by
  constructor
  · rintro ⟨w, hw_matrix, hw_pos⟩ hconsequence
    -- Convert the transpose inequality into the columnwise system hypotheses.
    have hw_columns :
        ∀ j : Fin n, dotProduct (helperForText_22_3_8_columnFamily A j) w ≤ 0 := by
      intro j
      simpa [helperForText_22_3_8_columnFamily, Matrix.mulVec, dotProduct, mul_comm] using hw_matrix j
    -- Consequence would force `⟪a,w⟫ ≤ 0`, contradicting the strict positivity witness.
    have ha_nonpos : dotProduct a w ≤ 0 := hconsequence hw_columns
    linarith
  · intro hnot_consequence
    classical
    -- If no dual witness existed, every columnwise-feasible `w` would satisfy `⟪a,w⟫ ≤ 0`.
    by_contra hno_dual
    apply hnot_consequence
    intro w hw_columns
    have hw_matrix : A.transpose.mulVec w ≤ 0 := by
      intro j
      simpa [helperForText_22_3_8_columnFamily, Matrix.mulVec, dotProduct, mul_comm] using hw_columns j
    have hnot_pos : ¬ 0 < dotProduct a w := by
      intro hw_pos
      exact hno_dual ⟨w, hw_matrix, hw_pos⟩
    exact le_of_not_gt hnot_pos

Text 22.3.8: Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `A`A ∈ ℝ^{Unknown identifier `m`m × Unknown identifier `n`n} and failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `a`a ∈ ℝ^Unknown identifier `m`m. Exactly one of the following two systems has a solution: (Unknown identifier `P`P) there exists Unknown identifier `x`sorry ≥ 0 : Propx ≥ 0 with Unknown identifier `A`sorry * sorry = sorry : PropA * Unknown identifier `x`x = Unknown identifier `a`a; (Unknown identifier `D`D) there exists Unknown identifier `w`w with and .

theorem farkasAlternative_nonnegative_matrix
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    ((∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x = a) ∨
        ∃ w : Fin m → ℝ, A.transpose.mulVec w ≤ 0 ∧ 0 < dotProduct a w) ∧
      ¬((∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x = a) ∧
        ∃ w : Fin m → ℝ, A.transpose.mulVec w ≤ 0 ∧ 0 < dotProduct a w) := by
  -- Route correction: identify the primal system with a homogeneous consequence statement
  -- for the columns of `A`, and identify the dual system with its negation.
  let consequence : Prop :=
    IsConsequenceOfLinearInequalitySystem a 0
      (helperForText_22_3_8_columnFamily A) (fun _ : Fin n => (0 : ℝ))
  have hprimal :
      (∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x = a) ↔ consequence := by
    -- The primal equivalence is exactly the column-family reformulation above.
    simpa [consequence] using helperForText_22_3_8_primal_iff_homogeneousConsequence A a
  have hdual :
      (∃ w : Fin m → ℝ, A.transpose.mulVec w ≤ 0 ∧ 0 < dotProduct a w) ↔ ¬ consequence := by
    -- The dual branch packages the failure of that consequence.
    simpa [consequence] using
      helperForText_22_3_8_dual_iff_not_homogeneousConsequence A a
  by_cases hconsequence : consequence
  · -- In the consequence branch, the primal system is solvable and the dual is impossible.
    have hprimalSolvable : ∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x = a := hprimal.2 hconsequence
    refine ⟨Or.inl hprimalSolvable, ?_⟩
    rintro ⟨hprimal', hdual'⟩
    exact (hdual.1 hdual') hconsequence
  · -- In the negated branch, the dual witness exists and the primal system is impossible.
    have hdualSolvable : ∃ w : Fin m → ℝ, A.transpose.mulVec w ≤ 0 ∧ 0 < dotProduct a w :=
      hdual.2 hconsequence
    refine ⟨Or.inr hdualSolvable, ?_⟩
    rintro ⟨hprimal', hdual'⟩
    exact hconsequence (hprimal.1 hprimal')

-- Proof sketch: adjoin a nonnegative slack vector `s ≥ 0` and rewrite `A x ≤ a` as
-- `A x + s = a` with `(x, s) ≥ 0`. Applying the nonnegative equality-form alternative to
-- this enlarged system yields the stated dual conditions `w ≥ 0`, `Aᵀ w ≥ 0`, and
-- `⟪a, w⟫ < 0`.

Helper for Text 22.3.9: the slack-variable matrix used to convert Unknown identifier `A`sorry ≤ sorry : PropA x ≤ Unknown identifier `a`a into a nonnegative equality system.

abbrev helperForText_22_3_9_augmentedMatrix
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : Matrix (Fin m) (Fin (n + m)) ℝ :=
  fun i => Fin.addCases (fun j : Fin n => A i j) (fun k : Fin m => if i = k then 1 else 0)

Helper for Text 22.3.9: multiplying the augmented slack matrix by (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `s`s) gives Unknown identifier `A`sorry + sorry : ?m.5A x + Unknown identifier `s`s.

lemma helperForText_22_3_9_augmentedMatrix_mulVec
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (x : Fin n → ℝ) (s : Fin m → ℝ) :
    (helperForText_22_3_9_augmentedMatrix A).mulVec (Fin.addCases x s) = A.mulVec x + s := by
  -- Split the sum over `Fin (n + m)` into the original coordinates and the slack block.
  ext i
  calc
    (helperForText_22_3_9_augmentedMatrix A).mulVec (Fin.addCases x s) i
        = ∑ j : Fin (n + m),
            helperForText_22_3_9_augmentedMatrix A i j * Fin.addCases x s j := by
            simp [Matrix.mulVec, dotProduct]
    _ = (∑ j : Fin n,
            helperForText_22_3_9_augmentedMatrix A i (Fin.castAdd m j) *
              Fin.addCases x s (Fin.castAdd m j)) +
          ∑ k : Fin m,
            helperForText_22_3_9_augmentedMatrix A i (Fin.natAdd n k) *
              Fin.addCases x s (Fin.natAdd n k) := by
            rw [show (∑ j : Fin (n + m),
                helperForText_22_3_9_augmentedMatrix A i j * Fin.addCases x s j) =
                ∑ t : Fin n ⊕ Fin m,
                  helperForText_22_3_9_augmentedMatrix A i (finSumFinEquiv t) *
                    Fin.addCases x s (finSumFinEquiv t) by
                  symm
                  exact Fintype.sum_equiv finSumFinEquiv
                    (fun t : Fin n ⊕ Fin m =>
                      helperForText_22_3_9_augmentedMatrix A i (finSumFinEquiv t) *
                        Fin.addCases x s (finSumFinEquiv t))
                    (fun j : Fin (n + m) =>
                      helperForText_22_3_9_augmentedMatrix A i j * Fin.addCases x s j)
                    (by intro t; rfl)]
            rw [Fintype.sum_sum_type]
            simp [finSumFinEquiv_apply_left, finSumFinEquiv_apply_right]
    _ = (∑ j : Fin n, A i j * x j) + ∑ k : Fin m, (if i = k then 1 else 0) * s k := by
            simp [helperForText_22_3_9_augmentedMatrix, Fin.addCases_left, Fin.addCases_right]
    _ = (∑ j : Fin n, A i j * x j) + s i := by
            simp
    _ = (A.mulVec x + s) i := by
            simp [Matrix.mulVec, dotProduct]

Helper for Text 22.3.9: the inequality system Unknown identifier `x`sorry ≥ 0 : Propx ≥ 0, Unknown identifier `A`sorry ≤ sorry : PropA x ≤ Unknown identifier `a`a is equivalent to the nonnegative equality system for the augmented slack matrix.

lemma helperForText_22_3_9_primal_iff_augmentedPrimal
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    (∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x ≤ a) ↔
      ∃ z : Fin (n + m) → ℝ, 0 ≤ z ∧ (helperForText_22_3_9_augmentedMatrix A).mulVec z = a := by
  constructor
  · rintro ⟨x, hx_nonneg, hx_le⟩
    -- Add the slack vector `a - A x`, which is nonnegative exactly because `A x ≤ a`.
    refine ⟨Fin.addCases x (a - A.mulVec x), ?_, ?_⟩
    · intro j
      cases j using Fin.addCases with
      | left j =>
          simpa [Pi.zero_apply, Fin.addCases_left] using hx_nonneg j
      | right i =>
          simpa [Pi.zero_apply, Fin.addCases_right, Pi.sub_apply] using
            sub_nonneg.mpr (hx_le i)
    · calc
        (helperForText_22_3_9_augmentedMatrix A).mulVec (Fin.addCases x (a - A.mulVec x))
            = A.mulVec x + (a - A.mulVec x) :=
              helperForText_22_3_9_augmentedMatrix_mulVec A x (a - A.mulVec x)
        _ = a := by
            ext i
            simp
  · rintro ⟨z, hz_nonneg, hz_eq⟩
    let x : Fin n → ℝ := fun j => z (Fin.castAdd m j)
    let s : Fin m → ℝ := fun i => z (Fin.natAdd n i)
    -- Read the first block of coordinates as `x` and the second block as the slack vector.
    have hz_split : z = Fin.addCases x s := by
      ext j
      cases j using Fin.addCases with
      | left j =>
          simp [x, Fin.addCases_left]
      | right i =>
          simp [s, Fin.addCases_right]
    have hEq : A.mulVec x + s = a := by
      calc
        A.mulVec x + s = (helperForText_22_3_9_augmentedMatrix A).mulVec (Fin.addCases x s) := by
          symm
          exact helperForText_22_3_9_augmentedMatrix_mulVec A x s
        _ = (helperForText_22_3_9_augmentedMatrix A).mulVec z := by
          rw [hz_split]
        _ = a := hz_eq
    refine ⟨x, ?_, ?_⟩
    · -- The first block of the nonnegative augmented vector gives `x ≥ 0`.
      intro j
      exact hz_nonneg (Fin.castAdd m j)
    · -- The second block is a nonnegative slack vector, so `A x ≤ a`.
      intro i
      have hs_nonneg : 0 ≤ s i := hz_nonneg (Fin.natAdd n i)
      have hi : A.mulVec x i + s i = a i := congrArg (fun v => v i) hEq
      linarith

Helper for Text 22.3.9: the transpose multiplier for the augmented slack matrix splits into the blocks and Unknown identifier `u`u.

lemma helperForText_22_3_9_augmentedTranspose_mulVec
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (u : Fin m → ℝ) :
    (helperForText_22_3_9_augmentedMatrix A).transpose.mulVec u =
      Fin.addCases (A.transpose.mulVec u) u := by
  -- Compute the transpose action coordinatewise on the original block and the slack block.
  ext j
  cases j using Fin.addCases with
  | left j =>
      simp [helperForText_22_3_9_augmentedMatrix, Matrix.mulVec, dotProduct, Fin.addCases_left]
  | right k =>
      simp [helperForText_22_3_9_augmentedMatrix, Matrix.mulVec, dotProduct, Fin.addCases_right]

Helper for Text 22.3.9: the dual branch for the augmented matrix is equivalent to the target dual certificate after negating the multiplier.

lemma helperForText_22_3_9_dual_iff_augmentedDual
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    (∃ u : Fin m → ℝ,
        (helperForText_22_3_9_augmentedMatrix A).transpose.mulVec u ≤ 0 ∧
          0 < dotProduct a u) ↔
      ∃ w : Fin m → ℝ, 0 ≤ w ∧ 0 ≤ A.transpose.mulVec w ∧ dotProduct a w < 0 := by
  constructor
  · rintro ⟨u, hu_nonpos, hu_dot⟩
    -- Negating the multiplier turns the nonpositive equality-form dual into the target
    -- nonnegative inequality-form dual.
    refine ⟨-u, ?_, ?_, ?_⟩
    · intro i
      have hi :
          (helperForText_22_3_9_augmentedMatrix A).transpose.mulVec u (Fin.natAdd n i) ≤ 0 :=
        hu_nonpos (Fin.natAdd n i)
      simpa [helperForText_22_3_9_augmentedTranspose_mulVec, Pi.neg_apply] using
        (neg_nonneg.mpr hi)
    · intro j
      have hj :
          (helperForText_22_3_9_augmentedMatrix A).transpose.mulVec u (Fin.castAdd m j) ≤ 0 :=
        hu_nonpos (Fin.castAdd m j)
      simpa [helperForText_22_3_9_augmentedTranspose_mulVec, Matrix.mulVec_neg, Pi.neg_apply] using
        (neg_nonneg.mpr hj)
    · simpa [dotProduct_neg] using (neg_neg_of_pos hu_dot)
  · rintro ⟨w, hw_nonneg, hw_transpose, hw_dot⟩
    -- Reversing the same sign change recovers the dual branch of the equality-form theorem.
    refine ⟨-w, ?_, ?_⟩
    · intro j
      cases j using Fin.addCases with
      | left j =>
          have hj : 0 ≤ A.transpose.mulVec w j := hw_transpose j
          simpa [helperForText_22_3_9_augmentedTranspose_mulVec, Matrix.mulVec_neg,
            Pi.neg_apply, Fin.addCases_left] using (neg_nonpos.mpr hj)
      | right i =>
          have hi : 0 ≤ w i := hw_nonneg i
          simpa [helperForText_22_3_9_augmentedTranspose_mulVec, Pi.neg_apply,
            Fin.addCases_right] using (neg_nonpos.mpr hi)
    · simpa [dotProduct_neg] using (neg_pos.mpr hw_dot)

Text 22.3.9: Let failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `A`A ∈ ℝ^{Unknown identifier `m`m × Unknown identifier `n`n} and failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `a`a ∈ ℝ^Unknown identifier `m`m. Exactly one of the following two systems has a solution: (Unknown identifier `P`P) Unknown identifier `x`sorry ≥ 0 : Propx ≥ 0 and Unknown identifier `A`sorry * sorry ≤ sorry : PropA * Unknown identifier `x`x ≤ Unknown identifier `a`a; (Unknown identifier `D`D) Unknown identifier `w`sorry ≥ 0 : Propw ≥ 0, , and .

theorem farkasAlternative_nonnegative_subsolution_matrix
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) :
    ((∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x ≤ a) ∨
        ∃ w : Fin m → ℝ, 0 ≤ w ∧ 0 ≤ A.transpose.mulVec w ∧ dotProduct a w < 0) ∧
      ¬((∃ x : Fin n → ℝ, 0 ≤ x ∧ A.mulVec x ≤ a) ∧
        ∃ w : Fin m → ℝ, 0 ≤ w ∧ 0 ≤ A.transpose.mulVec w ∧ dotProduct a w < 0) := by
  -- Route correction: do not attack the inequality system directly; introduce slack
  -- variables and rewrite the statement to the already proved equality-form alternative.
  simpa [helperForText_22_3_9_primal_iff_augmentedPrimal,
    helperForText_22_3_9_dual_iff_augmentedDual] using
    farkasAlternative_nonnegative_matrix (helperForText_22_3_9_augmentedMatrix A) a

A family of real intervals indexed by Fin sorry : TypeFin Unknown identifier `N`N, interpreted as convex subsets of ℝ : Typeℝ.

abbrev RealIntervalFamily (N : ℕ) := { I : Fin N → Set ℝ // ∀ j, Convex ℝ (I j) }

Text 22.3.9.1: Given Unknown identifier `N`sorry = sorry + sorry : PropN = Unknown identifier `m`m + Unknown identifier `n`n, a real coefficient matrix Unknown identifier `A`sorry = sorry : PropA = (Unknown identifier `αᵢⱼ`αᵢⱼ), and real intervals , the general primal system is the set of all such that Unknown identifier `ζ_j`sorry ∈ sorry : Propζ_j ∈ Unknown identifier `I_j`I_j for every and for every .

def generalPrimalSystem
    {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ)
    (I : RealIntervalFamily (n + m)) : Set (Fin (n + m) → ℝ) :=
  {ζ |
    (∀ j, ζ j ∈ I.1 j) ∧
      ∀ i, ζ (Fin.natAdd n i) = ∑ j, A i j * ζ (Fin.castAdd m j)}

-- Proof sketch: the first `n` coordinates use the unrestricted interval `(-∞, +∞) = univ`,
-- and the last `m` coordinates use the lower intervals `(-∞, aᵢ] = Iic (a i)`; each of
-- these sets is convex, so the resulting indexed family is a valid `RealIntervalFamily`.

The interval family that encodes the inequalities Unknown identifier `A`sorry ≤ sorry : PropA x ≤ Unknown identifier `a`a as a general primal system.

lemma linearInequalityIntervalFamily_convex
    {m n : ℕ} (a : Fin m → ℝ) :
    ∀ j : Fin (n + m),
      Convex ℝ
        (Fin.addCases (m := n) (n := m)
          (fun _ : Fin n => (Set.univ : Set ℝ))
          (fun i : Fin m => Set.Iic (a i)) j) := by
  intro j
  cases j using Fin.addCases with
  | left j =>
      simpa using (convex_univ : Convex ℝ (Set.univ : Set ℝ))
  | right i =>
      simpa using (convex_Iic (a i))

The interval family with unrestricted first coordinates and upper-bounded last coordinates determined by Unknown identifier `a`a.

abbrev linearInequalityIntervalFamily
    {m n : ℕ} (a : Fin m → ℝ) : RealIntervalFamily (n + m) :=
  ⟨Fin.addCases (m := n) (n := m)
      (fun _ : Fin n => (Set.univ : Set ℝ))
      (fun i : Fin m => Set.Iic (a i)),
    linearInequalityIntervalFamily_convex a⟩

-- Proof sketch: unfold `generalPrimalSystem` and `linearInequalityIntervalFamily` for the
-- point `ζ = Fin.addCases x (A.mulVec x)`. The first `n` coordinates are automatically in
-- `univ`, while the last `m` coordinates satisfy the defining equalities by construction; the
-- remaining membership conditions are exactly `(A.mulVec x) i ≤ a i` for each `i`.

Text 22.3.9.2: The system Unknown identifier `A`sorry ≤ sorry : PropA x ≤ Unknown identifier `a`a is represented by the general primal system with for and for .

theorem linearInequality_as_generalPrimalSystem
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) (x : Fin n → ℝ) :
    Fin.addCases (m := n) (n := m) x (A.mulVec x) ∈
        generalPrimalSystem A (linearInequalityIntervalFamily (n := n) a) ↔
      A.mulVec x ≤ a := by
  -- Route correction: keep the argument purely definitional by unfolding the general
  -- primal-system membership for the specific point `Fin.addCases x (A.mulVec x)`.
  change
    ((∀ j : Fin (n + m),
        Fin.addCases (m := n) (n := m) x (A.mulVec x) j ∈
          (linearInequalityIntervalFamily (n := n) a).1 j) ∧
      ∀ i : Fin m,
        Fin.addCases (m := n) (n := m) x (A.mulVec x) (Fin.natAdd n i) =
          ∑ j : Fin n,
            A i j * Fin.addCases (m := n) (n := m) x (A.mulVec x) (Fin.castAdd m j)) ↔
      A.mulVec x ≤ a
  constructor
  · Try this: intro hz iintro hz
    -- Evaluating the interval-membership condition on the right block gives the inequalities.
    intro i
    have hi := hz.1 (Fin.natAdd n i)
    simpa [linearInequalityIntervalFamily] using hi
  · intro hx
    refine ⟨?_, ?_⟩
    · intro j
      -- Split the index between the unrestricted `x`-coordinates and the bounded
      -- `A.mulVec x`-coordinates.
      cases j using Fin.addCases with
      | left j =>
          simp
      | right i =>
          simpa [linearInequalityIntervalFamily] using hx i
    · intro i
      -- The defining equations on the last block are exactly the formula for `A.mulVec x`.
      simp [Matrix.mulVec, dotProduct]

-- Proof sketch: the first `n` coordinates use the nonnegative interval `[0, +∞) = Ici 0`,
-- and the last `m` coordinates use the singleton intervals `{a_i}`; both kinds of sets are
-- convex, so these data define a valid `RealIntervalFamily` for the general primal system.

The interval family that encodes the system Unknown identifier `x`sorry ≥ 0 : Propx ≥ 0, Unknown identifier `A`sorry = sorry : PropA x = Unknown identifier `a`a as a general primal system.

lemma nonnegativeEqualityIntervalFamily_convex
    {m n : ℕ} (a : Fin m → ℝ) :
    ∀ j : Fin (n + m),
      Convex ℝ
        (Fin.addCases (m := n) (n := m)
          (fun _ : Fin n => Set.Ici (0 : ℝ))
          (fun i : Fin m => ({a i} : Set ℝ)) j) := by
  intro j
  -- Split the family into the nonnegative half-lines on the left block and the singleton
  -- intervals on the right block.
  cases j using Fin.addCases with
  | left j =>
      simpa using (convex_Ici (0 : ℝ))
  | right i =>
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa using Set.convex_singleton (a i)

The interval family with nonnegative first coordinates and fixed last coordinates given by Unknown identifier `a`a.

abbrev nonnegativeEqualityIntervalFamily
    {m n : ℕ} (a : Fin m → ℝ) : RealIntervalFamily (n + m) :=
  ⟨Fin.addCases (m := n) (n := m)
      (fun _ : Fin n => Set.Ici (0 : ℝ))
      (fun i : Fin m => ({a i} : Set ℝ)),
    nonnegativeEqualityIntervalFamily_convex a⟩

-- Proof sketch: unfold `generalPrimalSystem` and `nonnegativeEqualityIntervalFamily` for the
-- point `ζ = Fin.addCases x a`. Membership of the first `n` coordinates is exactly `0 ≤ x`,
-- while membership of the last `m` coordinates in the singletons `{a_i}` is automatic; the
-- defining equalities for the last coordinates are precisely the equation `A.mulVec x = a`.

Helper for Text 22.3.9.3: identify the interval-membership part of the general primal system with the coordinatewise nonnegativity condition on Unknown identifier `x`x.

lemma helperForText_22_3_9_3_intervalMembership_iff
    {m n : ℕ} (a : Fin m → ℝ) (x : Fin n → ℝ) :
    (∀ j : Fin (n + m),
      Fin.addCases (m := n) (n := m) x a j ∈
        (nonnegativeEqualityIntervalFamily (n := n) a).1 j) ↔ 0 ≤ x := by
  constructor
  · Try this: intro hz jintro hz
    intro j
    -- Read the first block of interval constraints as the nonnegativity conditions on `x`.
    have hj := hz (Fin.castAdd m j)
    simpa [nonnegativeEqualityIntervalFamily] using hj
  · Try this: intro hx jintro hx
    intro j
    -- Split the index so the right block is automatic singleton membership and the left block
    -- is exactly `hx`.
    cases j using Fin.addCases with
    | left j =>
        simpa [nonnegativeEqualityIntervalFamily] using hx j
    | right i =>
        simp

Helper for Text 22.3.9.3: identify the tail equations in the general primal system with the matrix equation Unknown identifier `A.mulVec`sorry = sorry : PropA.mulVec x = Unknown identifier `a`a.

lemma helperForText_22_3_9_3_tailEquations_iff
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) (x : Fin n → ℝ) :
    (∀ i : Fin m,
      Fin.addCases (m := n) (n := m) x a (Fin.natAdd n i) =
        ∑ j : Fin n,
          A i j * Fin.addCases (m := n) (n := m) x a (Fin.castAdd m j)) ↔
      A.mulVec x = a := by
  constructor
  · intro h
    -- Evaluate the tail equations coordinatewise and rewrite them as `A.mulVec x = a`.
    ext i
    simpa [Matrix.mulVec, dotProduct] using (h i).symm
  · Try this: intro h iintro h
    intro i
    -- Conversely, each coordinate of `A.mulVec x = a` is one of the defining tail equations.
    have hi := congrArg (fun v => v i) h
    simpa [Matrix.mulVec, dotProduct] using hi.symm

Text 22.3.9.3: The system Unknown identifier `x`sorry ≥ 0 : Propx ≥ 0, Unknown identifier `A`sorry = sorry : PropA x = Unknown identifier `a`a is represented by the general primal system with for and for .

theorem nonnegativeLinearEquality_as_generalPrimalSystem
    {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (a : Fin m → ℝ) (x : Fin n → ℝ) :
    Fin.addCases (m := n) (n := m) x a ∈
        generalPrimalSystem A (nonnegativeEqualityIntervalFamily (n := n) a) ↔
      0 ≤ x ∧ A.mulVec x = a := by
  -- Route correction: keep the proof definitional, separating the interval constraints from
  -- the tail equations and translating each part independently.
  change
    ((∀ j : Fin (n + m),
        Fin.addCases (m := n) (n := m) x a j ∈
          (nonnegativeEqualityIntervalFamily (n := n) a).1 j) ∧
      ∀ i : Fin m,
        Fin.addCases (m := n) (n := m) x a (Fin.natAdd n i) =
          ∑ j : Fin n,
            A i j * Fin.addCases (m := n) (n := m) x a (Fin.castAdd m j)) ↔
      0 ≤ x ∧ A.mulVec x = a
  -- Rewrite the two conjuncts using the dedicated helper lemmas.
  rw [helperForText_22_3_9_3_intervalMembership_iff,
    helperForText_22_3_9_3_tailEquations_iff]

Text 22.3.11: For , the support of Unknown identifier `z`z is the set of indices such that Unknown identifier `z`sorry ≠ 0 : Propz j ≠ 0. This uses Fin sorry : TypeFin Unknown identifier `N`N to model the textbook index set .

def vectorSupport {N : ℕ} (z : Fin N → ℝ) : Set (Fin N) :=
  {j | z j ≠ 0}

Text 22.3.12: A nonzero vector Unknown identifier `z`z of the linear subspace failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `L`L ⊆ ℝ^Unknown identifier `N`N is an elementary vector of Unknown identifier `L`L if no nonzero vector of Unknown identifier `L`L has support strictly contained in the support of Unknown identifier `z`z.

def IsElementaryVector {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) (z : Fin N → ℝ) : Prop :=
  z ≠ 0 ∧ z ∈ L ∧ ¬∃ y : Fin N → ℝ, y ≠ 0 ∧ y ∈ L ∧ vectorSupport y ⊂ vectorSupport z

Helper for Lemma 22.4: a nonzero vector has a coordinate that does not vanish.

lemma helperForLemma_22_4_exists_pivotIndex
    {N : ℕ} {z : Fin N → ℝ} (hz : z ≠ 0) : ∃ i : Fin N, z i ≠ 0 := by
  classical
  -- If every coordinate vanished, function extensionality would force `z = 0`.
  by_contra hno
  push_neg at hno
  apply hz
  ext i
  exact hno i

Helper for Lemma 22.4: equal supports mean each coordinate vanishes for one vector exactly when it vanishes for the other.

lemma helperForLemma_22_4_sameSupport_coord_zero_iff
    {N : ℕ} {z z' : Fin N → ℝ} (hsupp : vectorSupport z = vectorSupport z') (i : Fin N) :
    z i = 0 ↔ z' i = 0 := by
  constructor
  · intro hzi
    -- A nonzero coordinate of `z'` would place `i` in the common support, contradicting `z i = 0`.
    by_contra hz'i
    have hi' : i ∈ vectorSupport z' := by
      simpa [vectorSupport] using hz'i
    have hi : i ∈ vectorSupport z := by
      rw [hsupp]
      exact hi'
    have hzi_ne : z i ≠ 0 := by
      simpa [vectorSupport] using hi
    exact hzi_ne hzi
  · intro hz'i
    -- The same support comparison works in the reverse direction.
    by_contra hzi
    have hi : i ∈ vectorSupport z := by
      simpa [vectorSupport] using hzi
    have hi' : i ∈ vectorSupport z' := by
      rw [← hsupp]
      exact hi
    have hz'i_ne : z' i ≠ 0 := by
      simpa [vectorSupport] using hi'
    exact hz'i_ne hz'i

Helper for Lemma 22.4: cancelling a scalar multiple cannot create new support outside the common support.

lemma helperForLemma_22_4_cancel_support_subset
    {N : ℕ} {z z' : Fin N → ℝ} (hsupp : vectorSupport z = vectorSupport z') (c : ℝ) :
    vectorSupport (z' - c • z) ⊆ vectorSupport z := by
  intro j hj
  change z j ≠ 0
  -- Outside the support of `z`, the common-support hypothesis also forces `z' j = 0`.
  by_contra hzj
  have hz'j : z' j = 0 := (helperForLemma_22_4_sameSupport_coord_zero_iff hsupp j).mp hzj
  have hcancel : (z' - c • z) j = 0 := by
    simp [Pi.smul_apply, hzj, hz'j]
  change (z' - c • z) j ≠ 0 at hj
  exact hj hcancel

Helper for Lemma 22.4: cancelling the pivot coordinate strictly decreases the common support.

lemma helperForLemma_22_4_cancel_support_ssubset
    {N : ℕ} {z z' : Fin N → ℝ} {i : Fin N}
    (hsupp : vectorSupport z = vectorSupport z') (hzi : z i ≠ 0) :
    vectorSupport (z' - (z' i / z i) • z) ⊂ vectorSupport z := by
  refine ⟨helperForLemma_22_4_cancel_support_subset hsupp (z' i / z i), ?_⟩
  intro hreverse
  -- The chosen pivot stays in `vectorSupport z`, but the cancellation makes it vanish in the
  -- new vector, so reverse inclusion is impossible.
  have hiz : i ∈ vectorSupport z := by
    simpa [vectorSupport] using hzi
  have hiy : i ∈ vectorSupport (z' - (z' i / z i) • z) := hreverse hiz
  have hyi : (z' - (z' i / z i) • z) i = 0 := by
    calc
      (z' - (z' i / z i) • z) i = z' i - (z' i / z i) * z i := by
        simp [Pi.smul_apply]
      _ = z' i - z' i := by
        rw [div_mul_cancel₀ _ hzi]
      _ = 0 := sub_self _
  have hiy_ne : (z' - (z' i / z i) • z) i ≠ 0 := by
    simpa [vectorSupport] using hiy
  exact hiy_ne hyi

-- Proof sketch: if `z` and `z'` have the same support but are not proportional, choose an
-- index in their common support and subtract a suitable scalar multiple so that one coordinate
-- vanishes. The resulting nonzero vector still lies in `L` and has strictly smaller support,
-- contradicting the elementary property.

Lemma 22.4: If Unknown identifier `z`z and Unknown identifier `z'`z' are elementary vectors of a subspace failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `L`L ⊆ ℝ^Unknown identifier `N`N with the same support, then Unknown identifier `z'`z' is a nonzero scalar multiple of Unknown identifier `z`z.

lemma elementaryVector_eq_smul_of_same_support
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) {z z' : Fin N → ℝ}
    (hz : IsElementaryVector L z) (hz' : IsElementaryVector L z')
    (hsupp : vectorSupport z = vectorSupport z') :
    ∃ c : ℝ, c ≠ 0 ∧ z' = c • z := by
  rcases hz with ⟨hz_ne, hz_mem, hz_min⟩
  rcases hz' with ⟨hz'_ne, hz'_mem, hz'_min⟩
  rcases helperForLemma_22_4_exists_pivotIndex hz_ne with ⟨i, hzi⟩
  -- The common-support hypothesis gives a pivot where both vectors are nonzero.
  have hz'i : z' i ≠ 0 := by
    intro hz'i0
    exact hzi ((helperForLemma_22_4_sameSupport_coord_zero_iff hsupp i).mpr hz'i0)
  let c : ℝ := z' i / z i
  let y : Fin N → ℝ := z' - c • z
  -- The cancellation vector stays in the same subspace.
  have hy_mem : y ∈ L := by
    dsimp [y, c]
    exact L.sub_mem hz'_mem (L.smul_mem _ hz_mem)
  by_cases hy_zero : y = 0
  · -- If the cancellation vector vanishes, the desired proportionality is immediate.
    refine ⟨c, div_ne_zero hz'i hzi, ?_⟩
    dsimp [y] at hy_zero
    exact sub_eq_zero.mp hy_zero
  · -- Otherwise `y` is a nonzero vector in `L` with strictly smaller support, contradicting
    -- the elementary minimality of `z'`.
    have hy_support : vectorSupport y ⊂ vectorSupport z := by
      dsimp [y, c]
      exact helperForLemma_22_4_cancel_support_ssubset hsupp hzi
    have hy_support' : vectorSupport y ⊂ vectorSupport z' := by
      simpa [hsupp] using hy_support
    exact False.elim (hz'_min ⟨y, hy_zero, hy_mem, hy_support'⟩)

-- Proof sketch: each elementary vector determines a nonempty support subset of `Fin N`, and
-- there are only finitely many such subsets. By Lemma 22.4, two elementary vectors with the
-- same support differ by a nonzero scalar, so one representative for each realized support
-- gives finitely many scalar-multiple classes.

Helper for Corollary 22.4.1: the subtype of support sets realized by elementary vectors of Unknown identifier `L`L.

abbrev helperForCorollary_22_4_1_realizedSupportSubtype
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) :=
  {s : Set (Fin N) | ∃ z : Fin N → ℝ, IsElementaryVector L z ∧ vectorSupport z = s}

Helper for Corollary 22.4.1: the realized-support subtype is finite because Fin sorry : TypeFin Unknown identifier `N`N has only finitely many subsets.

lemma helperForCorollary_22_4_1_realizedSupportsFinite
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) :
    (Set.univ : Set (helperForCorollary_22_4_1_realizedSupportSubtype L)).Finite := by
  classical
  -- The realized supports form a subtype of the finite type `Set (Fin N)`.
  exact Set.finite_univ

Helper for Corollary 22.4.1: choose one elementary vector for each realized support.

noncomputable abbrev helperForCorollary_22_4_1_supportRepresentative
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) :
    helperForCorollary_22_4_1_realizedSupportSubtype L → (Fin N → ℝ) :=
  fun s => Classical.choose s.property

Helper for Corollary 22.4.1: the chosen representative is elementary and has the prescribed support.

lemma helperForCorollary_22_4_1_supportRepresentative_spec
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ))
    (s : helperForCorollary_22_4_1_realizedSupportSubtype L) :
    IsElementaryVector L (helperForCorollary_22_4_1_supportRepresentative L s) ∧
      vectorSupport (helperForCorollary_22_4_1_supportRepresentative L s) = s.1 := by
  -- Unpack the witness attached to the realized support.
  exact Classical.choose_spec s.property

Helper for Corollary 22.4.1: every elementary vector has the same support as one chosen representative.

lemma helperForCorollary_22_4_1_representatives_cover_by_support
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) {z : Fin N → ℝ}
    (hz : IsElementaryVector L z) :
    ∃ s : helperForCorollary_22_4_1_realizedSupportSubtype L,
      vectorSupport (helperForCorollary_22_4_1_supportRepresentative L s) = vectorSupport z := by
  -- Package the support of `z` as a realized support and appeal to the representative spec.
  refine ⟨⟨vectorSupport z, ⟨z, hz, rfl⟩⟩, ?_⟩
  exact helperForCorollary_22_4_1_supportRepresentative_spec L ⟨vectorSupport z, ⟨z, hz, rfl⟩⟩ |>.2

Corollary 22.4.1: A subspace Unknown identifier `L`L of ℝ ^ sorry : Typeℝ^Unknown identifier `N`N has only finitely many elementary vectors, up to scalar multiples. Equivalently, there is a finite set of representatives such that every elementary vector of Unknown identifier `L`L is a nonzero scalar multiple of one of them.

theorem elementaryVector_finite_upToScalarMultiples
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) :
    ∃ S : Set (Fin N → ℝ), S.Finite ∧
      (∀ y : Fin N → ℝ, y ∈ S → IsElementaryVector L y) ∧
      ∀ z : Fin N → ℝ, IsElementaryVector L z →
        ∃ y ∈ S, ∃ c : ℝ, c ≠ 0 ∧ z = c • y := by
  classical
  let S : Set (Fin N → ℝ) :=
    helperForCorollary_22_4_1_supportRepresentative L ''
      (Set.univ : Set (helperForCorollary_22_4_1_realizedSupportSubtype L))
  refine ⟨S, ?_, ?_, ?_⟩
  · -- The representative set is finite as the image of a finite subtype.
    dsimp [S]
    exact (helperForCorollary_22_4_1_realizedSupportsFinite L).image
      (helperForCorollary_22_4_1_supportRepresentative L)
  · intro y hy
    -- Any element of `S` is one of the chosen representatives, hence elementary.
    rw [Set.mem_image] at hy
    rcases hy with ⟨s, -, rfl⟩
    exact (helperForCorollary_22_4_1_supportRepresentative_spec L s).1
  · intro z hz
    -- Choose the representative for the support class of `z`.
    rcases helperForCorollary_22_4_1_representatives_cover_by_support L hz with ⟨s, hsupp⟩
    let y := helperForCorollary_22_4_1_supportRepresentative L s
    have hyS : y ∈ S := by
      dsimp [S, y]
      exact ⟨s, Set.mem_univ s, rfl⟩
    have hyElem : IsElementaryVector L y := by
      -- The representative inherits elementary status from the support witness.
      dsimp [y]
      exact (helperForCorollary_22_4_1_supportRepresentative_spec L s).1
    -- Lemma 22.4 upgrades equality of supports to equality up to nonzero scalar.
    rcases elementaryVector_eq_smul_of_same_support L hyElem hz hsupp with ⟨c, hc, hzc⟩
    exact ⟨y, hyS, c, hc, hzc⟩

-- Proof sketch: argue by induction on the size of the support of `z ∈ L`. If `z = 0`, the
-- claim is immediate; otherwise, either `z` is elementary or there exists a nonzero `y ∈ L`
-- with strictly smaller support. Subtracting a suitable multiple of `y` reduces the support,
-- and the induction hypothesis yields a decomposition into elementary vectors.

Helper for Lemma 22.5: a strict support inclusion forces a strict drop in support cardinality.

lemma helperForLemma_22_5_supportNcard_lt_of_ssubset
    {N : ℕ} {y z : Fin N → ℝ} (hss : vectorSupport y ⊂ vectorSupport z) :
    (vectorSupport y).ncard < (vectorSupport z).ncard := by
  classical
  -- Compare the finite supports through their `Finset` realizations.
  rw [Set.ncard_eq_toFinset_card, Set.ncard_eq_toFinset_card]
  exact Finset.card_lt_card ((Set.toFinite _).toFinset_ssubset_toFinset.2 hss)

Helper for Lemma 22.5: cancelling a scalar multiple of a vector with smaller support cannot introduce new nonzero coordinates.

lemma helperForLemma_22_5_cancel_support_subset
    {N : ℕ} {y z : Fin N → ℝ} (hsubset : vectorSupport y ⊆ vectorSupport z) (c : ℝ) :
    vectorSupport (z - c • y) ⊆ vectorSupport z := by
  intro j hj
  change z j ≠ 0
  -- Outside `vectorSupport z`, the smaller-support vector `y` also vanishes.
  by_contra hzj
  have hyj : y j = 0 := by
    by_contra hyj
    have hjy : j ∈ vectorSupport y := by
      simpa [vectorSupport] using hyj
    have hjz : j ∈ vectorSupport z := hsubset hjy
    have hzj_ne : z j ≠ 0 := by
      simpa [vectorSupport] using hjz
    exact hzj_ne hzj
  have hwj : (z - c • y) j = 0 := by
    simp [Pi.smul_apply, hzj, hyj]
  change (z - c • y) j ≠ 0 at hj
  exact hj hwj

Helper for Lemma 22.5: cancelling a pivot coordinate against a strictly smaller-support vector produces another vector with strictly smaller support.

lemma helperForLemma_22_5_cancel_support_ssubset
    {N : ℕ} {y z : Fin N → ℝ} {i : Fin N}
    (hss : vectorSupport y ⊂ vectorSupport z) (hyi : y i ≠ 0) :
    vectorSupport (z - (z i / y i) • y) ⊂ vectorSupport z := by
  refine ⟨helperForLemma_22_5_cancel_support_subset hss.1 (z i / y i), ?_⟩
  intro hreverse
  -- The pivot belongs to `vectorSupport z`, but the chosen scalar cancels it in the new vector.
  have hiz : i ∈ vectorSupport z := hss.1 (by simpa [vectorSupport] using hyi)
  have hiw : i ∈ vectorSupport (z - (z i / y i) • y) := hreverse hiz
  have hwi : (z - (z i / y i) • y) i = 0 := by
    calc
      (z - (z i / y i) • y) i = z i - (z i / y i) * y i := by
        simp [Pi.smul_apply]
      _ = z i - z i := by
        rw [div_mul_cancel₀ _ hyi]
      _ = 0 := sub_self _
  have hwi_ne : (z - (z i / y i) • y) i ≠ 0 := by
    simpa [vectorSupport] using hiw
  exact hwi_ne hwi

Helper for Lemma 22.5: a vector with empty support is the zero vector.

lemma helperForLemma_22_5_zero_of_supportNcard_eq_zero
    {N : ℕ} {z : Fin N → ℝ} (hzcard : (vectorSupport z).ncard = 0) :
    z = 0 := by
  -- A nonzero coordinate would make the support nonempty, contradicting the zero cardinality.
  ext i
  by_contra hzi
  have hnonempty : (vectorSupport z).Nonempty := by
    exact ⟨i, by simpa [vectorSupport] using hzi⟩
  have hpos : 0 < (vectorSupport z).ncard := hnonempty.ncard_pos
  linarith

Lemma 22.5: Every vector in a subspace failed to synthesize HasSubset Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `L`L ⊆ ℝ^Unknown identifier `N`N belongs to the linear span of the elementary vectors of Unknown identifier `L`L; equivalently, every vector of Unknown identifier `L`L can be expressed as a linear combination of elementary vectors of Unknown identifier `L`L.

lemma mem_span_elementaryVectors
    {N : ℕ} (L : Submodule ℝ (Fin N → ℝ)) {z : Fin N → ℝ} (hz : z ∈ L) :
    z ∈ Submodule.span ℝ {y : Fin N → ℝ | IsElementaryVector L y} := by
  classical
  let E : Set (Fin N → ℝ) := {y : Fin N → ℝ | IsElementaryVector L y}
  have hspan :
      ∀ n : ℕ, ∀ {x : Fin N → ℝ}, x ∈ L → (vectorSupport x).ncard ≤ n →
        x ∈ Submodule.span ℝ E := by
    intro n
    induction' n with n ih
    · intro x hx hxcard
      -- The zero-cardinality support case forces `x = 0`.
      have hx_zero : x = 0 := by
        exact helperForLemma_22_5_zero_of_supportNcard_eq_zero (Nat.le_zero.mp hxcard)
      try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hx_zero] using Submodule.zero_mem (Submodule.span ℝ E)
    · intro x hx hxcard
      -- Split first on whether the current vector already vanishes.
      by_cases hx_zero : x = 0
      · try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hx_zero] using Submodule.zero_mem (Submodule.span ℝ E)
      · by_cases hxElem : IsElementaryVector L x
        · -- Elementary vectors belong to the span by construction.
          exact Submodule.subset_span hxElem
        · -- Route correction: instead of searching for a basis argument, peel off one
          -- smaller-support vector and a cancellation remainder, then invoke the induction
          -- hypothesis on both.
          have hy_exists : ∃ y : Fin N → ℝ,
              y ≠ 0 ∧ y ∈ L ∧ vectorSupport y ⊂ vectorSupport x := by
            by_contra hno
            exact hxElem ⟨hx_zero, hx, hno⟩
          rcases hy_exists with ⟨y, hy_zero, hy_mem, hy_support⟩
          have hy_card_lt : (vectorSupport y).ncard < (vectorSupport x).ncard :=
            helperForLemma_22_5_supportNcard_lt_of_ssubset hy_support
          have hy_card_le : (vectorSupport y).ncard ≤ n := by
            exact Nat.lt_succ_iff.mp (lt_of_lt_of_le hy_card_lt hxcard)
          have hy_span : y ∈ Submodule.span ℝ E := ih hy_mem hy_card_le
          rcases helperForLemma_22_4_exists_pivotIndex hy_zero with ⟨i, hyi⟩
          let c : ℝ := x i / y i
          let w : Fin N → ℝ := x - c • y
          have hw_mem : w ∈ L := by
            -- Submodules are closed under subtraction and scalar multiplication.
            dsimp [w, c]
            exact L.sub_mem hx (L.smul_mem _ hy_mem)
          have hw_support : vectorSupport w ⊂ vectorSupport x := by
            -- Cancelling the pivot coordinate strictly shrinks the support.
            dsimp [w, c]
            exact helperForLemma_22_5_cancel_support_ssubset hy_support hyi
          have hw_card_lt : (vectorSupport w).ncard < (vectorSupport x).ncard :=
            helperForLemma_22_5_supportNcard_lt_of_ssubset hw_support
          have hw_card_le : (vectorSupport w).ncard ≤ n := by
            exact Nat.lt_succ_iff.mp (lt_of_lt_of_le hw_card_lt hxcard)
          have hw_span : w ∈ Submodule.span ℝ E := ih hw_mem hw_card_le
          have hc_y_span : c • y ∈ Submodule.span ℝ E := by
            -- The span is closed under scalar multiplication.
            exact Submodule.smul_mem (Submodule.span ℝ E) c hy_span
          have hsum_span : w + c • y ∈ Submodule.span ℝ E := by
            -- The span is also closed under addition.
            exact Submodule.add_mem (Submodule.span ℝ E) hw_span hc_y_span
          have hx_decomp : x = w + c • y := by
            -- Unfold the cancellation remainder and simplify coordinatewise.
            ext j
            simp [w, c, sub_eq_add_neg, add_comm, add_left_comm, This simp argument is unused:
  add_assoc

Hint: Omit it from the simp argument list.
  simp [w, c, sub_eq_add_neg, add_comm, add_left_comm,̵ ̵a̵d̵d̵_̵a̵s̵s̵o̵c̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`add_assoc]
          simpa [hx_decomp] using hsum_span
  -- Apply the bounded-support induction at the actual support size of `z`.
  exact hspan (vectorSupport z).ncard hz le_rfl

-- Proof sketch: for a finite family of intervals on the line, pairwise intersection implies
-- the family of left endpoints is bounded above by every right endpoint. Choose a point between
-- the maximal left endpoint and minimal right endpoint; it then lies in every interval.

Helper for Text 22.5.1: a singleton subfamily already has nonempty intersection because pairwise intersection with itself shows the chosen interval is nonempty.

lemma helperForText_22_5_1_singletonSubfamily_nonempty
    {m : ℕ} (J : Fin m → Set ℝ)
    (hpair : ∀ i j : Fin m, (J i ∩ J j).Nonempty)
    (i : Fin m) :
    (⋂ j ∈ ({i} : Finset (Fin m)), J j).Nonempty := by
  -- A singleton intersection is just `J i`, and `hpair i i` provides a point of `J i`.
  simpa using hpair i i

Helper for Text 22.5.1: a two-element subfamily has nonempty intersection by the pairwise-intersection hypothesis.

lemma helperForText_22_5_1_pairSubfamily_nonempty
    {m : ℕ} (J : Fin m → Set ℝ)
    (hpair : ∀ i j : Fin m, (J i ∩ J j).Nonempty)
    (i j : Fin m) :
    (⋂ k ∈ ({i, j} : Finset (Fin m)), J k).Nonempty := by
  -- Simplifying the finite intersection over `{i, j}` recovers `J i ∩ J j`.
  simpa [Set.inter_assoc, Set.inter_left_comm, Set.inter_comm] using hpair i j

Helper for Text 22.5.1: every subfamily of cardinality at most two has nonempty intersection. This is the one-dimensional Helly hypothesis.

lemma helperForText_22_5_1_smallSubfamily_nonempty
    {m : ℕ} (J : Fin m → Set ℝ)
    (hpair : ∀ i j : Fin m, (J i ∩ J j).Nonempty) :
    ∀ s : Finset (Fin m), s.card ≤ 2 → (⋂ i ∈ s, J i).Nonempty := by
  classical
  intro s hs
  -- Split the cardinality bound into the only possible cases `0`, `1`, and `2`.
  have hs_cases : s.card = 0 ∨ s.card = 1 ∨ s.card = 2 := by
    omega
  rcases hs_cases with hs_zero | hs_one | hs_two
  · -- The empty subfamily intersects to `univ`.
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [Finset.card_eq_zero.mp hs_zero]
  · -- Rewrite the singleton subfamily and invoke the dedicated helper.
    rcases Finset.card_eq_one.mp hs_one with ⟨i, rfl⟩
    exact helperForText_22_5_1_singletonSubfamily_nonempty J hpair i
  · -- Rewrite the two-point subfamily and use pairwise intersection.
    rcases Finset.card_eq_two.mp hs_two with ⟨i, j, hij, rfl⟩
    exact helperForText_22_5_1_pairSubfamily_nonempty J hpair i j

Text 22.5.1: If are real intervals such that every pair Unknown identifier `Jᵢ`Jᵢ, Unknown identifier `Jⱼ`Jⱼ intersects, then their total intersection is nonempty. We model a real interval as an order-connected subset of ℝ : Typeℝ.

theorem pairwiseIntersecting_realIntervals_nonempty_iInter
    {m : ℕ} (J : Fin m → Set ℝ)
    (hJ : ∀ i, Set.OrdConnected (J i))
    (hpair : ∀ i j : Fin m, (J i ∩ J j).Nonempty) :
    (⋂ i, J i).Nonempty := by
  classical
  -- Route correction: apply Helly directly in the one-dimensional space `ℝ` instead of
  -- introducing endpoint bounds for the intervals.
  have hConvex : ∀ i : Fin m, Convex ℝ (J i) := by
    -- Order-connected subsets of `ℝ` are convex.
    intro i
    exact (hJ i).convex
  have hHelly :
      (⋂ i ∈ (Finset.univ : Finset (Fin m)), J i).Nonempty := by
    -- Helly reduces the global intersection to intersections of subfamilies of size at most two.
    refine Convex.helly_theorem' (𝕜 := ℝ) (E := ℝ)
      (F := J) (s := (Finset.univ : Finset (Fin m))) ?_ ?_
    · intro i hi
      exact hConvex i
    · intro s hs_sub hs_card
      exact helperForText_22_5_1_smallSubfamily_nonempty J hpair s (by simpa using hs_card)
  -- The finite intersection over `Finset.univ` is the same as the total indexed intersection.
  simpa using hHelly

end Section22end Chap04