[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr ↑(floor b m)) i = ↑⌊↑(↑b.repr m) i⌋
[PROOFSTEP]
classical simp only [floor, zsmul_eq_smul_cast K, b.repr.map_smul, Finsupp.single_apply, Finset.sum_apply',
  Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum, Finset.mem_univ, if_true,
  coe_smul_of_tower, Basis.restrictScalars_apply, LinearEquiv.map_sum]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr ↑(floor b m)) i = ↑⌊↑(↑b.repr m) i⌋
[PROOFSTEP]
simp only [floor, zsmul_eq_smul_cast K, b.repr.map_smul, Finsupp.single_apply, Finset.sum_apply', Basis.repr_self,
  Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum, Finset.mem_univ, if_true, coe_smul_of_tower,
  Basis.restrictScalars_apply, LinearEquiv.map_sum]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr ↑(ceil b m)) i = ↑⌈↑(↑b.repr m) i⌉
[PROOFSTEP]
classical simp only [ceil, zsmul_eq_smul_cast K, b.repr.map_smul, Finsupp.single_apply, Finset.sum_apply',
  Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum, Finset.mem_univ, if_true,
  coe_smul_of_tower, Basis.restrictScalars_apply, LinearEquiv.map_sum]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr ↑(ceil b m)) i = ↑⌈↑(↑b.repr m) i⌉
[PROOFSTEP]
simp only [ceil, zsmul_eq_smul_cast K, b.repr.map_smul, Finsupp.single_apply, Finset.sum_apply', Basis.repr_self,
  Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum, Finset.mem_univ, if_true, coe_smul_of_tower,
  Basis.restrictScalars_apply, LinearEquiv.map_sum]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ↑(floor b m) = m
[PROOFSTEP]
apply b.ext_elem
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑(↑b.repr ↑(floor b m)) i = ↑(↑b.repr m) i
[PROOFSTEP]
simp_rw [repr_floor_apply b]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑⌊↑(↑b.repr m) i⌋ = ↑(↑b.repr m) i
[PROOFSTEP]
intro i
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑⌊↑(↑b.repr m) i⌋ = ↑(↑b.repr m) i
[PROOFSTEP]
obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h i
[GOAL]
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌊↑(↑b.repr m) i⌋ = ↑(↑b.repr m) i
[PROOFSTEP]
rw [← hz]
[GOAL]
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌊↑(algebraMap ℤ K) z⌋ = ↑(algebraMap ℤ K) z
[PROOFSTEP]
exact congr_arg (Int.cast : ℤ → K) (Int.floor_intCast z)
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ↑(ceil b m) = m
[PROOFSTEP]
apply b.ext_elem
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑(↑b.repr ↑(ceil b m)) i = ↑(↑b.repr m) i
[PROOFSTEP]
simp_rw [repr_ceil_apply b]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
[PROOFSTEP]
intro i
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
[PROOFSTEP]
obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h i
[GOAL]
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
[PROOFSTEP]
rw [← hz]
[GOAL]
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌈↑(algebraMap ℤ K) z⌉ = ↑(algebraMap ℤ K) z
[PROOFSTEP]
exact congr_arg (Int.cast : ℤ → K) (Int.ceil_intCast z)
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr (fract b m)) i = Int.fract (↑(↑b.repr m) i)
[PROOFSTEP]
rw [fract, LinearEquiv.map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ ↑(↑b.repr (fract b (fract b m))) x✝ = ↑(↑b.repr (fract b m)) x✝
[PROOFSTEP]
classical simp only [repr_fract_apply, Int.fract_fract]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ ↑(↑b.repr (fract b (fract b m))) x✝ = ↑(↑b.repr (fract b m)) x✝
[PROOFSTEP]
simp only [repr_fract_apply, Int.fract_fract]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ↑b)
⊢ fract b (v + m) = fract b m
[PROOFSTEP]
classical
refine (Basis.ext_elem_iff b).mpr fun i => ?_
simp_rw [repr_fract_apply, Int.fract_eq_fract]
use(b.restrictScalars ℤ).repr ⟨v, h⟩ i
rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right, ← eq_intCast (algebraMap ℤ K) _,
  Basis.restrictScalars_repr_apply, coe_mk]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ↑b)
⊢ fract b (v + m) = fract b m
[PROOFSTEP]
refine (Basis.ext_elem_iff b).mpr fun i => ?_
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑(↑b.repr (fract b (v + m))) i = ↑(↑b.repr (fract b m)) i
[PROOFSTEP]
simp_rw [repr_fract_apply, Int.fract_eq_fract]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ∃ z, ↑(↑b.repr (v + m)) i - ↑(↑b.repr m) i = ↑z
[PROOFSTEP]
use(b.restrictScalars ℤ).repr ⟨v, h⟩ i
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑(↑b.repr (v + m)) i - ↑(↑b.repr m) i = ↑(↑(↑(Basis.restrictScalars ℤ b).repr { val := v, property := h }) i)
[PROOFSTEP]
rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right, ← eq_intCast (algebraMap ℤ K) _,
  Basis.restrictScalars_repr_apply, coe_mk]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ↑b)
⊢ fract b (m + v) = fract b m
[PROOFSTEP]
rw [add_comm, fract_zspan_add b m h]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b
[PROOFSTEP]
classical simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self, mem_fundamentalDomain, Set.mem_Ico]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b
[PROOFSTEP]
simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self, mem_fundamentalDomain, Set.mem_Ico]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ↑b)
[PROOFSTEP]
classical
rw [eq_comm, Basis.ext_elem_iff b]
simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem, sub_eq_neg_add, map_add,
  LinearEquiv.map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _,
  Set.mem_range]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ↑b)
[PROOFSTEP]
rw [eq_comm, Basis.ext_elem_iff b]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), ↑(↑b.repr (fract b n)) i = ↑(↑b.repr (fract b m)) i) ↔ -m + n ∈ span ℤ (Set.range ↑b)
[PROOFSTEP]
simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem, sub_eq_neg_add, map_add,
  LinearEquiv.map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _,
  Set.mem_range]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i : ι, ‖↑b i‖
[PROOFSTEP]
classical
calc
  ‖fract b m‖ = ‖∑ i, b.repr (fract b m) i • b i‖ := by rw [b.sum_repr]
  _ = ‖∑ i, Int.fract (b.repr m i) • b i‖ := by simp_rw [repr_fract_apply]
  _ ≤ ∑ i, ‖Int.fract (b.repr m i) • b i‖ := (norm_sum_le _ _)
  _ = ∑ i, ‖Int.fract (b.repr m i)‖ * ‖b i‖ := by simp_rw [norm_smul]
  _ ≤ ∑ i, ‖b i‖ := Finset.sum_le_sum fun i _ => ?_
suffices ‖Int.fract ((b.repr m) i)‖ ≤ 1
  by
  convert mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
  exact (one_mul _).symm
rw [(norm_one.symm : 1 = ‖(1 : K)‖)]
apply norm_le_norm_of_abs_le_abs
rw [abs_one, Int.abs_fract]
exact le_of_lt (Int.fract_lt_one _)
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i : ι, ‖↑b i‖
[PROOFSTEP]
calc
  ‖fract b m‖ = ‖∑ i, b.repr (fract b m) i • b i‖ := by rw [b.sum_repr]
  _ = ‖∑ i, Int.fract (b.repr m i) • b i‖ := by simp_rw [repr_fract_apply]
  _ ≤ ∑ i, ‖Int.fract (b.repr m i) • b i‖ := (norm_sum_le _ _)
  _ = ∑ i, ‖Int.fract (b.repr m i)‖ * ‖b i‖ := by simp_rw [norm_smul]
  _ ≤ ∑ i, ‖b i‖ := Finset.sum_le_sum fun i _ => ?_
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ = ‖∑ i : ι, ↑(↑b.repr (fract b m)) i • ↑b i‖
[PROOFSTEP]
rw [b.sum_repr]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖∑ i : ι, ↑(↑b.repr (fract b m)) i • ↑b i‖ = ‖∑ i : ι, Int.fract (↑(↑b.repr m) i) • ↑b i‖
[PROOFSTEP]
simp_rw [repr_fract_apply]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ∑ i : ι, ‖Int.fract (↑(↑b.repr m) i) • ↑b i‖ = ∑ i : ι, ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖
[PROOFSTEP]
simp_rw [norm_smul]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖ ≤ ‖↑b i‖
[PROOFSTEP]
suffices ‖Int.fract ((b.repr m) i)‖ ≤ 1
  by
  convert mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
  exact (one_mul _).symm
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ * ‖↑b i‖ ≤ ‖↑b i‖
[PROOFSTEP]
convert mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
[GOAL]
case h.e'_4
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
⊢ ‖↑b i‖ = 1 * ‖↑b i‖
[PROOFSTEP]
exact (one_mul _).symm
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ ≤ 1
[PROOFSTEP]
rw [(norm_one.symm : 1 = ‖(1 : K)‖)]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract (↑(↑b.repr m) i)‖ ≤ ‖1‖
[PROOFSTEP]
apply norm_le_norm_of_abs_le_abs
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ |Int.fract (↑(↑b.repr m) i)| ≤ |1|
[PROOFSTEP]
rw [abs_one, Int.abs_fract]
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ Int.fract (↑(↑b.repr m) i) ≤ 1
[PROOFSTEP]
exact le_of_lt (Int.fract_lt_one _)
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ?m.341988 k
⊢ ↑(↑(?m.341992 k).repr ↑(floor (Basis.singleton ι K) k)) x✝ = ↑(↑(?m.341992 k).repr ↑⌊k⌋) x✝
[PROOFSTEP]
rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ?m.344934 k
⊢ ↑(↑(?m.344938 k).repr (fract (Basis.singleton ι K) k)) x✝ = ↑(↑(?m.344938 k).repr (Int.fract k)) x✝
[PROOFSTEP]
rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
⊢ Metric.Bounded (fundamentalDomain b)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ Metric.Bounded (fundamentalDomain b)
[PROOFSTEP]
use 2 * ∑ j, ‖b j‖
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ ∀ (x : E), x ∈ fundamentalDomain b → ∀ (y : E), y ∈ fundamentalDomain b → dist x y ≤ 2 * ∑ j : ι, ‖↑b j‖
[PROOFSTEP]
intro x hx y hy
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ dist x y ≤ 2 * ∑ j : ι, ‖↑b j‖
[PROOFSTEP]
refine le_trans (dist_le_norm_add_norm x y) ?_
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ‖x‖ + ‖y‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
[PROOFSTEP]
rw [← fract_eq_self.mpr hx, ← fract_eq_self.mpr hy]
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ‖fract b x‖ + ‖fract b y‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
[PROOFSTEP]
refine (add_le_add (norm_fract_le b x) (norm_fract_le b y)).trans ?_
[GOAL]
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ∑ i : ι, ‖↑b i‖ + ∑ i : ι, ‖↑b i‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
[PROOFSTEP]
rw [← two_mul]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : { x // x ∈ span ℤ (Set.range ↑b) }
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
[PROOFSTEP]
rw [Subtype.ext_iff, ← add_right_inj x, AddSubgroupClass.coe_neg, ← sub_eq_add_neg, ← fract_apply, ←
  fract_zspan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ← fract_eq_self]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b
[PROOFSTEP]
refine ⟨-floor b x, ?_, fun y h => ?_⟩
[GOAL]
case intro.refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
⊢ (fun v => v +ᵥ x ∈ fundamentalDomain b) (-floor b x)
[PROOFSTEP]
exact (vadd_mem_fundamentalDomain b (-floor b x) x).mpr rfl
[GOAL]
case intro.refine_2
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
val✝ : Fintype ι
y : { x // x ∈ span ℤ (Set.range ↑b) }
h : (fun v => v +ᵥ x ∈ fundamentalDomain b) y
⊢ y = -floor b x
[PROOFSTEP]
exact (vadd_mem_fundamentalDomain b y x).mp h
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
⊢ E ⧸ span ℤ (Set.range ↑b) ≃ ↑(fundamentalDomain b)
[PROOFSTEP]
refine Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩
[GOAL]
case refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
⊢ E ⧸ span ℤ (Set.range ↑b) → ↑(fundamentalDomain b)
[PROOFSTEP]
refine fun q => Quotient.liftOn q (fract_restrict b) (fun _ _ h => ?_)
[GOAL]
case refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
q : E ⧸ span ℤ (Set.range ↑b)
x✝¹ x✝ : E
h : x✝¹ ≈ x✝
⊢ fract_restrict b x✝¹ = fract_restrict b x✝
[PROOFSTEP]
rw [Subtype.mk.injEq, fract_restrict_apply, fract_restrict_apply, fract_eq_fract]
[GOAL]
case refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
q : E ⧸ span ℤ (Set.range ↑b)
x✝¹ x✝ : E
h : x✝¹ ≈ x✝
⊢ -x✝¹ + x✝ ∈ span ℤ (Set.range ↑b)
[PROOFSTEP]
exact QuotientAddGroup.leftRel_apply.mp h
[GOAL]
case refine_2
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x y : E ⧸ span ℤ (Set.range ↑b)
⊢ Quotient.liftOn x (fract_restrict b) (_ : ∀ (x x_1 : E), x ≈ x_1 → fract_restrict b x = fract_restrict b x_1) =
      Quotient.liftOn y (fract_restrict b) (_ : ∀ (x x_1 : E), x ≈ x_1 → fract_restrict b x = fract_restrict b x_1) →
    x = y
[PROOFSTEP]
refine Quotient.inductionOn₂ x y (fun _ _ hxy => ?_)
[GOAL]
case refine_2
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x y : E ⧸ span ℤ (Set.range ↑b)
x✝¹ x✝ : E
hxy :
  Quotient.liftOn (Quotient.mk (quotientRel (span ℤ (Set.range ↑b))) x✝¹) (fract_restrict b)
      (_ : ∀ (x x_1 : E), x ≈ x_1 → fract_restrict b x = fract_restrict b x_1) =
    Quotient.liftOn (Quotient.mk (quotientRel (span ℤ (Set.range ↑b))) x✝) (fract_restrict b)
      (_ : ∀ (x x_1 : E), x ≈ x_1 → fract_restrict b x = fract_restrict b x_1)
⊢ Quotient.mk (quotientRel (span ℤ (Set.range ↑b))) x✝¹ = Quotient.mk (quotientRel (span ℤ (Set.range ↑b))) x✝
[PROOFSTEP]
rw [Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fract_restrict,
  Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fract_restrict, Subtype.mk.injEq] at hxy 
[GOAL]
case refine_2
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x y : E ⧸ span ℤ (Set.range ↑b)
x✝¹ x✝ : E
hxy : fract b x✝¹ = fract b x✝
⊢ Quotient.mk (quotientRel (span ℤ (Set.range ↑b))) x✝¹ = Quotient.mk (quotientRel (span ℤ (Set.range ↑b))) x✝
[PROOFSTEP]
apply Quotient.sound'
[GOAL]
case refine_2.a
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x y : E ⧸ span ℤ (Set.range ↑b)
x✝¹ x✝ : E
hxy : fract b x✝¹ = fract b x✝
⊢ Setoid.r x✝¹ x✝
[PROOFSTEP]
rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← fract_eq_fract]
[GOAL]
case refine_3
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ ∃ a, Quotient.liftOn a (fract_restrict b) (_ : ∀ (x x_1 : E), x ≈ x_1 → fract_restrict b x = fract_restrict b x_1) = x
[PROOFSTEP]
obtain ⟨a, rfl⟩ := fract_restrict_surjective b x
[GOAL]
case refine_3.intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
a : E
⊢ ∃ a_1,
    Quotient.liftOn a_1 (fract_restrict b) (_ : ∀ (x x_1 : E), x ≈ x_1 → fract_restrict b x = fract_restrict b x_1) =
      fract_restrict b a
[PROOFSTEP]
exact ⟨Quotient.mk'' a, rfl⟩
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ ↑(QuotientEquiv b).symm x = Submodule.Quotient.mk ↑x
[PROOFSTEP]
rw [Equiv.symm_apply_eq, quotientEquiv_apply_mk b ↑x, Subtype.ext_iff, fract_restrict_apply]
[GOAL]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ ↑x = fract b ↑x
[PROOFSTEP]
exact (fract_eq_self.mpr x.prop).symm
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
⊢ MeasurableSet (fundamentalDomain b)
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
⊢ MeasurableSet (fundamentalDomain b)
[PROOFSTEP]
let f := (Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toLinearMap.comp b.repr.toLinearMap
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
⊢ MeasurableSet (fundamentalDomain b)
[PROOFSTEP]
let D : Set (ι → ℝ) := Set.pi Set.univ fun _ : ι => Set.Ico (0 : ℝ) 1
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet (fundamentalDomain b)
[PROOFSTEP]
rw [(_ : fundamentalDomain b = f ⁻¹' D)]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet (↑f ⁻¹' D)
[PROOFSTEP]
refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional f).measurable ?_
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet D
[PROOFSTEP]
exact MeasurableSet.pi Set.countable_univ fun _ _ => measurableSet_Ico
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ fundamentalDomain b = ↑f ⁻¹' D
[PROOFSTEP]
ext
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
x✝ : E
⊢ x✝ ∈ fundamentalDomain b ↔ x✝ ∈ ↑f ⁻¹' D
[PROOFSTEP]
simp only [fundamentalDomain, Set.mem_setOf_eq, LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Set.mem_preimage,
  Function.comp_apply, Set.mem_univ_pi, Finsupp.linearEquivFunOnFinite_apply]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
⊢ IsAddFundamentalDomain { x // x ∈ toAddSubgroup (span ℤ (Set.range ↑b)) } (fundamentalDomain b)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
val✝ : Fintype ι
⊢ IsAddFundamentalDomain { x // x ∈ toAddSubgroup (span ℤ (Set.range ↑b)) } (fundamentalDomain b)
[PROOFSTEP]
exact
  IsAddFundamentalDomain.mk' (nullMeasurableSet (fundamentalDomain_measurableSet b)) fun x =>
    exist_unique_vadd_mem_fundamentalDomain b x
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
⊢ AddSubgroup.FG L
[PROOFSTEP]
suffices (AddSubgroup.toIntSubmodule L).FG by exact (fg_iff_add_subgroup_fg _).mp this
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this : Submodule.FG (↑AddSubgroup.toIntSubmodule L)
⊢ AddSubgroup.FG L
[PROOFSTEP]
exact (fg_iff_add_subgroup_fg _).mp this
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
⊢ Submodule.FG (↑AddSubgroup.toIntSubmodule L)
[PROOFSTEP]
obtain ⟨s, ⟨h_incl, ⟨h_span, h_lind⟩⟩⟩ :=
  exists_linearIndependent K
    (L : Set E)
      -- Let `s` be a maximal `K`-linear independent family of elements of `L`. We show that
        -- `L` is finitely generated (as a ℤ-module) because it fits in the exact sequence
        -- `0 → span ℤ s → L → L ⧸ span ℤ s → 0` with `span ℤ s` and `L ⧸ span ℤ s` finitely generated.
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ Submodule.FG (↑AddSubgroup.toIntSubmodule L)
[PROOFSTEP]
refine fg_of_fg_map_of_fg_inf_ker (span ℤ s).mkQ ?_ ?_
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ Submodule.FG (map (mkQ (span ℤ s)) (↑AddSubgroup.toIntSubmodule L))
[PROOFSTEP]
refine fg_def.mpr ⟨map (span ℤ s).mkQ (AddSubgroup.toIntSubmodule L), ?_, span_eq _⟩
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ Set.Finite ↑(map (mkQ (span ℤ s)) (↑AddSubgroup.toIntSubmodule L))
[PROOFSTEP]
let b :=
  Basis.mk h_lind
    (by
      rw [← hs, ← h_span]
      exact span_mono (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl]))
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ ⊤ ≤ span K (Set.range Subtype.val)
[PROOFSTEP]
rw [← hs, ← h_span]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ span K s ≤ span K (Set.range Subtype.val)
[PROOFSTEP]
exact span_mono (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl])
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ s ⊆ Set.range Subtype.val
[PROOFSTEP]
simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl]
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
⊢ Set.Finite ↑(map (mkQ (span ℤ s)) (↑AddSubgroup.toIntSubmodule L))
[PROOFSTEP]
rw [show span ℤ s = span ℤ (Set.range b) by simp [Basis.coe_mk, Subtype.range_coe_subtype]]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
⊢ span ℤ s = span ℤ (Set.range ↑b)
[PROOFSTEP]
simp [Basis.coe_mk, Subtype.range_coe_subtype]
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
⊢ Set.Finite ↑(map (mkQ (span ℤ (Set.range ↑b))) (↑AddSubgroup.toIntSubmodule L))
[PROOFSTEP]
have : Fintype s := Set.Finite.fintype h_lind.finite
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑s
⊢ Set.Finite ↑(map (mkQ (span ℤ (Set.range ↑b))) (↑AddSubgroup.toIntSubmodule L))
[PROOFSTEP]
refine
  Set.Finite.of_finite_image (f := ((↑) : _ → E) ∘ Zspan.QuotientEquiv b) ?_
    (Function.Injective.injOn (Subtype.coe_injective.comp (Zspan.QuotientEquiv b).injective) _)
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑s
⊢ Set.Finite
    (Subtype.val ∘ ↑(Zspan.QuotientEquiv b) '' ↑(map (mkQ (span ℤ (Set.range ↑b))) (↑AddSubgroup.toIntSubmodule L)))
[PROOFSTEP]
have : Set.Finite ((Zspan.fundamentalDomain b) ∩ L) :=
  Metric.Finite_bounded_inter_isClosed (Zspan.fundamentalDomain_bounded b) inferInstance
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
⊢ Set.Finite
    (Subtype.val ∘ ↑(Zspan.QuotientEquiv b) '' ↑(map (mkQ (span ℤ (Set.range ↑b))) (↑AddSubgroup.toIntSubmodule L)))
[PROOFSTEP]
refine Set.Finite.subset this ?_
[GOAL]
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
⊢ Subtype.val ∘ ↑(Zspan.QuotientEquiv b) '' ↑(map (mkQ (span ℤ (Set.range ↑b))) (↑AddSubgroup.toIntSubmodule L)) ⊆
    Zspan.fundamentalDomain b ∩ ↑L
[PROOFSTEP]
rintro _ ⟨_, ⟨⟨x, ⟨h_mem, rfl⟩⟩, rfl⟩⟩
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ (Subtype.val ∘ ↑(Zspan.QuotientEquiv b)) (↑(mkQ (span ℤ (Set.range ↑b))) x) ∈ Zspan.fundamentalDomain b ∩ ↑L
[PROOFSTEP]
rw [Function.comp_apply, mkQ_apply, Zspan.quotientEquiv_apply_mk, Zspan.fract_restrict_apply]
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ Zspan.fract b x ∈ Zspan.fundamentalDomain b ∩ ↑L
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ Zspan.fract b x ∈ Zspan.fundamentalDomain b
[PROOFSTEP]
exact Zspan.fract_mem_fundamentalDomain b x
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ Zspan.fract b x ∈ ↑L
[PROOFSTEP]
rw [Zspan.fract, SetLike.mem_coe, sub_eq_add_neg]
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ x + -↑(Zspan.floor b x) ∈ L
[PROOFSTEP]
refine AddSubgroup.add_mem _ h_mem (neg_mem (Set.mem_of_subset_of_mem ?_ (Subtype.mem (Zspan.floor b x))))
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ ↑(span ℤ (Set.range ↑b)) ⊆ ↑L
[PROOFSTEP]
rw [show (L : Set E) = AddSubgroup.toIntSubmodule L by rfl]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ ↑L = ↑(↑AddSubgroup.toIntSubmodule L)
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ ↑(span ℤ (Set.range ↑b)) ⊆ ↑(↑AddSubgroup.toIntSubmodule L)
[PROOFSTEP]
rw [SetLike.coe_subset_coe, Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq]
[GOAL]
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑s
this : Set.Finite (Zspan.fundamentalDomain b ∩ ↑L)
x : E
h_mem : x ∈ ↑(↑AddSubgroup.toIntSubmodule L)
⊢ span ℤ s ≤ ↑AddSubgroup.toIntSubmodule L
[PROOFSTEP]
exact span_le.mpr h_incl
[GOAL]
case intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ Submodule.FG (↑AddSubgroup.toIntSubmodule L ⊓ LinearMap.ker (mkQ (span ℤ s)))
[PROOFSTEP]
rw [ker_mkQ, inf_of_le_right (span_le.mpr h_incl)]
[GOAL]
case intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ Submodule.FG (span ℤ s)
[PROOFSTEP]
exact fg_span (LinearIndependent.finite h_lind)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
⊢ Module.Free ℤ { x // x ∈ L }
[PROOFSTEP]
have : Module.Finite ℤ L := module_finite K hs
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this : Module.Finite ℤ { x // x ∈ L }
⊢ Module.Free ℤ { x // x ∈ L }
[PROOFSTEP]
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝ : Module.Finite ℤ { x // x ∈ L }
this : Module ℚ E
⊢ Module.Free ℤ { x // x ∈ L }
[PROOFSTEP]
have : NoZeroSMulDivisors ℤ E := RatModule.noZeroSMulDivisors
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝¹ : Module.Finite ℤ { x // x ∈ L }
this✝ : Module ℚ E
this : NoZeroSMulDivisors ℤ E
⊢ Module.Free ℤ { x // x ∈ L }
[PROOFSTEP]
have : NoZeroSMulDivisors ℤ L :=
  by
  change NoZeroSMulDivisors ℤ (AddSubgroup.toIntSubmodule L)
  exact noZeroSMulDivisors _
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝¹ : Module.Finite ℤ { x // x ∈ L }
this✝ : Module ℚ E
this : NoZeroSMulDivisors ℤ E
⊢ NoZeroSMulDivisors ℤ { x // x ∈ L }
[PROOFSTEP]
change NoZeroSMulDivisors ℤ (AddSubgroup.toIntSubmodule L)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝¹ : Module.Finite ℤ { x // x ∈ L }
this✝ : Module ℚ E
this : NoZeroSMulDivisors ℤ E
⊢ NoZeroSMulDivisors ℤ { x // x ∈ ↑AddSubgroup.toIntSubmodule L }
[PROOFSTEP]
exact noZeroSMulDivisors _
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
this✝ : NoZeroSMulDivisors ℤ E
this : NoZeroSMulDivisors ℤ { x // x ∈ L }
⊢ Module.Free ℤ { x // x ∈ L }
[PROOFSTEP]
exact Module.free_of_finite_type_torsion_free'
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
classical
have : Module.Finite ℤ L := module_finite K hs
have : Module.Free ℤ L := module_free K hs
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
let b₀ := Module.Free.chooseBasis ℤ L
let b := Subtype.val ∘ b₀
have : LinearIndependent ℤ b :=
  LinearIndependent.map' b₀.linearIndependent (L.toIntSubmodule.subtype)
    (ker_subtype _)
      -- We prove some assertions that will be useful later on
have h_spanL : span ℤ (Set.range b) = AddSubgroup.toIntSubmodule L :=
  by
  convert congrArg (map (Submodule.subtype (AddSubgroup.toIntSubmodule L))) b₀.span_eq
  · rw [map_span, Set.range_comp]
    rfl
  · exact (map_subtype_top _).symm
have h_spanE : span K (Set.range b) = ⊤ := by rwa [← span_span_of_tower (R := ℤ), h_spanL]
have h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ L) = (Set.range b).toFinset.card :=
  by
  rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
  rfl
  exact Subtype.coe_injective.comp (Basis.injective _)
rw [finrank_eq_card_chooseBasisIndex]
  -- We prove that `finrank ℤ L ≤ finrank K E` and `finrank K E ≤ finrank ℤ L`
refine le_antisymm ?_ ?_
·
  -- To prove that `finrank ℤ L ≤ finrank K E`, we proceed by contradiction and prove that, in
      -- this case, there is a ℤ-relation between the vectors of `b`
  obtain ⟨t, ⟨ht_inc, ⟨ht_span, ht_lin⟩⟩⟩ :=
    exists_linearIndependent K
      (Set.range b)
        -- `e` is a `K`-basis of `E` formed of vectors of `b`
  let e : Basis t K E := Basis.mk ht_lin (by simp [ht_span, h_spanE])
  have : Fintype t := Set.Finite.fintype ((Set.range b).toFinite.subset ht_inc)
  have h : LinearIndependent ℤ (fun x : (Set.range b) => (x : E)) := by
    rwa [linearIndependent_subtype_range (Subtype.coe_injective.comp b₀.injective)]
  contrapose! h
  obtain ⟨v, hv⟩ : (Set.range b \ Set.range e).Nonempty :=
    by
    rw [Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq, ← Set.toFinset_nonempty]
    contrapose h
    rw [Finset.not_nonempty_iff_eq_empty, Set.toFinset_diff, Finset.sdiff_eq_empty_iff_subset] at h 
    replace h := Finset.card_le_of_subset h
    rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span, finrank_span_set_eq_card _ ht_lin]
      -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
  suffices ¬LinearIndependent ℤ (fun x : ↥(insert v (Set.range e)) => (x : E))
    by
    contrapose! this
    refine LinearIndependent.mono ?_ this
    exact
      Set.insert_subset (Set.mem_of_mem_diff hv)
        (by simp [ht_inc])
          -- We prove finally that `e ∪ {v}` is not ℤ-linear independent or, equivalently,
              -- not ℚ-linear independent by showing that `v ∈ span ℚ e`.
  rw [LinearIndependent.iff_fractionRing ℤ ℚ, (linearIndependent_insert (Set.not_mem_of_mem_diff hv)), not_and, not_not]
  intro
    _
      -- But that follows from the fact that there exist `n, m : ℕ`, `n ≠ m`
          -- such that `(n - m) • v ∈ span ℤ e` which is true since `n ↦ Zspan.fract e (n • v)`
          -- takes value into the finite set `fundamentalDomain e ∩ L`
  have h_mapsto :
    Set.MapsTo (fun n : ℤ => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) :=
    by
    rw [Set.mapsTo_inter, Set.maps_univ_to, Set.maps_univ_to]
    refine ⟨fun _ => mem_closedBall_zero_iff.mpr (Zspan.norm_fract_le e _), fun _ => ?_⟩
    · change _ ∈ AddSubgroup.toIntSubmodule L
      rw [← h_spanL]
      refine sub_mem ?_ ?_
      · exact zsmul_mem (subset_span (Set.diff_subset _ _ hv)) _
      · exact span_mono (by simp [ht_inc]) (coe_mem _)
  have h_finite : Set.Finite (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) :=
    Metric.Finite_bounded_inter_isClosed Metric.bounded_closedBall inferInstance
  obtain ⟨n, -, m, -, h_neq, h_eq⟩ := Set.Infinite.exists_ne_map_eq_of_mapsTo Set.infinite_univ h_mapsto h_finite
  have h_nz : (-n + m : ℚ) ≠ 0 := by rwa [Ne.def, add_eq_zero_iff_eq_neg.not, neg_inj, Rat.coe_int_inj, ← Ne.def]
  apply (smul_mem_iff _ h_nz).mp
  refine span_subset_span ℤ ℚ _ ?_
  rwa [add_smul, neg_smul, SetLike.mem_coe, ← Zspan.fract_eq_fract, ← zsmul_eq_smul_cast ℚ, ← zsmul_eq_smul_cast ℚ]
·
  -- To prove that `finrank K E ≤ finrank ℤ L`, we use the fact `b` generates `E` over `K`
      -- and thus `finrank K E ≤ card b = finrank ℤ L`
  rw [← topEquiv.finrank_eq, ← h_spanE]
  convert finrank_span_le_card (K := K) (Set.range b)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have : Module.Finite ℤ L := module_finite K hs
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this : Module.Finite ℤ { x // x ∈ L }
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have : Module.Free ℤ L := module_free K hs
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝ : Module.Finite ℤ { x // x ∈ L }
this : Module.Free ℤ { x // x ∈ L }
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝¹ : Module.Finite ℤ { x // x ∈ L }
this✝ : Module.Free ℤ { x // x ∈ L }
this : Module ℚ E
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
let b₀ := Module.Free.chooseBasis ℤ L
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝¹ : Module.Finite ℤ { x // x ∈ L }
this✝ : Module.Free ℤ { x // x ∈ L }
this : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
let b := Subtype.val ∘ b₀
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝¹ : Module.Finite ℤ { x // x ∈ L }
this✝ : Module.Free ℤ { x // x ∈ L }
this : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have : LinearIndependent ℤ b :=
  LinearIndependent.map' b₀.linearIndependent (L.toIntSubmodule.subtype)
    (ker_subtype _)
      -- We prove some assertions that will be useful later on
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have h_spanL : span ℤ (Set.range b) = AddSubgroup.toIntSubmodule L :=
  by
  convert congrArg (map (Submodule.subtype (AddSubgroup.toIntSubmodule L))) b₀.span_eq
  · rw [map_span, Set.range_comp]
    rfl
  · exact (map_subtype_top _).symm
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
⊢ span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
[PROOFSTEP]
convert congrArg (map (Submodule.subtype (AddSubgroup.toIntSubmodule L))) b₀.span_eq
[GOAL]
case h.e'_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
⊢ span ℤ (Set.range b) = map (Submodule.subtype (↑AddSubgroup.toIntSubmodule L)) (span ℤ (Set.range ↑b₀))
[PROOFSTEP]
rw [map_span, Set.range_comp]
[GOAL]
case h.e'_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
⊢ span ℤ (Subtype.val '' Set.range ↑b₀) = span ℤ (↑(Submodule.subtype (↑AddSubgroup.toIntSubmodule L)) '' Set.range ↑b₀)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
⊢ ↑AddSubgroup.toIntSubmodule L = map (Submodule.subtype (↑AddSubgroup.toIntSubmodule L)) ⊤
[PROOFSTEP]
exact (map_subtype_top _).symm
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have h_spanE : span K (Set.range b) = ⊤ := by rwa [← span_span_of_tower (R := ℤ), h_spanL]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
⊢ span K (Set.range b) = ⊤
[PROOFSTEP]
rwa [← span_span_of_tower (R := ℤ), h_spanL]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
have h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ L) = (Set.range b).toFinset.card :=
  by
  rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
  rfl
  exact Subtype.coe_injective.comp (Basis.injective _)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
[PROOFSTEP]
rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card Finset.univ
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
⊢ Function.Injective b
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
⊢ Function.Injective b
[PROOFSTEP]
exact Subtype.coe_injective.comp (Basis.injective _)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
⊢ finrank ℤ { x // x ∈ L } = finrank K E
[PROOFSTEP]
rw [finrank_eq_card_chooseBasisIndex]
  -- We prove that `finrank ℤ L ≤ finrank K E` and `finrank K E ≤ finrank ℤ L`
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = finrank K E
[PROOFSTEP]
refine le_antisymm ?_ ?_
[GOAL]
case refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ≤ finrank K E
[PROOFSTEP]
obtain ⟨t, ⟨ht_inc, ⟨ht_span, ht_lin⟩⟩⟩ :=
  exists_linearIndependent K
    (Set.range b)
      -- `e` is a `K`-basis of `E` formed of vectors of `b`
[GOAL]
case refine_1.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ≤ finrank K E
[PROOFSTEP]
let e : Basis t K E := Basis.mk ht_lin (by simp [ht_span, h_spanE])
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
⊢ ⊤ ≤ span K (Set.range Subtype.val)
[PROOFSTEP]
simp [ht_span, h_spanE]
[GOAL]
case refine_1.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ≤ finrank K E
[PROOFSTEP]
have : Fintype t := Set.Finite.fintype ((Set.range b).toFinite.subset ht_inc)
[GOAL]
case refine_1.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ≤ finrank K E
[PROOFSTEP]
have h : LinearIndependent ℤ (fun x : (Set.range b) => (x : E)) := by
  rwa [linearIndependent_subtype_range (Subtype.coe_injective.comp b₀.injective)]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
⊢ LinearIndependent ℤ fun x => ↑x
[PROOFSTEP]
rwa [linearIndependent_subtype_range (Subtype.coe_injective.comp b₀.injective)]
[GOAL]
case refine_1.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : LinearIndependent ℤ fun x => ↑x
⊢ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ≤ finrank K E
[PROOFSTEP]
contrapose! h
[GOAL]
case refine_1.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
⊢ ¬LinearIndependent ℤ fun x => ↑x
[PROOFSTEP]
obtain ⟨v, hv⟩ : (Set.range b \ Set.range e).Nonempty :=
  by
  rw [Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq, ← Set.toFinset_nonempty]
  contrapose h
  rw [Finset.not_nonempty_iff_eq_empty, Set.toFinset_diff, Finset.sdiff_eq_empty_iff_subset] at h 
  replace h := Finset.card_le_of_subset h
  rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span, finrank_span_set_eq_card _ ht_lin]
    -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
⊢ Set.Nonempty (Set.range b \ Set.range ↑e)
[PROOFSTEP]
rw [Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq, ← Set.toFinset_nonempty]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
⊢ Finset.Nonempty (Set.toFinset (Set.range b \ t))
[PROOFSTEP]
contrapose h
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : ¬Finset.Nonempty (Set.toFinset (Set.range b \ t))
⊢ ¬finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
[PROOFSTEP]
rw [Finset.not_nonempty_iff_eq_empty, Set.toFinset_diff, Finset.sdiff_eq_empty_iff_subset] at h 
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : Set.toFinset (Set.range b) ⊆ Set.toFinset t
⊢ ¬finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
[PROOFSTEP]
replace h := Finset.card_le_of_subset h
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : Finset.card (Set.toFinset (Set.range b)) ≤ Finset.card (Set.toFinset t)
⊢ ¬finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
[PROOFSTEP]
rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span, finrank_span_set_eq_card _ ht_lin]
  -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
[GOAL]
case refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
⊢ ¬LinearIndependent ℤ fun x => ↑x
[PROOFSTEP]
suffices ¬LinearIndependent ℤ (fun x : ↥(insert v (Set.range e)) => (x : E))
  by
  contrapose! this
  refine LinearIndependent.mono ?_ this
  exact
    Set.insert_subset (Set.mem_of_mem_diff hv)
      (by simp [ht_inc])
        -- We prove finally that `e ∪ {v}` is not ℤ-linear independent or, equivalently,
            -- not ℚ-linear independent by showing that `v ∈ span ℚ e`.
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝⁴ : Module.Finite ℤ { x // x ∈ L }
this✝³ : Module.Free ℤ { x // x ∈ L }
this✝² : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝¹ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
this : ¬LinearIndependent ℤ fun x => ↑x
⊢ ¬LinearIndependent ℤ fun x => ↑x
[PROOFSTEP]
contrapose! this
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝⁴ : Module.Finite ℤ { x // x ∈ L }
this✝³ : Module.Free ℤ { x // x ∈ L }
this✝² : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝¹ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
this : LinearIndependent ℤ fun x => ↑x
⊢ LinearIndependent ℤ fun x => ↑x
[PROOFSTEP]
refine LinearIndependent.mono ?_ this
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝⁴ : Module.Finite ℤ { x // x ∈ L }
this✝³ : Module.Free ℤ { x // x ∈ L }
this✝² : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝¹ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
this : LinearIndependent ℤ fun x => ↑x
⊢ insert v (Set.range ↑(Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val)))) ⊆
    Set.range (Subtype.val ∘ ↑(Module.Free.chooseBasis ℤ { x // x ∈ L }))
[PROOFSTEP]
exact
  Set.insert_subset (Set.mem_of_mem_diff hv)
    (by simp [ht_inc])
      -- We prove finally that `e ∪ {v}` is not ℤ-linear independent or, equivalently,
          -- not ℚ-linear independent by showing that `v ∈ span ℚ e`.
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝⁴ : Module.Finite ℤ { x // x ∈ L }
this✝³ : Module.Free ℤ { x // x ∈ L }
this✝² : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝¹ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this✝ : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
this : LinearIndependent ℤ fun x => ↑x
⊢ Set.range ↑(Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))) ⊆
    Set.range (Subtype.val ∘ ↑(Module.Free.chooseBasis ℤ { x // x ∈ L }))
[PROOFSTEP]
simp [ht_inc]
[GOAL]
case refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
⊢ ¬LinearIndependent ℤ fun x => ↑x
[PROOFSTEP]
rw [LinearIndependent.iff_fractionRing ℤ ℚ, (linearIndependent_insert (Set.not_mem_of_mem_diff hv)), not_and, not_not]
[GOAL]
case refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
⊢ (LinearIndependent ℚ fun b => ↑b) → v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
intro
  _
    -- But that follows from the fact that there exist `n, m : ℕ`, `n ≠ m`
        -- such that `(n - m) • v ∈ span ℤ e` which is true since `n ↦ Zspan.fract e (n • v)`
        -- takes value into the finite set `fundamentalDomain e ∩ L`
[GOAL]
case refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
⊢ v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
have h_mapsto :
  Set.MapsTo (fun n : ℤ => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) :=
  by
  rw [Set.mapsTo_inter, Set.maps_univ_to, Set.maps_univ_to]
  refine ⟨fun _ => mem_closedBall_zero_iff.mpr (Zspan.norm_fract_le e _), fun _ => ?_⟩
  · change _ ∈ AddSubgroup.toIntSubmodule L
    rw [← h_spanL]
    refine sub_mem ?_ ?_
    · exact zsmul_mem (subset_span (Set.diff_subset _ _ hv)) _
    · exact span_mono (by simp [ht_inc]) (coe_mem _)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
⊢ Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
[PROOFSTEP]
rw [Set.mapsTo_inter, Set.maps_univ_to, Set.maps_univ_to]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
⊢ (∀ (a : ℤ), Zspan.fract e (a • v) ∈ Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖)) ∧ ∀ (a : ℤ), Zspan.fract e (a • v) ∈ ↑L
[PROOFSTEP]
refine ⟨fun _ => mem_closedBall_zero_iff.mpr (Zspan.norm_fract_le e _), fun _ => ?_⟩
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
x✝ : ℤ
⊢ Zspan.fract e (x✝ • v) ∈ ↑L
[PROOFSTEP]
change _ ∈ AddSubgroup.toIntSubmodule L
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
x✝ : ℤ
⊢ Zspan.fract e (x✝ • v) ∈ ↑AddSubgroup.toIntSubmodule L
[PROOFSTEP]
rw [← h_spanL]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
x✝ : ℤ
⊢ Zspan.fract e (x✝ • v) ∈ span ℤ (Set.range b)
[PROOFSTEP]
refine sub_mem ?_ ?_
[GOAL]
case refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
x✝ : ℤ
⊢ x✝ • v ∈ span ℤ (Set.range b)
[PROOFSTEP]
exact zsmul_mem (subset_span (Set.diff_subset _ _ hv)) _
[GOAL]
case refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
x✝ : ℤ
⊢ ↑(Zspan.floor e (x✝ • v)) ∈ span ℤ (Set.range b)
[PROOFSTEP]
exact span_mono (by simp [ht_inc]) (coe_mem _)
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
x✝ : ℤ
⊢ Set.range ↑e ⊆ Set.range b
[PROOFSTEP]
simp [ht_inc]
[GOAL]
case refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
⊢ v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
have h_finite : Set.Finite (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) :=
  Metric.Finite_bounded_inter_isClosed Metric.bounded_closedBall inferInstance
[GOAL]
case refine_1.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
h_finite : Set.Finite (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
⊢ v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
obtain ⟨n, -, m, -, h_neq, h_eq⟩ := Set.Infinite.exists_ne_map_eq_of_mapsTo Set.infinite_univ h_mapsto h_finite
[GOAL]
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
h_finite : Set.Finite (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
n m : ℤ
h_neq : n ≠ m
h_eq : Zspan.fract e (n • v) = Zspan.fract e (m • v)
⊢ v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
have h_nz : (-n + m : ℚ) ≠ 0 := by rwa [Ne.def, add_eq_zero_iff_eq_neg.not, neg_inj, Rat.coe_int_inj, ← Ne.def]
[GOAL]
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
h_finite : Set.Finite (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
n m : ℤ
h_neq : n ≠ m
h_eq : Zspan.fract e (n • v) = Zspan.fract e (m • v)
⊢ -↑n + ↑m ≠ 0
[PROOFSTEP]
rwa [Ne.def, add_eq_zero_iff_eq_neg.not, neg_inj, Rat.coe_int_inj, ← Ne.def]
[GOAL]
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
h_finite : Set.Finite (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
n m : ℤ
h_neq : n ≠ m
h_eq : Zspan.fract e (n • v) = Zspan.fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
apply (smul_mem_iff _ h_nz).mp
[GOAL]
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
h_finite : Set.Finite (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
n m : ℤ
h_neq : n ≠ m
h_eq : Zspan.fract e (n • v) = Zspan.fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ (-↑n + ↑m) • v ∈ span ℚ (Set.range ↑e)
[PROOFSTEP]
refine span_subset_span ℤ ℚ _ ?_
[GOAL]
case refine_1.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝³ : Module.Finite ℤ { x // x ∈ L }
this✝² : Module.Free ℤ { x // x ∈ L }
this✝¹ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin (_ : ⊤ ≤ span K (Set.range Subtype.val))
this : Fintype ↑t
h : finrank K E < Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
v : E
hv : v ∈ Set.range b \ Set.range ↑e
a✝ : LinearIndependent ℚ fun b => ↑b
h_mapsto : Set.MapsTo (fun n => Zspan.fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
h_finite : Set.Finite (Metric.closedBall 0 (∑ i : ↑t, ‖↑e i‖) ∩ ↑L)
n m : ℤ
h_neq : n ≠ m
h_eq : Zspan.fract e (n • v) = Zspan.fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ (-↑n + ↑m) • v ∈ ↑(span ℤ (Set.range ↑e))
[PROOFSTEP]
rwa [add_smul, neg_smul, SetLike.mem_coe, ← Zspan.fract_eq_fract, ← zsmul_eq_smul_cast ℚ, ← zsmul_eq_smul_cast ℚ]
[GOAL]
case refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
⊢ finrank K E ≤ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
[PROOFSTEP]
rw [← topEquiv.finrank_eq, ← h_spanE]
[GOAL]
case refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : AddSubgroup E
inst✝ : DiscreteTopology { x // x ∈ L }
hs : span K ↑L = ⊤
this✝² : Module.Finite ℤ { x // x ∈ L }
this✝¹ : Module.Free ℤ { x // x ∈ L }
this✝ : Module ℚ E
b₀ : Basis (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) ℤ { x // x ∈ L } := Module.Free.chooseBasis ℤ { x // x ∈ L }
b : Module.Free.ChooseBasisIndex ℤ { x // x ∈ L } → E := Subtype.val ∘ ↑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = ↑AddSubgroup.toIntSubmodule L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L }) = Finset.card (Set.toFinset (Set.range b))
⊢ finrank K { x // x ∈ span K (Set.range b) } ≤ Fintype.card (Module.Free.ChooseBasisIndex ℤ { x // x ∈ L })
[PROOFSTEP]
convert finrank_span_le_card (K := K) (Set.range b)
