-- 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
inst_8 : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier
          (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
            {x : E | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)
c : ℝ
hc : 0 < c
aux₁ : Ne (α := ℝ) (↑(card ι) : ℝ) 0
aux₂ : 0 < HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹
aux₃ : (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ ≠ 0
aux₄ : HPow.hPow (β := ℝ) c (-(↑(card ι) : ℝ)⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x : E
h :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x ∧ x ∈ L ↔
    Membership.mem.{u_2, u_2} (α := ι → ℝ) (γ := Set (ι → ℝ))
        (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ c})
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ) ∧
      Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)
h₅ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x ∧ x ∈ L ↔
    (∃ (x_1 : E),
        Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x_1 ∧
          Eq.{u_2 + 1} (α := ι → ℝ) ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x_1 : ι → ℝ)
            ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)) ∧
      Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)
h₆ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x ∧ x ∈ L ↔
    (∃ (x_1 : E), Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x_1 ∧ x_1 = x) ∧
      Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)
h₇ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x ∧ x ∈ L ↔
    Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x ∧
      Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)
h₈ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x →
    (x ∈ L ↔
      Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ))
h₉ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x →
    (Membership.mem (γ := Submodule ℤ E)
        (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) x ↔
      Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ))
h₁₀ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x →
    ((∀ (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) → ι →₀ ℝ)
                    x :
                  ι →₀ ℝ) :
                (a : ι) → ℝ)
              i :
            ℝ)) ↔
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
          ((((Basis.repr (Pi.basisFun ℝ ι) : (a : ι → ℝ) → ι →₀ ℝ)
                    ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ) :
                  ι →₀ ℝ) :
                (a : ι) → ℝ)
              i :
            ℝ))
h₁₁ :
  Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x →
    ((∀ (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) → ι →₀ ℝ)
                    x :
                  ι →₀ ℝ) :
                (a : ι) → ℝ)
              i :
            ℝ)) ↔
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
          ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x i : ℝ))
h₁₂ : Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x → True
⊢ Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c} x ∧ x ∈ (↑L : Set E) ↔
    Membership.mem.{u_2, u_2} (α := ι → ℝ) (γ := Set (ι → ℝ))
        (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ c})
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ) ∧
      Membership.mem (α := ι → ℝ) (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
        ((Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (a : E) → ι → ℝ) x : ι → ℝ)

Tactic:
simp_rw [SetLike.mem_coe, Set.mem_image, EmbeddingLike.apply_eq_iff_eq, exists_eq_right,
      and_congr_right_iff, ← b.ofZLatticeBasis_span ℝ, Basis.mem_span_iff_repr_mem,
      Pi.basisFun_repr, Basis.equivFun_apply, implies_true]

Premises used: Real, Set.mem_image, exists_eq_right, Module.Basis.ofZLatticeBasis_span, and_congr_right_iff, EmbeddingLike.apply_eq_iff_eq, SetLike.mem_coe, Module.Basis.equivFun_apply, implies_true, Pi.basisFun_repr, Module.Basis.mem_span_iff_repr_mem