awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : DiscreteTopology.{u_3} ↥L₀
rw :
  Submodule.map (Submodule.subtype (span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) =
    Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤
rw₁ :
  Eq (α := Submodule ℝ E)
    (span ℝ
      ((⇑(Submodule.subtype (span ℝ (↑L : Set E))) : (a : ↥(span ℝ (↑L : Set E))) → E) ''
        (↑L₀ : Set ↥(span ℝ (↑L : Set E)))))
    (Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤)
rw₂ :
  Eq (α := Submodule ℝ E)
    (span ℝ
      ((⇑(Submodule.subtype (span ℝ (↑L : Set E))) : (a : ↥(span ℝ (↑L : Set E))) → E) ''
        (↑L₀ : Set ↥(span ℝ (↑L : Set E)))))
    (LinearMap.range (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))))
rw₃ :
  Eq (α := Submodule ℝ E)
    (span ℝ
      ((⇑(Submodule.subtype (span ℝ (↑L : Set E))) : (a : ↥(span ℝ (↑L : Set E))) → E) ''
        (↑L₀ : Set ↥(span ℝ (↑L : Set E)))))
    (span ℝ (↑L : Set E))
⊢ Eq (α := Submodule ℝ ↥(span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) ⊤
have rw₄ : Eq (α := Submodule ℝ E) (span ℝ (↑L : Set E)) (span ℝ (↑L : Set E))
Tactic: rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : DiscreteTopology.{u_3} ↥L₀
⊢ Module.Finite.{0, u_3} ℤ ↥L₀
have this₁ : IsZLattice ℝ L₀
Tactic: have : IsZLattice ℝ L₀ := ⟨by
    rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
inst_10 : IsZLattice K L
⊢ Free.{0, u_2} ℤ ↥L
have this : Module.Finite.{0, u_2} ℤ ↥L
Tactic: have : Module.Finite ℤ L := module_finite K L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
inst_10 : IsZLattice K L
this : Module.Finite.{0, u_2} ℤ ↥L
⊢ Free.{0, u_2} ℤ ↥L
have have : ∀ (this : Module ℚ E), Free.{0, u_2} ℤ ↥L
Tactic: have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
inst_10 : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this : Module ℚ E
⊢ Free.{0, u_2} ℤ ↥L
have this₁ : IsAddTorsionFree E
Tactic: have : IsAddTorsionFree E := .of_module_rat _
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
⊢ Free.{0, u_3} ℤ ↥L
have have : ∀ (this : Module ℚ E), Free.{0, u_3} ℤ ↥L
Tactic: have : Module ℚ E := Module.compHom E (algebraMap ℚ ℝ)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
this : Module ℚ E
⊢ Free.{0, u_3} ℤ ↥L
have this₁ : IsAddTorsionFree E
Tactic: have : IsAddTorsionFree E := .of_module_rat _
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have this : Module.Finite.{0, u_2} ℤ ↥L
Tactic: have : Module.Finite ℤ L := module_finite K L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 : Module.Finite.{0, u_2} ℤ ↥L
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have have : ∀ (this : Module ℚ E), finrank.{0, u_2} ℤ ↥L = finrank K E
Tactic: have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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 : Module ℚ E
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have this₁ : IsAddTorsionFree E
Tactic: have : IsAddTorsionFree E := .of_module_rat _
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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 : 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)
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have this₁ : LinearIndependent ℤ b
Tactic: have : LinearIndependent ℤ b :=
    LinearIndependent.map' b₀.linearIndependent (L.subtype) (ker_subtype _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
have h : span ℤ (Set.range b) =
  Submodule.map L.subtype
    (span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)))
Tactic: convert! congrArg (map (Submodule.subtype L)) b₀.span_eq
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 :
  span ℤ (Set.range b) =
    Submodule.map L.subtype
      (span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)))
⊢ span ℤ (Set.range b) = L
have h₁ : L = Submodule.map L.subtype ⊤
Tactic: convert! congrArg (map (Submodule.subtype L)) b₀.span_eq
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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) =
    Submodule.map L.subtype
      (span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L)))
have h : Eq (α := Submodule ℤ E)
  (span ℤ
    (Set.image (α := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L))
      (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L))))
  (span ℤ
    (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E)
      (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L) (⇑b₀ : (a : Free.ChooseBasisIndex ℤ ↥L) → ↥L))))
Tactic: rw [map_span, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have h_spanL : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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)) ⊤
have rw : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
Tactic: rw [← span_span_of_tower (R := ℤ), h_spanL]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have h_spanE : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
have rw : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = Finset.card.{u_2} (α := Free.ChooseBasisIndex ℤ ↥L) Finset.univ
Tactic: rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
have rw₁ : Function.Injective b
Tactic: rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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)) ⊤
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have h_card : 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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E
have rw : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
Tactic: rw [finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
have refine_1 : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) ≤ finrank K E
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
have refine_2 : finrank K E ≤ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
have 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
Tactic: obtain ⟨t, ⟨ht_inc, ⟨ht_span, ht_lin⟩⟩⟩ := exists_linearIndependent K (Set.range b)