-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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 (ι → ℝ))
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 (ι → ℝ))
h₇ :
  x ∈ s ∧
      x ∈
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
    x ∈ s ∧
      (⇑(((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) ↔
      (⇑(((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 →
    (HSMul.hSMul (α := ℝ) (↑n : ℝ) x ∈
        (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
      HSMul.hSMul (α := ℝ) (β := ι → ℝ) (↑n : ℝ)
          (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                    (a : E) → ι →₀ ℝ)
                  x :
                ι →₀ ℝ) :
            (a : ι) → ℝ) ∈
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
h₁₀ :
  x ∈ s →
    (HSMul.hSMul (α := ℝ) (↑n : ℝ) x ∈
        (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
      (⇑(HSMul.hSMul (α := ℝ) (β := ι →₀ ℝ) (↑n : ℝ)
              (((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                    (a : E) → ι →₀ ℝ)
                  x :
                ι →₀ ℝ)) :
          (a : ι) → ℝ) ∈
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
h₁₁ :
  x ∈ s →
    (HSMul.hSMul (α := ℝ) (↑n : ℝ) x ∈
        (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) : Set E) ↔
      (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                  (a : E) → ι →₀ ℝ)
                (HSMul.hSMul (α := ℝ) (↑n : ℝ) x) :
              ι →₀ ℝ) :
          (a : ι) → ℝ) ∈
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
h₁₂ :
  x ∈ s →
    (Membership.mem (γ := Submodule ℤ E)
        (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E)))
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) x) ↔
      Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                  (a : E) → ι →₀ ℝ)
                (HSMul.hSMul (α := ℝ) (↑n : ℝ) x) :
              ι →₀ ℝ) :
          (a : ι) → ℝ))
h₁₃ :
  x ∈ s →
    ((∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
          (((((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                      (a : E) → ι →₀ ℝ)
                    (HSMul.hSMul (α := ℝ) (↑n : ℝ) x) :
                  ι →₀ ℝ) :
                (a : ι) → ℝ)
              i :
            ℝ)) ↔
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
          ((((Basis.repr (Pi.basisFun ℝ ι) : (a : ι → ℝ) → ι →₀ ℝ)
                    (⇑(((Basis.repr (Basis.ofZLatticeBasis ℝ L b) :
                                LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι →₀ ℝ)) :
                              (a : E) → ι →₀ ℝ)
                            (HSMul.hSMul (α := ℝ) (↑n : ℝ) x) :
                          ι →₀ ℝ) :
                      (a : ι) → ℝ) :
                  ι →₀ ℝ) :
                (a : ι) → ℝ)
              i :
            ℝ))
h₁₄ : x ∈ s → True
⊢ 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 :
        ι → ℝ)

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]

Premises used: LinearEquiv.coe_toEquiv, Real, Set.mem_inv_smul_set_iff₀, congrArg, Set.mem_inter_iff, cast, Set.mem_image, exists_eq_right, Module.Basis.ofZLatticeBasis_span, Ne, and_congr_right_iff, EmbeddingLike.apply_eq_iff_eq, Nat.cast, LT.lt.ne', Finsupp.coe_smul, DFunLike.coe_fn_eq, SetLike.mem_coe, Module.Basis.equivFun_apply, Nat.cast_inj._simp_1, implies_true, Nat.cast_zero, Eq.symm, Pi.basisFun_repr, Not, Module.Basis.mem_span_iff_repr_mem, Eq.trans, map_smul