-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem ZLattice.rank [hs : IsZLattice K L] : finrank ℤ L = finrank K E

Proof state:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Free ℤ ↥L
this✝ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
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)

Tactic:
simp [ht_span, h_spanE]

Result:
no goals

Proof state:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Free ℤ ↥L
this✝¹ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
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 ⋯
this : Fintype ↑t
⊢ LinearIndepOn ℤ id (Set.range b)

Tactic:
rwa [linearIndepOn_id_range_iff (Subtype.coe_injective.comp b₀.injective)]

Result:
no goals

Proof state:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Free ℤ ↥L
this✝ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
⊢ finrank K E ≤ Fintype.card (Free.ChooseBasisIndex ℤ ↥L)

Tactic:
rw [← topEquiv.finrank_eq, ← h_spanE]

Result:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Free ℤ ↥L
this✝ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
⊢ finrank K ↥(span K (Set.range b)) ≤ Fintype.card (Free.ChooseBasisIndex ℤ ↥L)

Proof state:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝¹ : Module.Finite ℤ ↥L
this✝ : Free ℤ ↥L
this : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
⊢ finrank ℤ ↥L = finrank K E

Tactic:
have : LinearIndependent ℤ b :=
  LinearIndependent.map' b₀.linearIndependent (L.subtype) (ker_subtype _)

Result:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Free ℤ ↥L
this✝ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
⊢ finrank ℤ ↥L = finrank K E

Proof state:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Free ℤ ↥L
this✝ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
⊢ finrank ℤ ↥L = finrank K E

Tactic:
have h_spanE : span K (Set.range b) = ⊤ := by
  rw [← span_span_of_tower (R := ℤ), h_spanL]
  exact hs.span_top

Result:
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 : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Free ℤ ↥L
this✝ : Module ℚ E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
⊢ finrank ℤ ↥L = finrank K E