-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
L : Submodule ℤ E
inst_2 : DiscreteTopology.{u_1} ↥L
inst_3 : IsZLattice ℝ L
ι : Type u_2
inst_4 : Fintype ι
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
n : ℕ
hn : 0 < n
x : E
h :
  x ∈ s ∧ x ∈ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E) ↔
    Membership.mem.{u_2, u_2} (α := ι → ℝ) (γ := Set (ι → ℝ))
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
        ((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) :
              (a : E) → ι → ℝ)
            x :
          ι → ℝ) ∧
      Membership.mem (α := ι → ℝ)
        (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
        ((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) :
              (a : E) → ι → ℝ)
            x :
          ι → ℝ)
h₁ :
  x ∈ s ∧
      x ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
    Membership.mem.{u_2, u_2} (α := ι → ℝ) (γ := Set (ι → ℝ))
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
        ((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) :
              (a : E) → ι → ℝ)
            x :
          ι → ℝ) ∧
      Membership.mem (α := ι → ℝ)
        (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
        ((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) :
              (a : E) → ι → ℝ)
            x :
          ι → ℝ)
h₂ :
  x ∈ s ∧
      x ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
    Membership.mem.{u_2, u_2} (α := ι → ℝ) (γ := Set (ι → ℝ))
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ) ∧
      Membership.mem (α := ι → ℝ)
        (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)
h₃ :
  x ∈ s ∧
      x ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
    Membership.mem (γ := Set (ι → ℝ))
        ((fun (a : E) ↦
            (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                      (a : E) → ι →₀ ℝ)
                    a :
                  ι →₀ ℝ) :
              (a : ι) → ℝ)) ''
          s)
        (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                  (a : E) → ι →₀ ℝ)
                x :
              ι →₀ ℝ) :
          (a : ι) → ℝ) ∧
      (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                  (a : E) → ι →₀ ℝ)
                x :
              ι →₀ ℝ) :
          (a : ι) → ℝ) ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
h₄ :
  x ∈ s ∧
      x ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
    (∃ x_1 ∈ s,
        Eq.{u_2 + 1} (α := ι → ℝ)
          (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                    (a : E) → ι →₀ ℝ)
                  x_1 :
                ι →₀ ℝ) :
            (a : ι) → ℝ)
          (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                    (a : E) → ι →₀ ℝ)
                  x :
                ι →₀ ℝ) :
            (a : ι) → ℝ)) ∧
      (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                  (a : E) → ι →₀ ℝ)
                x :
              ι →₀ ℝ) :
          (a : ι) → ℝ) ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
h₅ :
  x ∈ s ∧
      x ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
    (∃ x_1 ∈ s,
        Eq.{u_2 + 1} (α := ι →₀ ℝ)
          (((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                (a : E) → ι →₀ ℝ)
              x_1 :
            ι →₀ ℝ)
          (((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                (a : E) → ι →₀ ℝ)
              x :
            ι →₀ ℝ)) ∧
      (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                  (a : E) → ι →₀ ℝ)
                x :
              ι →₀ ℝ) :
          (a : ι) → ℝ) ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ x ∈ s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E) ↔
    Membership.mem (α := ι → ℝ)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
      ((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) :
            (a : E) → ι → ℝ)
          x :
        ι → ℝ)
have h₆ : x ∈ s ∧
    x ∈
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
  (∃ x_1 ∈ s, x_1 = x) ∧
    (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                (a : E) → ι →₀ ℝ)
              x :
            ι →₀ ℝ) :
        (a : ι) → ℝ) ∈
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
Tactic: simp_rw [Set.mem_inter_iff, ← b.ofZLatticeBasis_span ℝ, LinearEquiv.coe_toEquiv,
      Basis.equivFun_apply, Set.mem_image, DFunLike.coe_fn_eq, EmbeddingLike.apply_eq_iff_eq,
      exists_eq_right, and_congr_right_iff, Set.mem_inv_smul_set_iff₀
      (mod_cast hn.ne' : (n : ℝ) ≠ 0), ← Finsupp.coe_smul, ← map_smul, SetLike.mem_coe,
      Basis.mem_span_iff_repr_mem, Pi.basisFun_repr, implies_true]