-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
haveI₃ :
  ∀ (this : Fintype ι),
    hs.fundamentalDomain (s := s) ⊆ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
haveI₄ :
  ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)),
    x ∈ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
haveI₅ :
  ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)),
    LE.le.{u_3} (α := ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
        HSMul.hSMul (α := ℚ) (β := ι → ℚ)
          ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                    (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                  (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                (a : (↑hs.basisSet : Type u_3)) → ℚ)
              i :
            ℚ)
          ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ))
      (∑ x : (↑hs.basisSet : Type u_3), (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x : ι → ℕ))
haveI₆ :
  ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)) (i : (↑(hs.basisSet (s := s)) : Type u_3))
    (hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i),
    HSMul.hSMul (α := ℚ) (β := ι → ℚ)
        ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                  (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
              (a : (↑hs.basisSet : Type u_3)) → ℚ)
            i :
          ℚ)
        ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ) ≤
      (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ)
⊢ hs.fundamentalDomain (s := s).Finite
have haveI₇ : ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)) (i : (↑(hs.basisSet (s := s)) : Type u_3))
  (hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i),
  HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ) ≤
    (hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i
Tactic: classical
  haveI := Fintype.ofFinite ι
  apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset
  intro x hx
  rw [mem_Iic, ← toRatVec_mono, map_add, map_sum, ← add_sub_cancel (toRatVec hs.base) (toRatVec x),
    add_le_add_iff_left, ← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]
  refine Finset.sum_le_sum fun i hi => ?_
  rw [← hs.basis_apply i]
  apply smul_le_of_le_one_left
  · rw [hs.basis_apply]
    exact toRatVec_nonneg _
  · exact (hx i).2.le