awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
have have₁ have₂ :
  ∀ (this : FiniteDimensional ℝ E), fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have have₃ : ∀ (this : FiniteDimensional ℝ E),
  Eq (α := ENNReal)
    ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
      ENNReal)
    (0 : ENNReal)
Tactic: classical
  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
  rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
  suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
      AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by
    refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
    refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
    simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
    exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
  intro x hx
  simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_diff, Set.mem_setOf_eq,
    mem_fundamentalDomain, Set.mem_Ico, not_forall, not_and, not_lt] at hx
  obtain ⟨i, hi⟩ := hx.2
  have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
  rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
  refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
  exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
have have₁ have₂ :
  ∀ (this : FiniteDimensional ℝ E), fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have₃ :
  ∀ (this : FiniteDimensional ℝ E),
    Eq (α := ENNReal)
      ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
        ENNReal)
      (0 : ENNReal)
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have have₄ : ∀ (this : FiniteDimensional ℝ E),
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
Tactic: classical
  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
  rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
  suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
      AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by
    refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
    refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
    simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
    exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
  intro x hx
  simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_diff, Set.mem_setOf_eq,
    mem_fundamentalDomain, Set.mem_Ico, not_forall, not_and, not_lt] at hx
  obtain ⟨i, hi⟩ := hx.2
  have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
  rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
  refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
  exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
have have₁ have₂ :
  ∀ (this : FiniteDimensional ℝ E), fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have₃ :
  ∀ (this : FiniteDimensional ℝ E),
    Eq (α := ENNReal)
      ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
        ENNReal)
      (0 : ENNReal)
have₄ :
  ∀ (this : FiniteDimensional ℝ E),
    parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
      ⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E)
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have have₅ : ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
  (hx : x ∈ parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b),
  Membership.mem (γ := Set E)
    (⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E))
    x
Tactic: classical
  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
  rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
  suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
      AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by
    refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
    refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
    simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
    exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
  intro x hx
  simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_diff, Set.mem_setOf_eq,
    mem_fundamentalDomain, Set.mem_Ico, not_forall, not_and, not_lt] at hx
  obtain ⟨i, hi⟩ := hx.2
  have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
  rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
  refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
  exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
⊢ L.FG
have obtain : ∀ (s : Set E) (h_incl : s ⊆ (↑L : Set E)) (h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E)))
  (h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))),
  L.FG
Tactic: obtain ⟨s, ⟨h_incl, ⟨h_span, h_lind⟩⟩⟩ := exists_linearIndependent K (L : Set E)
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ L.FG
have refine_1 : Submodule.FG (M := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (Submodule.map (mkQ (span ℤ s)) L)
Tactic: refine fg_of_fg_map_of_fg_inf_ker (span ℤ s).mkQ ?_ ?_
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
refine_1 : Submodule.FG (M := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (Submodule.map (mkQ (span ℤ s)) L)
⊢ L.FG
have refine_2 : (L ⊓ LinearMap.ker (M₂ := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (mkQ (span ℤ s))).FG
Tactic: refine fg_of_fg_map_of_fg_inf_ker (span ℤ s).mkQ ?_ ?_
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ Submodule.FG (M := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (Submodule.map (mkQ (span ℤ s)) L)
have refine_1 : (↑(Submodule.map (mkQ (span ℤ s)) L) : Set (E ⧸ span ℤ s)).Finite
Tactic: refine fg_def.mpr ⟨map (span ℤ s).mkQ L, ?_, span_eq _⟩
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ LE.le.{u_2} (α := Submodule K E) ⊤
    (span K (Set.range (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))))
have rw : LE.le (α := Submodule K E) (span K s)
  (span K (Set.range (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))))
Tactic: rw [← hs.span_top, ← h_span]
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ (↑(Submodule.map (mkQ (span ℤ s)) L) : Set (E ⧸ span ℤ s)).Finite
have refine_1 : (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
    Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite
Tactic: rw [show span ℤ s = span ℤ (Set.range b) by simp [b, Basis.coe_mk, Subtype.range_coe_subtype]]
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite
have refine_1 : ∀ (this : Fintype (↑s : Type u_2)),
  (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite
Tactic: have : Fintype s := h_lind.setFinite.fintype
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite
have refine_1 : Set.Finite (α := E)
  (Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
      (⇑(quotientEquiv b) :
        (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
    (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))))
Tactic: refine Set.Finite.of_finite_image (f := ((↑) : _ → E) ∘ quotientEquiv b) ?_
      (Function.Injective.injOn (Subtype.coe_injective.comp (quotientEquiv b).injective))
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ (fundamentalDomain b ∩ (↑L : Set E)).Finite
have change : (fundamentalDomain b ∩ (↑L.toAddSubgroup : Set E)).Finite
Tactic: change ((fundamentalDomain b) ∩ L.toAddSubgroup).Finite
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ (fundamentalDomain b ∩ (↑L.toAddSubgroup : Set E)).Finite
have this₁ : DiscreteTopology.{u_2} ↥L.toAddSubgroup
Tactic: have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ Set.Finite (α := E)
    (Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
        (⇑(quotientEquiv b) :
          (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
      (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))))
have this₁ : (fundamentalDomain b ∩ (↑L : Set E)).Finite
Tactic: have : ((fundamentalDomain b) ∩ L).Finite := by
      change ((fundamentalDomain b) ∩ L.toAddSubgroup).Finite
      have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
      exact Metric.finite_isBounded_inter_isClosed
        DiscreteTopology.isDiscrete (fundamentalDomain_isBounded b) inferInstance
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
⊢ Set.Finite (α := E)
    (Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
        (⇑(quotientEquiv b) :
          (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
      (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))))
have refine_1 : Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
      (⇑(quotientEquiv b) :
        (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
    (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))) ⊆
  fundamentalDomain b ∩ (↑L : Set E)
Tactic: refine Set.Finite.subset this ?_
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ Function.comp (α :=
      HasQuotient.Quotient E (B := Submodule ℤ E)
        (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))))
      (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
      ((⇑(quotientEquiv b) :
          (a :
              HasQuotient.Quotient E (B := Submodule ℤ E)
                (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) →
            (↑(fundamentalDomain b) : Type u_2)) :
        (a :
            HasQuotient.Quotient E (B := Submodule ℤ E)
              (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) →
          (↑(fundamentalDomain b) : Type u_2))
      ((mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))) :
            (a : E) → E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))
          x :
        HasQuotient.Quotient E (B := Submodule ℤ E)
          (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) ∈
    fundamentalDomain b ∩ (↑L : Set E)
have refine_1 : fract b x ∈ fundamentalDomain b ∩ (↑L : Set E)
Tactic: rw [Function.comp_apply, mkQ_apply, quotientEquiv_apply_mk, fractRestrict_apply]
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ fract b x ∈ fundamentalDomain b ∩ (↑L : Set E)
have refine_1 : fract b x ∈ fundamentalDomain b
Tactic: refine ⟨?_, ?_⟩
-- 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
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
refine_1 : fract b x ∈ fundamentalDomain b
⊢ fract b x ∈ fundamentalDomain b ∩ (↑L : Set E)
have refine_1₁ : fract b x ∈ (↑L : Set E)
Tactic: refine ⟨?_, ?_⟩