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