awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
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 ι) : ℝ)⁻¹
⊢ ((fun (x : ℝ) ↦
          (↑(Nat.card.{u_2}
                  (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                          {x : E | x ∈ X ∧ F x ≤ 1} ∩
                        x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                    Type u_2)) :
              ℝ) /
            x ^ card ι) ∘
        fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (↑(card ι) : ℝ)⁻¹)
      c =
    (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c
have aux₃ : (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ ≠ 0
Tactic: have aux₃ : (c ^ (card ι : ℝ)⁻¹)⁻¹ ≠ 0 := inv_ne_zero aux₂.ne'
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
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
⊢ ((fun (x : ℝ) ↦
          (↑(Nat.card.{u_2}
                  (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                          {x : E | x ∈ X ∧ F x ≤ 1} ∩
                        x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                    Type u_2)) :
              ℝ) /
            x ^ card ι) ∘
        fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (↑(card ι) : ℝ)⁻¹)
      c =
    (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c
have aux₄ : HPow.hPow (β := ℝ) c (-(↑(card ι) : ℝ)⁻¹) ≠ 0
Tactic: have aux₄ : c ^ (-(card ι : ℝ)⁻¹) ≠ 0 := (Real.rpow_pos_of_pos hc _).ne'
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
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
⊢ ((fun (x : ℝ) ↦
          (↑(Nat.card.{u_2}
                  (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                          {x : E | x ∈ X ∧ F x ≤ 1} ∩
                        x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                    Type u_2)) :
              ℝ) /
            x ^ card ι) ∘
        fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (↑(card ι) : ℝ)⁻¹)
      c =
    (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c
have hc₁ : 0 ≤ c
Tactic: obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
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
⊢ ((fun (x : ℝ) ↦
          (↑(Nat.card.{u_2}
                  (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                          {x : E | x ∈ X ∧ F x ≤ 1} ∩
                        x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                    Type u_2)) :
              ℝ) /
            x ^ card ι) ∘
        fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (↑(card ι) : ℝ)⁻¹)
      c =
    (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c
have hc₂ : 0 ≠ c
Tactic: obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc
-- 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
⊢ ((fun (x : ℝ) ↦
          (↑(Nat.card.{u_2}
                  (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                          {x : E | x ∈ X ∧ F x ≤ 1} ∩
                        x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                    Type u_2)) :
              ℝ) /
            x ^ card ι) ∘
        fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (↑(card ι) : ℝ)⁻¹)
      c =
    (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c
have h : (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c =
  (↑(Nat.card.{u_2}
          (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                  {x : E | x ∈ X ∧ F x ≤ 1} ∩
                (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ •
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_2)) :
      ℝ) /
    c
Tactic: rw [Function.comp_apply, ← Real.rpow_natCast, Real.rpow_inv_rpow hc₁ aux₁, eq_comm]
-- 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
⊢ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c =
    (↑(Nat.card.{u_2}
            (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                    {x : E | x ∈ X ∧ F x ≤ 1} ∩
                  (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ •
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_2)) :
        ℝ) /
      c
have h : Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1) =
  Nat.card.{u_2}
    (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
            {x : E | x ∈ X ∧ F x ≤ 1} ∩
          (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ •
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_2)
Tactic: congr
-- 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
⊢ Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1) =
    Nat.card.{u_2}
      (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
              {x : E | x ∈ X ∧ F x ≤ 1} ∩
            (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ •
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_2)
have h : ∀ (x : E),
  x ∈ {x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E) ↔
    Membership.mem (α := ι → ℝ)
      (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1} ∩
        (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ •
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
      (((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))).trans
              (Equiv.smulRight aux₄) :
            (a : E) → ι → ℝ)
          x :
        ι → ℝ)
Tactic: refine Nat.card_congr <| Equiv.subtypeEquiv ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.trans
          (Equiv.smulRight aux₄)) fun _ ↦ ?_
-- 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
⊢ x ∈ {x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E) ↔
    Membership.mem (α := ι → ℝ)
      (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1} ∩
        (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ •
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
      (((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))).trans
              (Equiv.smulRight aux₄) :
            (a : E) → ι → ℝ)
          x :
        ι → ℝ)
have h : 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: rw [Set.mem_inter_iff, Set.mem_inter_iff, Equiv.trans_apply, LinearEquiv.coe_toEquiv,
      Equiv.smulRight_apply, Real.rpow_neg hc₁, Set.smul_mem_smul_set_iff₀ aux₃,
      ← Set.mem_smul_set_iff_inv_smul_mem₀ aux₂.ne', ← image_smul_set,
      tendsto_card_le_div''_aux hX h₁ aux₂, ← Real.rpow_natCast, ← Real.rpow_mul hc₁,
      inv_mul_cancel₀ aux₁, Real.rpow_one]
-- 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
⊢ 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 ↔
  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 : ι → ℝ)
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]
-- 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 : ι → ℝ)
⊢ 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 ∧
        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 : ι → ℝ)
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]
-- 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)
⊢ Bornology.IsBounded.{u_2} (α := ι → ℝ)
    (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
      {x : E | x ∈ X ∧ F x ≤ 1})
have refine_2 : ∀ (h₂ : IsVonNBounded.{0, u_1} ℝ (E := 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)),
  IsVonNBounded.{0, u_2} ℝ (E := ι → ℝ)
    (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
      {x : E | x ∈ X ∧ F x ≤ 1})
Tactic: rw [← NormedSpace.isVonNBounded_iff ℝ] at h₂ ⊢
Cleared hypotheses: h₂, h₃, h₄