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

Proof state:
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 : 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
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n => fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i : ↑t, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_neq : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ v ∈ span ℚ (Set.range ⇑e)

Tactic:
apply (smul_mem_iff _ h_nz).mp

Result:
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 : 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
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n => fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i : ↑t, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_neq : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ (-↑n + ↑m) • v ∈ span ℚ (Set.range ⇑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
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n => fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i : ↑t, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i : ↑t, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_neq : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
⊢ -↑n + ↑m ≠ 0

Tactic:
rwa [Ne, add_eq_zero_iff_eq_neg.not, neg_inj, Rat.coe_int_inj, ← Ne]

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
⊢ finrank ℤ ↥L = finrank K E

Tactic:
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)

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
⊢ 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
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
x✝ : ℤ
⊢ fract e (x✝ • v) ∈ ↑L

Tactic:
rw [← h_spanL]

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) = ⊤
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
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
x✝ : ℤ
⊢ fract e (x✝ • v) ∈ ↑(span ℤ (Set.range b))