awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
⊢ (∀ (x : ℤ),
      Membership.mem (γ := Set E)
        (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)))
        (fract e (x • v))) ∧
    ∀ (x : ℤ), fract e (x • v) ∈ (↑L : Set E)

Tactic:
⟨fun _ ↦ mem_closedBall_zero_iff.mpr (norm_fract_le e _), fun _ => ?_⟩

Premises used: Iff.mpr, ZSpan.norm_fract_le, And.intro, HSMul.hSMul, mem_closedBall_zero_iff
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
refine : ∀ (x : ℤ), fract e (x • v) ∈ (↑L : Set E)
⊢ (∀ (x : ℤ),
      Membership.mem (γ := Set E)
        (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)))
        (fract e (x • v))) ∧
    ∀ (x : ℤ), fract e (x • v) ∈ (↑L : Set E)

Tactic:
refine ⟨fun _ ↦ mem_closedBall_zero_iff.mpr (norm_fract_le e _), fun _ => ?_⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
rw : fract e (x • v) ∈ (↑(span ℤ (Set.range b)) : Set E)
⊢ fract e (x • v) ∈ (↑L : Set E)

Tactic:
rw [← h_spanL]
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
⊢ fract e (x • v) ∈ (↑(span ℤ (Set.range b)) : Set E)

Tactic:
sub_mem ?_ ?_

Premises used: Set.Mem, sub_mem, ZSpan.fract
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
refine_1 : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range b)) (x • v)
refine_2 : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range b)) (↑(floor e (x • v)) : E)
⊢ fract e (x • v) ∈ (↑(span ℤ (Set.range b)) : Set E)

Tactic:
refine sub_mem ?_ ?_

Premises used: sub_mem
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
⊢ Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range b)) (x • v)

Tactic:
zsmul_mem (subset_span (Set.diff_subset hv)) _

Premises used: Set.diff_subset, zsmul_mem, Submodule.subset_span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
⊢ Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range b)) (x • v)

Tactic:
exact zsmul_mem (subset_span (Set.diff_subset hv)) _

Premises used: Set.diff_subset, zsmul_mem, Submodule.subset_span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
⊢ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E) ⊆ Set.range b

Tactic:
simp [e, ht_inc]
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
x : ℤ
⊢ Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range b)) (↑(floor e (x • v)) : E)

Tactic:
exact span_mono (by simp [e, ht_inc]) (coe_mem _)

Premises used: Submodule.coe_mem, Submodule.span_mono
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
⊢ Set.MapsTo (fun (n : ℤ) ↦ fract e (n • v)) Set.univ
    (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩ (↑L : Set E))

Tactic:
have h_mapsto : Set.MapsTo (fun n : ℤ => fract e (n • v)) Set.univ
        (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) := by
      rw [Set.mapsTo_inter, Set.mapsTo_univ_iff, Set.mapsTo_univ_iff]
      refine ⟨fun _ ↦ mem_closedBall_zero_iff.mpr (norm_fract_le e _), fun _ => ?_⟩
      · rw [← h_spanL]
        refine sub_mem ?_ ?_
        · exact zsmul_mem (subset_span (Set.diff_subset hv)) _
        · exact span_mono (by simp [e, ht_inc]) (coe_mem _)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
h_mapsto :
  Set.MapsTo (fun (n : ℤ) ↦ fract e (n • v)) Set.univ
    (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩ (↑L : Set E))
change :
  (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩
      (↑L.toAddSubgroup : Set E)).Finite
⊢ (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩
      (↑L : Set E)).Finite

Tactic:
change ((_ : Set E) ∩ L.toAddSubgroup).Finite

Premises used: Set.Finite, Inter.inter, SetLike.coe, Submodule.toAddSubgroup
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
h_mapsto :
  Set.MapsTo (fun (n : ℤ) ↦ fract e (n • v)) Set.univ
    (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩ (↑L : Set E))
⊢ DiscreteTopology.{u_2} ↥L.toAddSubgroup

Tactic:
have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this_5 : Fintype (↑t : Type u_2)
h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
h_mapsto :
  Set.MapsTo (fun (n : ℤ) ↦ fract e (n • v)) Set.univ
    (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩ (↑L : Set E))
this : DiscreteTopology.{u_2} ↥L.toAddSubgroup
⊢ (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩
      (↑L.toAddSubgroup : Set E)).Finite

Tactic:
Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
        Metric.isBounded_closedBall inferInstance

Premises used: Metric.isBounded_closedBall, DiscreteTopology.isDiscrete, inferInstance, Metric.finite_isBounded_inter_isClosed