-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
have have₁ have₂ : ∀ (this : Module.Finite.{0, u_2} ℤ ↥L), finrank.{0, u_2} ℤ ↥L = finrank K E
have₃ : ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this : Module ℚ E), finrank.{0, u_2} ℤ ↥L = finrank K E
have₄ have₅ have₆ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this : Module ℚ E) (this : IsAddTorsionFree E),
    finrank.{0, u_2} ℤ ↥L = finrank K E
have₇ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this : LinearIndependent ℤ b), finrank.{0, u_2} ℤ ↥L = finrank K E
have₈ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this_3 : LinearIndependent ℤ b) (h_spanL : span ℤ (Set.range b) = L), finrank.{0, u_2} ℤ ↥L = finrank K E
have₉ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this_3 : LinearIndependent ℤ b) (h_spanL : span ℤ (Set.range b) = L)
      (h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤), finrank.{0, u_2} ℤ ↥L = finrank K E
have₁₀ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this_3 : LinearIndependent ℤ b) (h_spanL : span ℤ (Set.range b) = L)
      (h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤)
      (h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card),
      finrank.{0, u_2} ℤ ↥L = finrank K E
have₁₁ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this_3 : LinearIndependent ℤ b) (h_spanL : span ℤ (Set.range b) = L)
      (h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤)
      (h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card),
      Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
refine_1 :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this_3 : LinearIndependent ℤ b) (h_spanL : span ℤ (Set.range b) = L)
      (h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤)
      (h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card),
      Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E
refine_2 refine_2₁ :
  ∀ (this : Module.Finite.{0, u_2} ℤ ↥L) (this_1 : Module ℚ E) (this_2 : IsAddTorsionFree E),
    let b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L;
    let b : Free.ChooseBasisIndex ℤ ↥L → E :=
      Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L);
    ∀ (this_3 : LinearIndependent ℤ b) (h_spanL : span ℤ (Set.range b) = L)
      (h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤)
      (h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card),
      finrank K E ≤ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E

Tactic:
classical
  have : Module.Finite ℤ L := module_finite K L
  have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
  have : IsAddTorsionFree E := .of_module_rat _
  let b₀ := Module.Free.chooseBasis ℤ L
  -- Let `b` be a `ℤ`-basis of `L` formed of vectors of `E`
  let b := Subtype.val ∘ b₀
  have : LinearIndependent ℤ b :=
    LinearIndependent.map' b₀.linearIndependent (L.subtype) (ker_subtype _)
  -- We prove some assertions that will be useful later on
  have h_spanL : span ℤ (Set.range b) = L := by
    convert! congrArg (map (Submodule.subtype 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
    rw [← span_span_of_tower (R := ℤ), h_spanL]
    exact hs.span_top
  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 : LinearIndepOn ℤ id (Set.range b) := by
      rwa [linearIndepOn_id_range_iff (Subtype.coe_injective.comp b₀.injective)]
    contrapose! h
    -- Since `finrank ℤ L > finrank K E`, there exists a vector `v ∈ b` with `v ∉ e`
    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 [Set.toFinset_diff, Finset.sdiff_eq_empty_iff_subset] at h
      replace h := Finset.card_le_card h
      rwa [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 ¬ LinearIndepOn ℤ id (insert v (Set.range e)) by
      contrapose this
      refine this.mono ?_
      exact Set.insert_subset (Set.mem_of_mem_diff hv) (by simp [e, ht_inc])
    -- We prove finally that `e ∪ {v}` is not ℤ-linear independent or, equivalently,
    -- not ℚ-linear independent by showing that `v ∈ span ℚ e`.
    rw [LinearIndepOn, LinearIndependent.iff_fractionRing ℤ ℚ, ← LinearIndepOn,
      linearIndepOn_id_insert (Set.notMem_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 : ℤ => fract e (n • v)) Set.univ
        (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) := by
      rw [Set.mapsTo_inter, Set.mapsTo_univ_iff, Set.mapsTo_univ_iff]
      refine ⟨fun _ ↦ mem_closedBall_zero_iff.mpr (norm_fract_le e _), fun _ => ?_⟩
      · rw [← h_spanL]
        refine sub_mem ?_ ?_
        · exact zsmul_mem (subset_span (Set.diff_subset hv)) _
        · exact span_mono (by simp [e, ht_inc]) (coe_mem _)
    have h_finite : Set.Finite (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) := by
      change ((_ : Set E) ∩ L.toAddSubgroup).Finite
      have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
      exact Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
        Metric.isBounded_closedBall inferInstance
    obtain ⟨n, -, m, -, h_ne, 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, add_eq_zero_iff_eq_neg.not, neg_inj, Rat.coe_int_inj, ← Ne]
    apply (smul_mem_iff _ h_nz).mp
    refine span_subset_span ℤ ℚ _ ?_
    rwa [add_smul, neg_smul, SetLike.mem_coe, ← fract_eq_fract, Int.cast_smul_eq_zsmul ℚ,
      Int.cast_smul_eq_zsmul ℚ]
  · -- 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 (R := K) (Set.range b)

Premises used: Submodule.span_subset_span, neg_smul, Submodule.topEquiv, Classical.not_not, Rat, LinearEquiv.finrank_eq, Int, LinearIndependent.iff_fractionRing, le_antisymm, Module.finrank_eq_card_chooseBasisIndex, add_smul, SetLike.mem_coe, not_and, ZSpan.fract_eq_fract, Int.cast_smul_eq_zsmul, LinearIndepOn