-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
x : ↥L
i_1 i : ι
simp_rw :
  Eq (α := ι →₀ K)
    (Function.comp (α := ↥L) (β := E)
      (⇑((↑ℤ :
              {S : Type u_1} →
                {M : Type u_2} →
                  {M₂ : Type (max u_1 u_3)} →
                    [inst : Semiring ℤ] →
                      [inst_10 : Semiring S] →
                        [inst_11 : AddCommMonoid M] →
                          [inst_12 : AddCommMonoid M₂] →
                            [inst_13 : Module ℤ M] →
                              [inst_14 : Module ℤ M₂] →
                                [inst_15 : Module S M] →
                                  [inst_16 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K)) :
        (a : E) → ι →₀ K)
      ((⇑L.subtype : (a : ↥L) → E) : (a : ↥L) → E) ((b : (a : ι) → ↥L) i : ↥L))
    (Function.comp (α := ↥L) (β := ι →₀ ℤ)
      (⇑(Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K)) : (a : ι →₀ ℤ) → ι →₀ K)
      ((⇑(↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ ℤ) : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i : ↥L))
simp_rw₁ :
  Eq (α := ι →₀ K)
    (((↑ℤ :
              {S : Type u_1} →
                {M : Type u_2} →
                  {M₂ : Type (max u_1 u_3)} →
                    [inst : Semiring ℤ] →
                      [inst_10 : Semiring S] →
                        [inst_11 : AddCommMonoid M] →
                          [inst_12 : AddCommMonoid M₂] →
                            [inst_13 : Module ℤ M] →
                              [inst_14 : Module ℤ M₂] →
                                [inst_15 : Module S M] →
                                  [inst_16 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) :
          (a : E) → ι →₀ K)
        ((L.subtype : (a : ↥L) → E) ((b : (a : ι) → ↥L) i : ↥L)) :
      ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) : (a : ι →₀ ℤ) → ι →₀ K)
        (((↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i)) :
      ι →₀ K)
simp_rw₂ :
  Eq (α := ι →₀ K)
    (((↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) : (a : E) → ι →₀ K)
        ((L.subtype : (a : ↥L) → E) ((b : (a : ι) → ↥L) i : ↥L)) :
      ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) : (a : ι →₀ ℤ) → ι →₀ K)
        (((↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i)) :
      ι →₀ K)
simp_rw₃ :
  Eq (α := ι →₀ K)
    ((repr (ofZLatticeBasis K L b) : (a : E) → ι →₀ K) ((L.subtype : (a : ↥L) → E) ((b : (a : ι) → ↥L) i : ↥L)) :
      ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) : (a : ι →₀ ℤ) → ι →₀ K)
        ((b.repr : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i)) :
      ι →₀ K)
simp_rw₄ :
  Eq (α := ι →₀ K) ((repr (ofZLatticeBasis K L b) : (a : E) → ι →₀ K) (↑((b : (a : ι) → ↥L) i) : E) : ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) : (a : ι →₀ ℤ) → ι →₀ K)
        ((b.repr : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i)) :
      ι →₀ K)
⊢ Eq (α := ι →₀ K)
    (((↑ℤ :
                {S : Type u_1} →
                  {M : Type u_2} →
                    {M₂ : Type (max u_1 u_3)} →
                      [inst : Semiring ℤ] →
                        [inst_10 : Semiring S] →
                          [inst_11 : AddCommMonoid M] →
                            [inst_12 : AddCommMonoid M₂] →
                              [inst_13 : Module ℤ M] →
                                [inst_14 : Module ℤ M₂] →
                                  [inst_15 : Module S M] →
                                    [inst_16 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) ∘ₗ
            L.subtype :
          (a : ↥L) → ι →₀ K)
        ((b : (a : ι) → ↥L) i) :
      ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ (↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ K)
        ((b : (a : ι) → ↥L) i) :
      ι →₀ K)
have simp_rw₅ : Eq (α := ι →₀ K) ((repr (ofZLatticeBasis K L b) : (a : E) → ι →₀ K) ((ofZLatticeBasis K L b : (a : ι) → E) i) : ι →₀ K)
  ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) : (a : ι →₀ ℤ) → ι →₀ K)
      ((b.repr : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i)) :
    ι →₀ K)
Tactic: simp_rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, coe_subtype, ← b.ofZLatticeBasis_apply K, repr_self,
    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]