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 : 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 : finrank K E < Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)
h_1 : LinearIndepOn.{u_2, 0, u_2} (ι := E) ℚ id (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))
h_mapsto :
  Set.MapsTo (fun (n : ℤ) ↦ fract e (n • v)) Set.univ
    (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩ (↑L : Set E))
h_finite :
  (Metric.closedBall 0 (∑ i : (↑t : Type u_2), norm (E := E) ((e : (a : (↑t : Type u_2)) → E) i : E)) ∩
      (↑L : Set E)).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : HAdd.hAdd (α := ℚ) (-(↑n : ℚ)) (↑m : ℚ) ≠ 0
refine_1 :
  HSMul.hSMul (α := ℚ) (-(↑n : ℚ)) v + HSMul.hSMul (α := ℚ) (↑m : ℚ) v ∈
    (↑(span ℤ (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))) : Set E)
refine_1₁ :
  -HSMul.hSMul (α := ℚ) (↑n : ℚ) v + HSMul.hSMul (α := ℚ) (↑m : ℚ) v ∈
    (↑(span ℤ (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))) : Set E)
refine_1₂ :
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E)))
    (-HSMul.hSMul (α := ℚ) (↑n : ℚ) v + HSMul.hSMul (α := ℚ) (↑m : ℚ) v)
refine_1₃ : fract e (HSMul.hSMul (α := ℚ) (↑n : ℚ) v) = fract e (HSMul.hSMul (α := ℚ) (↑m : ℚ) v)
⊢ HAdd.hAdd (α := ℚ) (-(↑n : ℚ)) (↑m : ℚ) • v ∈
    (↑(span ℤ (Set.range (ι := (↑t : Type u_2)) (⇑e : (a : (↑t : Type u_2)) → E))) : Set E)
have refine_1₄ : fract e (n • v) = fract e (HSMul.hSMul (α := ℚ) (↑m : ℚ) v)
Tactic: rwa [add_smul, neg_smul, SetLike.mem_coe, ← fract_eq_fract, Int.cast_smul_eq_zsmul ℚ,
      Int.cast_smul_eq_zsmul ℚ]
-- 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 K E ≤ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
have refine_2 : finrank.{u_1, u_2} K ↥(span K (Set.range b)) ≤ Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L)
Tactic: rw [← topEquiv.finrank_eq, ← h_spanE]
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
⊢ Basis ι K E
have this : Module.Finite.{0, u_2} ℤ ↥L
Tactic: have : Module.Finite ℤ L := ZLattice.module_finite K L
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this : Module.Finite.{0, u_2} ℤ ↥L
⊢ Basis ι K E
have this₁ : Free.{0, u_2} ℤ ↥L
Tactic: have : Free ℤ L := ZLattice.module_free 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
⊢ Basis ι K E
have have : (this : Fintype ι) → Basis ι K E
Tactic: have : Fintype ι := Fintype.ofEquiv _ e
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
⊢ Basis ι K E
have refine_1 : LE.le (α := Submodule K E) ⊤
  (span K (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
Tactic: refine basisOfTopLeSpanOfCardEqFinrank (L.subtype ∘ b) ?_ ?_
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
⊢ Basis ι K E
have refine_2 : Fintype.card ι = finrank K E
Tactic: refine basisOfTopLeSpanOfCardEqFinrank (L.subtype ∘ b) ?_ ?_
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1 : LE.le (α := Submodule K E) ⊤
  (span K
    (↑(span ℤ
          (Set.range.{u_2, u_3 + 1} (ι := ι)
            (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
      Set E))
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₁ : LE.le (α := Submodule K E) ⊤
  (span K
    (↑(span ℤ
          (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
      Set E))
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₂ : LE.le (α := Submodule K E) ⊤
  (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₂ :
  LE.le (α := Submodule K E) ⊤
    (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₃ : LE.le (α := Submodule K E) ⊤ (span K (↑(Submodule.map L.subtype ⊤) : Set E))
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₂ :
  LE.le (α := Submodule K E) ⊤
    (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
refine_1₃ : LE.le (α := Submodule K E) ⊤ (span K (↑(Submodule.map L.subtype ⊤) : Set E))
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₄ : LE.le (α := Submodule K E) ⊤ (span K (↑L.subtype.range : Set E))
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₂ :
  LE.le (α := Submodule K E) ⊤
    (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
refine_1₃ : LE.le (α := Submodule K E) ⊤ (span K (↑(Submodule.map L.subtype ⊤) : Set E))
refine_1₄ : LE.le (α := Submodule K E) ⊤ (span K (↑L.subtype.range : Set E))
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₅ : LE.le (α := Submodule K E) ⊤ (span K (↑L : Set E))
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₂ :
  LE.le (α := Submodule K E) ⊤
    (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
refine_1₃ : LE.le (α := Submodule K E) ⊤ (span K (↑(Submodule.map L.subtype ⊤) : Set E))
refine_1₄ : LE.le (α := Submodule K E) ⊤ (span K (↑L.subtype.range : Set E))
refine_1₅ : LE.le (α := Submodule K E) ⊤ (span K (↑L : Set E))
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₆ : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₂ :
  LE.le (α := Submodule K E) ⊤
    (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
refine_1₃ : LE.le (α := Submodule K E) ⊤ (span K (↑(Submodule.map L.subtype ⊤) : Set E))
refine_1₄ : LE.le (α := Submodule K E) ⊤ (span K (↑L.subtype.range : Set E))
refine_1₅ : LE.le (α := Submodule K E) ⊤ (span K (↑L : Set E))
refine_1₆ : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
have refine_1₇ : Eq.{u_2 + 1} (α := Submodule K E) ⊤ ⊤
Tactic: rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
⊢ Fintype.card ι = finrank K E
have refine_2 : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
Tactic: rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_2 : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
⊢ Fintype.card ι = finrank K E
have refine_2₁ : finrank.{0, u_2} ℤ ↥L = finrank K E
Tactic: rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_2 : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
refine_2₁ : finrank.{0, u_2} ℤ ↥L = finrank K E
⊢ Fintype.card ι = finrank K E
have refine_2₂ : finrank K E = finrank K E
Tactic: rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank K L]