-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
rw rw₁ rw₂ :
  ∀ (hy : ∃ (a : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ), y = ∑ i : (↑hs.basisSet : Type u_3), a i • (↑i : ι → ℕ)),
    hs.fract (s := s) (x + y) = hs.fract (s := s) x
rw₃ :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ),
    hs.fract (s := s) (x + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) = hs.fract (s := s) x
rw₄ :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ),
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
        (∑ i : (↑hs.basisSet : Type u_3),
            HSMul.hSMul (α := ℚ) (β := ι → ℚ)
              (Int.fract
                  ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                          (HSub.hSub (α := ι → ℚ) (β := ι → ℚ)
                            ((toRatVec : (a : ι → ℕ) → ι → ℚ)
                                (x + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) :
                              ι → ℚ)
                            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                        (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                      (a : (↑hs.basisSet : Type u_3)) → ℚ)
                    i) :
                ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
          ι → ℚ) =
      HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
        (∑ i : (↑hs.basisSet : Type u_3),
            HSMul.hSMul (α := ℚ) (β := ι → ℚ)
              (Int.fract
                  ((((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) :
                ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
          ι → ℚ)
h :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ) (x_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ x_1 →
      Eq (α := ℚ)
        (Int.fract
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                    (HSub.hSub (α := ι → ℚ) (β := ι → ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) :
                        ι → ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                  (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                (a : (↑hs.basisSet : Type u_3)) → ℚ)
              x_1) :
          ℚ)
        (Int.fract
            ((((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)) → ℚ)
              x_1) :
          ℚ)
h₁ :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ) (x_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ x_1 →
      Eq (α := ℚ)
        (Int.fract
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                    (HAdd.hAdd (β := ι → ℚ)
                      (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ))
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) :
                        ι → ℚ)) :
                  (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                (a : (↑hs.basisSet : Type u_3)) → ℚ)
              x_1) :
          ℚ)
        (Int.fract
            ((((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)) → ℚ)
              x_1) :
          ℚ)
⊢ hs.fract (s := s) (x + y) = hs.fract (s := s) x

Tactic:
classical
  rw [mem_closure_iff_of_fintype] at hy
  rcases hy with ⟨f, t, ht, hf, rfl⟩
  rw [← toRatVec_inj, hs.toRatVec_fract_eq, hs.toRatVec_fract_eq]
  congr! 3
  rw [map_add, ← sub_add_eq_add_sub]
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply]

Premises used: _private.0.IsProperLinearSet.toRatVec_fract_eq, map_add, AddSubmonoid.mem_closure_iff_of_fintype, _private.0.toRatVec_inj, nsmul_eq_mul, Finsupp.single_apply, _private.0.IsProperLinearSet.basis_apply, sub_add_eq_add_sub, rfl