-- 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 : ι → ℕ
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 : ι → ℕ) : ι → ℚ) :
          ι → ℚ)
⊢ hs.fract (s := s) (x + y) = hs.fract (s := s) x
have 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) :
        ℚ)
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]
Cleared hypotheses: y, hy