-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem covolume_comap {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
    [MeasurableSpace F] [BorelSpace F] (ν : Measure F

Proof state:
case h.e'_1.h.e'_6.h.e'_7.a
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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
i✝ : Free.ChooseBasisIndex ℤ ↥L
⊢ (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑e.toLinearEquiv)
        (Basis.ofZLatticeComap ℝ L e.toLinearEquiv (Free.chooseBasis ℤ ↥L)))
      i✝ =
    ((Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map e.symm.toLinearEquiv) i✝

Tactic:
simp

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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ (ν
        (fundamentalDomain
          (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑e.toLinearEquiv)
            (Basis.ofZLatticeComap ℝ L e.toLinearEquiv (Free.chooseBasis ℤ ↥L))))).toReal =
    (ν (fundamentalDomain ((Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map e.symm.toLinearEquiv))).toReal

Tactic:
congr!

Result:
case h.e'_1.h.e'_6.h.e'_7
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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑e.toLinearEquiv)
      (Basis.ofZLatticeComap ℝ L e.toLinearEquiv (Free.chooseBasis ℤ ↥L)) =
    (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map e.symm.toLinearEquiv

Proof state:
case h.e'_1.h.e'_6.h.e'_7
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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑e.toLinearEquiv)
      (Basis.ofZLatticeComap ℝ L e.toLinearEquiv (Free.chooseBasis ℤ ↥L)) =
    (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map e.symm.toLinearEquiv

Tactic:
ext

Result:
case h.e'_1.h.e'_6.h.e'_7.a
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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
i✝ : Free.ChooseBasisIndex ℤ ↥L
⊢ (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑e.toLinearEquiv)
        (Basis.ofZLatticeComap ℝ L e.toLinearEquiv (Free.chooseBasis ℤ ↥L)))
      i✝ =
    ((Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map e.symm.toLinearEquiv) i✝

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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ covolume (ZLattice.comap ℝ L ↑e.toLinearEquiv) ν = covolume L μ

Tactic:
rw [covolume_eq_measure_fundamentalDomain _ _ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
  covolume_eq_measure_fundamentalDomain _ _ ((isAddFundamentalDomain
  ((Free.chooseBasis ℤ L).ofZLatticeComap ℝ L e.toLinearEquiv) ν)), ← he.measure_preimage
  (fundamentalDomain_measurableSet _).nullMeasurableSet, ← e.image_symm_eq_preimage,
  ← e.symm.coe_toLinearEquiv, map_fundamentalDomain]

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 μ
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : autoParam (Measure F) _auto✝
inst✝ : Measure.IsAddHaarMeasure ν
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ (ν
        (fundamentalDomain
          (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑e.toLinearEquiv)
            (Basis.ofZLatticeComap ℝ L e.toLinearEquiv (Free.chooseBasis ℤ ↥L))))).toReal =
    (ν (fundamentalDomain ((Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map e.symm.toLinearEquiv))).toReal