awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
⊢ L = Submodule.map L.subtype ⊤

Tactic:
(map_subtype_top _).symm

Premises used: Set.Mem, Submodule.map_subtype_top, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
⊢ L = Submodule.map L.subtype ⊤

Tactic:
exact (map_subtype_top _).symm

Premises used: Submodule.map_subtype_top, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
⊢ span ℤ (Set.range b) = L

Tactic:
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
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
rw : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
⊢ Eq (α := Submodule K E) (span K (Set.range b)) ⊤

Tactic:
rw [← span_span_of_tower (R := ℤ), h_spanL]

Premises used: Submodule.span_span_of_tower, Int
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
⊢ Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤

Tactic:
hs.span_top

Premises used: IsZLattice.span_top
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
⊢ Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤

Tactic:
exact hs.span_top

Premises used: IsZLattice.span_top
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
⊢ Eq (α := Submodule K E) (span K (Set.range b)) ⊤

Tactic:
have h_spanE : span K (Set.range b) = ⊤ := by
    rw [← span_span_of_tower (R := ℤ), h_spanL]
    exact hs.span_top
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
rw : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = Finset.card.{u_2} (α := Free.ChooseBasisIndex ℤ ↥L) Finset.univ
rw₁ : Function.Injective b
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card

Tactic:
rw [Set.toFinset_range, Finset.univ.card_image_of_injective]

Premises used: Set.toFinset_range, Finset.univ, Finset.card_image_of_injective
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = Finset.card.{u_2} (α := Free.ChooseBasisIndex ℤ ↥L) Finset.univ

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
⊢ Function.Injective b

Tactic:
Subtype.coe_injective.comp (Basis.injective _)

Premises used: Module.Basis.injective, Subtype.coe_injective, Function.Injective.comp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
⊢ Function.Injective b

Tactic:
exact Subtype.coe_injective.comp (Basis.injective _)

Premises used: Module.Basis.injective, Subtype.coe_injective, Function.Injective.comp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card

Tactic:
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 _)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : 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
rw : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E

Tactic:
rw [finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : 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

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : 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
refine_1 : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E
refine_2 : finrank K E ≤ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : 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
refine_1 :
  ∀ (t : Set E) (ht_inc : t ⊆ Set.range b) (ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b)))
    (ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))),
    Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E

Tactic:
obtain ⟨t, ⟨ht_inc, ⟨ht_span, ht_lin⟩⟩⟩ := exists_linearIndependent K (Set.range b)

Premises used: exists_linearIndependent, Set.range
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
⊢ LE.le.{u_2} (α := Submodule K E) ⊤
    (span K (Set.range (ι := (↑t : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ t))))

Tactic:
simp [ht_span, h_spanE]
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
refine_1 : ∀ (this : Fintype (↑t : Type u_2)), Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E

Tactic:
have : Fintype t := Set.Finite.fintype ((Set.range b).toFinite.subset ht_inc)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
rwa rwa₁ rwa₂ rwa₃ :
  LinearIndependent (ι := Free.ChooseBasisIndex ℤ ↥L) ℤ (M := E)
    ((fun (a : ↥L) ↦ (↑a : E)) ∘ (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L))
⊢ LinearIndepOn ℤ id (Set.range b)

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

Premises used: linearIndepOn_id_range_iff, Module.Basis.injective, Subtype.coe_injective, Function.Injective.comp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
⊢ LinearIndepOn ℤ id (Set.range b)

Tactic:
have h : LinearIndepOn ℤ id (Set.range b) := by
      rwa [linearIndepOn_id_range_iff (Subtype.coe_injective.comp b₀.injective)]
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this_3 : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E :=
  Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)
this_4 : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : Eq (α := Submodule K E) (span K (Set.range b)) ⊤
h_card : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : Eq (α := Submodule K E) (span K t) (span K (Set.range b))
ht_lin : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ t }) K (Subtype.val (p := fun (x : E) ↦ x ∈ t))
e : Basis (↑t : Type u_2) K E := Basis.mk ht_lin ⋯
this : Fintype (↑t : Type u_2)
h : LinearIndepOn ℤ id (Set.range b)
refine_1 : ∀ (h : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)), ¬LinearIndepOn ℤ id (Set.range b)
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E

Tactic:
contrapose! h