-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
simp :
  Int.floor (α := ℚ)
      ((((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 :
        ℚ) ≤
    Int.floor (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + y) : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
hab :
  LE.le (α := ℚ)
    ((((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 :
      ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + y) : ι → ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
hab₁ :
  LE.le (α := ℚ) (0 : ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
hab₂ :
  ∀ (hy : ∃ (a : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ), y = ∑ i : (↑hs.basisSet : Type u_3), a i • (↑i : ι → ℕ)),
    LE.le (α := ℚ) (0 : ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
hab₃ :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ),
    LE.le (α := ℚ) (0 : ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) (∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) : ι → ℚ) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
⊢ hs.floor (s := s) x i ≤ hs.floor (s := s) (x + y) i
have hab₄ : ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ),
  LE.le (α := ℚ) 0
    (∑ c : (↑hs.basisSet : Type u_3),
      (((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (f c • (↑c : ι → ℕ)) : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i)
Tactic: classical
  simp only [floor]
  apply Int.floor_le_floor
  simp_rw [map_add, add_sub_right_comm, map_add, Finsupp.add_apply, le_add_iff_nonneg_right]
  rw [mem_closure_iff_of_fintype] at hy
  rcases hy with ⟨f, rfl⟩
  simp_rw [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply]
  apply Finset.sum_nonneg
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply, ite_nonneg]
Cleared hypotheses: y, hy