-- 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 v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
i : ι
h₁ :
  HSub.hSub (α := K) (β := K)
      ((HAdd.hAdd (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) v : ι →₀ K)
              ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) :
            (a : ι) → K)
          i :
        K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
h₂ :
  HSub.hSub (β := K)
      (HAdd.hAdd (α := (a : ι) → K) (β := (a : ι) → K) (⇑((b.repr : (a : E) → ι →₀ K) v : ι →₀ K) : (a : ι) → K)
        (⇑((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
h₃ :
  HSub.hSub (β := K)
      (HAdd.hAdd (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K))
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
h₄ :
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                      LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                        (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                    (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                  (Subtype.mk (p := fun (x : E) ↦
                    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
                      x)
                    v h) :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        K) :
      K)
⊢ HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) (v + m) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
have h₅ : Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) i : K)
  ((algebraMap ℤ K : (a : ℤ) → K)
      (((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i :
        ℤ) :
    K)
Tactic: rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]