awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₅ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₆ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) (span K (↑L : Set E)) = ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₆ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) (span K (↑L : Set E)) = ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₇ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) ⊤ = ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₆ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) (span K (↑L : Set E)) = ⊤
rw₇ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) ⊤ = ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₈ : (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F).range = ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₂ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₃ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e.symm : (a : E) → F) '' (↑L : Set E))) ⊤
rw₄ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e.symm : E ≃ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₅ :
  Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) : (a : E) → F) '' (↑L : Set E))) ⊤
rw₆ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) (span K (↑L : Set E)) = ⊤
rw₇ : Submodule.map (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F) ⊤ = ⊤
rw₈ : (↑(↑e.symm : E ≃ₗ[K] F) : E →ₗ[K] F).range = ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₉ : Eq.{u_3 + 1} (α := Submodule K F) ⊤ ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x_1 : ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))
x : F
hx : x ∈ ZLattice.comap K L (↑e : F →ₗ[K] E)
⊢ Membership.mem (α := E) L ((e : (a : F) → E) x : E)
have rwa : ∀ (hx : x ∈ (↑(ZLattice.comap K L (↑e : F →ₗ[K] E)) : Set F)), Membership.mem (α := E) L ((e : (a : F) → E) x : E)
Tactic: rwa [← SetLike.mem_coe, ZLattice.coe_comap] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x_1 : ↥(ZLattice.comap K L (↑e : F →ₗ[K] E))
x : F
hx : x ∈ ZLattice.comap K L (↑e : F →ₗ[K] E)
rwa : ∀ (hx : x ∈ (↑(ZLattice.comap K L (↑e : F →ₗ[K] E)) : Set F)), Membership.mem (α := E) L ((e : (a : F) → E) x : E)
⊢ Membership.mem (α := E) L ((e : (a : F) → E) x : E)
have rwa₁ : ∀ (hx : Membership.mem (γ := Set F) ((⇑(↑e : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E)) x),
  Membership.mem (α := E) L ((e : (a : F) → E) x : E)
Tactic: rwa [← SetLike.mem_coe, ZLattice.coe_comap] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
F : Type u_3
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace K F
inst_11 : FiniteDimensional K F
inst_12 : ProperSpace F
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_2} ↥L
inst_14 : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis.{u_4, 0, u_2} ι ℤ ↥L
⊢ ofZLatticeBasis K (ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) (ofZLatticeComap K L (↑e : F ≃ₗ[K] E) b) =
    Basis.map (ofZLatticeBasis K L b) (↑e.symm : E ≃ₗ[K] F)
have a : ∀ (i : ι),
  Eq.{u_3 + 1} (α := F)
    ((ofZLatticeBasis K (ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) (ofZLatticeComap K L (↑e : F ≃ₗ[K] E) b) :
          (a : ι) → F)
        i :
      F)
    ((Basis.map (ofZLatticeBasis K L b) (↑e.symm : E ≃ₗ[K] F) : (a : ι) → F) i : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
⊢ IsCompact (Set.range f)
have this : Free.{0, u_1} ℤ ↥L
Tactic: have := ZLattice.module_free ℝ L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ IsCompact (Set.range f)
have h : Set.range f = f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
Tactic: convert! (b.ofZLatticeBasis ℝ).parallelepiped.isCompact.image hf
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Set.range f = f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
have h : Set.range f ≤ f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
Tactic: refine le_antisymm ?_ (Set.image_subset_range _ _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : E
x' : ↥L :=
  (b.repr.symm : (a : Free.ChooseBasisIndex ℤ ↥L →₀ ℤ) → ↥L)
    ((Equiv.symm Finsupp.equivFunOnFinite : (a : Free.ChooseBasisIndex ℤ ↥L → ℤ) → Free.ChooseBasisIndex ℤ ↥L →₀ ℤ)
      fun (i : Free.ChooseBasisIndex ℤ ↥L) ↦
      Int.floor (α := ℝ)
        ((((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : (a : E) → Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) x :
                Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) :
              (a : Free.ChooseBasisIndex ℤ ↥L) → ℝ)
            i :
          ℝ))
⊢ f x ∈ f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
have h : x + -(↑x' : E) ∈ (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
Tactic: refine ⟨x + (- x'), ?_, hf' _ _ (- x').2⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
⊢ covolume L μ = μ.real F
have this : MeasurableVAdd (↥L) E
Tactic: have : MeasurableVAdd L E := (inferInstance : MeasurableVAdd L.toAddSubgroup E)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this : MeasurableVAdd (↥L) E
⊢ covolume L μ = μ.real F
have this₁ : VAddInvariantMeasure (↥L) E μ
Tactic: have : VAddInvariantMeasure L E μ := (inferInstance : VAddInvariantMeasure L.toAddSubgroup E μ)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
⊢ covolume L μ ≠ 0
have rw : Ne (α := ENNReal)
  ((μ : (a : Set E) → ENNReal)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
    ENNReal)
  (0 : ENNReal)
Tactic: rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
    measureReal_ne_zero_iff (ne_of_lt _)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
rw :
  Ne (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (0 : ENNReal)
⊢ covolume L μ ≠ 0
have rw₁ : LT.lt (α := ENNReal)
  ((μ : (a : Set E) → ENNReal)
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
    ENNReal)
  (⊤ : ENNReal)
Tactic: rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
    measureReal_ne_zero_iff (ne_of_lt _)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
⊢ covolume (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E)) ν = covolume L μ
have rw : ν.real
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
      (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
        (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))) =
  ν.real
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
      (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F)))
Tactic: rw [covolume_eq_measure_fundamentalDomain _ _ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
    covolume_eq_measure_fundamentalDomain _ _ ((isAddFundamentalDomain
    ((Free.chooseBasis ℤ L).ofZLatticeComap ℝ L e.toLinearEquiv) ν)), ← he.measureReal_preimage
    (fundamentalDomain_measurableSet _).nullMeasurableSet, ← e.image_symm_eq_preimage,
    ← e.symm.coe_toLinearEquiv, map_fundamentalDomain]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
⊢ ν.real
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
        (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
          (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))) =
    ν.real
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
        (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F)))
have h : Eq (α := Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ ↥L) ℝ F)
  (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
    (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))
  (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F))
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
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
⊢ Eq (α := Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ ↥L) ℝ F)
    (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
      (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))
    (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F))
have h : ∀ (i : Free.ChooseBasisIndex ℤ ↥L),
  Eq.{u_2 + 1} (α := F)
    ((Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
            (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)) :
          (a : Free.ChooseBasisIndex ℤ ↥L) → F)
        i :
      F)
    ((Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F) :
          (a : Free.ChooseBasisIndex ℤ ↥L) → F)
        i :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
ι : Type u_2
inst_8 : Fintype ι
inst_9 : DecidableEq ι
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ covolume L μ =
    HMul.hMul (α := ℝ)
      (|(b₀.det : (a : ι → E) → ℝ)
            (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))| :
        ℝ)
      (μ.real (fundamentalDomain b₀))
have rw : HMul.hMul (α := ℝ) (|(b₀.det : (a : ι → E) → ℝ) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E)| : ℝ)
    (μ.real (parallelepiped.{u_2, u_1} (ι := ι) (⇑b₀ : (a : ι) → E))) =
  HMul.hMul (α := ℝ)
    (|(b₀.det : (a : ι → E) → ℝ)
          (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))| :
      ℝ)
    (μ.real (parallelepiped.{u_2, u_1} (ι := ι) (⇑b₀ : (a : ι) → E)))
Tactic: rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),
    measureReal_fundamentalDomain _ _ b₀,
    measureReal_congr (fundamentalDomain_ae_parallelepiped b₀ μ)]