-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem covolume_eq_det_mul_measure {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ L)
    (b₀ : Basis ι ℝ E) :
    covolume L μ = |b₀.det ((↑) ∘ b)| * (μ (fundamentalDomain b₀)).toReal

Proof state:
case e_a.e_a.h.e_6.h.h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
x✝ : ι
⊢ (Basis.ofZLatticeBasis ℝ L b) x✝ = (Subtype.val ∘ ⇑b) x✝

Tactic:
exact b.ofZLatticeBasis_apply ℝ L _

Result:
no goals

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ 0 ≤ |b₀.det ⇑(Basis.ofZLatticeBasis ℝ L b)|

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * (μ (fundamentalDomain b₀)).toReal

Tactic:
rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),
  measure_fundamentalDomain _ _ b₀,
  measure_congr (fundamentalDomain_ae_parallelepiped b₀ μ), ENNReal.toReal_mul,
  ENNReal.toReal_ofReal (by positivity)]

Result:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ |b₀.det ⇑(Basis.ofZLatticeBasis ℝ L b)| * (μ (parallelepiped ⇑b₀)).toReal =
    |b₀.det (Subtype.val ∘ ⇑b)| * (μ (parallelepiped ⇑b₀)).toReal

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ |b₀.det ⇑(Basis.ofZLatticeBasis ℝ L b)| * (μ (parallelepiped ⇑b₀)).toReal =
    |b₀.det (Subtype.val ∘ ⇑b)| * (μ (parallelepiped ⇑b₀)).toReal

Tactic:
congr

Result:
case e_a.e_a.h.e_6.h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ ⇑(Basis.ofZLatticeBasis ℝ L b) = Subtype.val ∘ ⇑b

Proof state:
case e_a.e_a.h.e_6.h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ ⇑(Basis.ofZLatticeBasis ℝ L b) = Subtype.val ∘ ⇑b

Tactic:
ext

Result:
case e_a.e_a.h.e_6.h.h
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝² : Measure.IsAddHaarMeasure μ
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
b₀ : Basis ι ℝ E
x✝ : ι
⊢ (Basis.ofZLatticeBasis ℝ L b) x✝ = (Subtype.val ∘ ⇑b) x✝