awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
h : F x ≤ c ^ card ι → (c⁻¹ • x ∈ X ↔ x ∈ X)
⊢ x ∈ HSMul.hSMul (β := Set E) c {x : E | x ∈ X ∧ F x ≤ 1} ↔
    Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c ^ card ι} x

Tactic:
simp_rw [Set.mem_smul_set_iff_inv_smul_mem₀ hc.ne', Set.mem_setOf_eq, hF₁ _
    (inv_pos_of_pos hc).le, inv_pow, inv_mul_le_iff₀ (pow_pos hc _), mul_one, and_congr_left_iff]

Premises used: pow_pos, LT.lt.le, Set.mem_setOf_eq, inv_pow, inv_pos_of_pos, LT.lt.ne', inv_mul_le_iff₀, and_congr_left_iff, mul_one, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ F x ≤ c ^ card ι → (c⁻¹ • x ∈ X ↔ x ∈ X)

Tactic:
fun _ ↦ ⟨fun h ↦ (smul_inv_smul₀ hc.ne' x) ▸ hX h hc, fun h ↦ hX h (inv_pos_of_pos hc)⟩

Premises used: smul_inv_smul₀, Eq.rec, inv_pos_of_pos, LT.lt.ne', Iff.intro
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ F x ≤ c ^ card ι → (c⁻¹ • x ∈ X ↔ x ∈ X)

Tactic:
exact fun _ ↦ ⟨fun h ↦ (smul_inv_smul₀ hc.ne' x) ▸ hX h hc, fun h ↦ hX h (inv_pos_of_pos hc)⟩
-- 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)
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c) atTop
    (𝓝
      (Measure.real.{u_2} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1})))

Tactic:
Tendsto.congr' ?_ <| (tendsto_card_div_pow_atTop_volume'
      ((b.ofZLatticeBasis ℝ).equivFun '' {x ∈ X | F x ≤ 1}) ?_ ?_ h₄ fun x y hx hy ↦ ?_).comp
        (tendsto_rpow_atTop <| inv_pos.mpr
          (Nat.cast_pos.mpr card_pos) : Tendsto (fun x ↦ x ^ (card ι : ℝ)⁻¹) atTop atTop)

Premises used: Iff.mpr, Real, Nat.cast_pos, tendsto_rpow_atTop, setOf, Module.Basis.ofZLatticeBasis, Membership.mem, inv_pos, LE.le, And, Set.image, tendsto_card_div_pow_atTop_volume', Filter.Tendsto.comp, Filter.Tendsto.congr', OfNat.ofNat, DFunLike.coe, Fintype.card_pos, Module.Basis.equivFun
-- 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)
h :
  ∀ (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
⊢ EventuallyEq (β := ℝ) atTop
    ((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 ι) : ℝ)⁻¹)
    fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c

Tactic:
filter_upwards [eventually_gt_atTop 0] with c hc

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- 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
⊢ Ne (α := ℝ) (↑(card ι) : ℝ) 0

Tactic:
have aux₁ : (card ι : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr card_ne_zero
-- 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
⊢ 0 < HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹

Tactic:
have aux₂ : 0 < c ^ (card ι : ℝ)⁻¹ := Real.rpow_pos_of_pos hc _
-- 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 ι) : ℝ)⁻¹
⊢ (HPow.hPow (β := ℝ) c (↑(card ι) : ℝ)⁻¹)⁻¹ ≠ 0

Tactic:
have aux₃ : (c ^ (card ι : ℝ)⁻¹)⁻¹ ≠ 0 := inv_ne_zero aux₂.ne'
-- 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
⊢ HPow.hPow (β := ℝ) c (-(↑(card ι) : ℝ)⁻¹) ≠ 0

Tactic:
have aux₄ : c ^ (-(card ι : ℝ)⁻¹) ≠ 0 := (Real.rpow_pos_of_pos hc _).ne'
-- 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
⊢ 0 ≤ c

Tactic:
obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc

Premises used: lt_iff_le_and_ne, Iff.mp
-- 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
⊢ 0 ≠ c

Tactic:
obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc

Premises used: lt_iff_le_and_ne, Iff.mp
-- 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
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
⊢ ((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

Tactic:
rw [Function.comp_apply, ← Real.rpow_natCast, Real.rpow_inv_rpow hc₁ aux₁, eq_comm]

Premises used: eq_comm, Function.comp_apply, Real.rpow_inv_rpow, Real.rpow_natCast
-- 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
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)
⊢ (↑(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:
congr
-- 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
⊢ 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:
Nat.card_congr <| Equiv.subtypeEquiv ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.trans
          (Equiv.smulRight aux₄)) fun _ ↦ ?_

Premises used: Real, Equiv.trans, Module.Basis.ofZLatticeBasis, Equiv.subtypeEquiv, Nat.card_congr, LinearEquiv.toEquiv, Equiv.smulRight, Module.Basis.equivFun
-- 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
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 :
          ι → ℝ)
⊢ 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:
refine Nat.card_congr <| Equiv.subtypeEquiv ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.trans
          (Equiv.smulRight aux₄)) fun _ ↦ ?_

Premises used: Real, Equiv.trans, Module.Basis.ofZLatticeBasis, Equiv.subtypeEquiv, Nat.card_congr, LinearEquiv.toEquiv, Equiv.smulRight, Module.Basis.equivFun