-- 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 :
          ι → ℝ)
⊢ 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) ↔
  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 : ι → ℝ)
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]