-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
m n : E
simp_rw :
  (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i) : K)
        (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₁ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
          (↑z : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₂ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₃ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
    ∀ (i : ι),
      Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
        ((((b.repr : (a : E) → ι →₀ K) (-m + n) : ι →₀ K) : (a : ι) → K) i : K)
simp_rw₄ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HAdd.hAdd (α := K) (β := K) (-(((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)) ↔
    ∀ (i : ι),
      Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
        ((((b.repr : (a : E) → ι →₀ K) (-m + n) : ι →₀ K) : (a : ι) → K) i : K)
simp_rw₅ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HAdd.hAdd (α := K) (β := K) (-(((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)) ↔
    ∀ (i : ι),
      Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
        ((HAdd.hAdd (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) (-m) : ι →₀ K)
                ((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) :
              (a : ι) → K)
            i :
          K)
⊢ (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have simp_rw₆ : (∀ (i : ι),
    ∃ (z : ℤ),
      (↑z : K) =
        HAdd.hAdd (α := K) (β := K) (-(((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
          ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)) ↔
  ∀ (i : ι),
    Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
      ((HAdd.hAdd (α := ι →₀ K) (β := ι →₀ K) (-(b.repr : (a : E) → ι →₀ K) m : ι →₀ K)
              ((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) :
            (a : ι) → K)
          i :
        K)
Tactic: simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]