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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
x : ↥L
i : ι
⊢ Eq.{u_1 + 1} (α := K) ((((repr (ofZLatticeBasis K L b) : (a : E) → ι →₀ K) (↑x : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((↑((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i) : K) : K)
have suffices : Eq (α := ↥L →ₗ[ℤ] ι →₀ K)
  ((↑ℤ :
        {S : Type u_1} →
          {M : Type u_2} →
            {M₂ : Type (max u_1 u_3)} →
              [inst : Semiring ℤ] →
                [inst_10 : Semiring S] →
                  [inst_11 : AddCommMonoid M] →
                    [inst_12 : AddCommMonoid M₂] →
                      [inst_13 : Module ℤ M] →
                        [inst_14 : Module ℤ M₂] →
                          [inst_15 : Module S M] →
                            [inst_16 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) ∘ₗ
    L.subtype)
  (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ (↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ))
Tactic: suffices ((b.ofZLatticeBasis K L).repr.toLinearMap.restrictScalars ℤ) ∘ₗ L.subtype
      = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ b.repr.toLinearMap by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
-- 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
x : ↥L
i : ι
⊢ Eq (α := ↥L →ₗ[ℤ] ι →₀ K)
    ((↑ℤ :
          {S : Type u_1} →
            {M : Type u_2} →
              {M₂ : Type (max u_1 u_3)} →
                [inst : Semiring ℤ] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module ℤ M] →
                          [inst_14 : Module ℤ M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) ∘ₗ
      L.subtype)
    (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ (↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ))
have refine : ∀ (i : ι),
  Eq (α := ι →₀ K)
    (((↑ℤ :
                {S : Type u_1} →
                  {M : Type u_2} →
                    {M₂ : Type (max u_1 u_3)} →
                      [inst : Semiring ℤ] →
                        [inst_10 : Semiring S] →
                          [inst_11 : AddCommMonoid M] →
                            [inst_12 : AddCommMonoid M₂] →
                              [inst_13 : Module ℤ M] →
                                [inst_14 : Module ℤ M₂] →
                                  [inst_15 : Module S M] →
                                    [inst_16 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) ∘ₗ
            L.subtype :
          (a : ↥L) → ι →₀ K)
        ((b : (a : ι) → ↥L) i) :
      ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ (↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ K)
        ((b : (a : ι) → ↥L) i) :
      ι →₀ K)
Tactic: refine Basis.ext b fun i ↦ ?_
-- 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
x : ↥L
i_1 i : ι
⊢ Eq (α := ι →₀ K)
    (((↑ℤ :
                {S : Type u_1} →
                  {M : Type u_2} →
                    {M₂ : Type (max u_1 u_3)} →
                      [inst : Semiring ℤ] →
                        [inst_10 : Semiring S] →
                          [inst_11 : AddCommMonoid M] →
                            [inst_12 : AddCommMonoid M₂] →
                              [inst_13 : Module ℤ M] →
                                [inst_14 : Module ℤ M₂] →
                                  [inst_15 : Module S M] →
                                    [inst_16 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K) ∘ₗ
            L.subtype :
          (a : ↥L) → ι →₀ K)
        ((b : (a : ι) → ↥L) i) :
      ι →₀ K)
    ((Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ (↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ K)
        ((b : (a : ι) → ↥L) i) :
      ι →₀ K)
have simp_rw : Eq (α := ι →₀ K)
  (Function.comp (α := ↥L) (β := E)
    (⇑((↑ℤ :
            {S : Type u_1} →
              {M : Type u_2} →
                {M₂ : Type (max u_1 u_3)} →
                  [inst : Semiring ℤ] →
                    [inst_10 : Semiring S] →
                      [inst_11 : AddCommMonoid M] →
                        [inst_12 : AddCommMonoid M₂] →
                          [inst_13 : Module ℤ M] →
                            [inst_14 : Module ℤ M₂] →
                              [inst_15 : Module S M] →
                                [inst_16 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
          (↑(repr (ofZLatticeBasis K L b)) : E →ₗ[K] ι →₀ K)) :
      (a : E) → ι →₀ K)
    ((⇑L.subtype : (a : ↥L) → E) : (a : ↥L) → E) ((b : (a : ι) → ↥L) i : ↥L))
  (Function.comp (α := ↥L) (β := ι →₀ ℤ) (⇑(Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K)) : (a : ι →₀ ℤ) → ι →₀ K)
    ((⇑(↑b.repr : ↥L →ₗ[ℤ] ι →₀ ℤ) : (a : ↥L) → ι →₀ ℤ) : (a : ↥L) → ι →₀ ℤ) ((b : (a : ι) → ↥L) i : ↥L))
Tactic: simp_rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, coe_subtype, ← b.ofZLatticeBasis_apply K, repr_self,
    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]
-- 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
⊢ Eq (α := Submodule ℤ E) (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)))
    (span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))))
have e_s : Eq (α := Set E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E))
  (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))
Tactic: congr
-- 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
⊢ Eq (α := Set E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E))
    (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))
have e_s : ∀ (x : E),
  Membership.mem (γ := Set E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)) x ↔
    Membership.mem (γ := Set E)
      (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) x
Tactic: ext
-- 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
⊢ span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) =
    Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))
have rw : Eq (α := Submodule ℤ E)
  (span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))))
  (span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))))
Tactic: rw [Submodule.map_span]
-- 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
⊢ span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)) = L
have calc : Eq (α := Submodule ℤ E) (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)))
  (span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))))
Tactic: calc span ℤ (Set.range (b.ofZLatticeBasis K))
    _ = span ℤ (L.subtype '' Set.range b) := by congr; ext; simp
    _ = map L.subtype (span ℤ (Set.range b)) := by rw [Submodule.map_span]
    _ = L := by simp [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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
calc :
  Eq (α := Submodule ℤ E) (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)))
    (span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))))
⊢ span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)) = L
have calc₁ : span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) =
  Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))
Tactic: calc span ℤ (Set.range (b.ofZLatticeBasis K))
    _ = span ℤ (L.subtype '' Set.range b) := by congr; ext; simp
    _ = map L.subtype (span ℤ (Set.range b)) := by rw [Submodule.map_span]
    _ = L := by simp [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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
calc :
  Eq (α := Submodule ℤ E) (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)))
    (span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))))
calc₁ :
  span ℤ (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) =
    Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))
⊢ span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)) = L
have calc₂ : Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) = L
Tactic: calc span ℤ (Set.range (b.ofZLatticeBasis K))
    _ = span ℤ (L.subtype '' Set.range b) := by congr; ext; simp
    _ = map L.subtype (span ℤ (Set.range b)) := by rw [Submodule.map_span]
    _ = L := by simp [b.span_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_3
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_4} ↥L
inst_4 : IsZLattice ℝ L
inst_5 : Finite ι
b : Basis.{u_3, 0, u_4} ι ℤ ↥L
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
μ : Measure E
⊢ IsAddFundamentalDomain (↥L) (fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ
have h : ∀ (x : E), L = span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))
Tactic: convert! ZSpan.isAddFundamentalDomain (b.ofZLatticeBasis ℝ) μ
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_3
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_4} ↥L
inst_4 : IsZLattice ℝ L
inst_5 : Finite ι
b : Basis.{u_3, 0, u_4} ι ℤ ↥L
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
μ : Measure E
h : ∀ (x : E), L = span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))
⊢ IsAddFundamentalDomain (↥L) (fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ
have h₁ : ↥L = ↥(span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))) →
  L = span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))
Tactic: convert! ZSpan.isAddFundamentalDomain (b.ofZLatticeBasis ℝ) μ
-- 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
ι : Type u_3
hs : IsZLattice K L_1
b : Basis.{u_3, 0, u_2} ι ℤ ↥L_1
E : Type u_4
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_4} ↥L
inst_14 : IsZLattice ℝ L
⊢ Countable.{u_4 + 1} ↥L
have simp_rw : Countable.{u_4 + 1}
  ↥(span ℤ
      (Set.range (ι := Free.ChooseBasisIndex ℤ ↥L)
        (⇑(Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) : (a : Free.ChooseBasisIndex ℤ ↥L) → E)))
Tactic: simp_rw [← (Module.Free.chooseBasis ℤ L).ofZLatticeBasis_span ℝ]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
⊢ Set.finrank ℝ s = Set.finrank ℤ s
have this : DiscreteTopology.{u_4} ↥L
Tactic: have : DiscreteTopology L := by
    let e : span ℤ s ≃L[ℤ] L :=
      ⟨f.symm, continuous_of_discreteTopology, Isometry.continuous fun _ ↦ congrFun rfl⟩
    exact e.toHomeomorph.discreteTopology
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
this : DiscreteTopology.{u_4} ↥L
⊢ Set.finrank ℝ s = Set.finrank ℤ s
have this₁ : IsZLattice ℝ L
Tactic: have : IsZLattice ℝ L := ⟨eq_top_iff.mpr <|
    span_span_coe_preimage.symm.le.trans (span_mono (Set.preimage_mono subset_span))⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology.{u_4} ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) :=
  comap (σ₁₂ := RingHom.id ℤ) (Submodule.subtype (Submodule.restrictScalars ℤ F)) (span ℤ s)
f : ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) :=
  comapSubtypeEquivOfLe ⋯
this_1 : DiscreteTopology.{u_4} ↥L
this : IsZLattice ℝ L
⊢ Set.finrank ℝ s = Set.finrank ℤ s
have rw : finrank.{0, u_4} ℝ ↥(span ℝ s) =
  finrank.{0, u_4} ℤ ↥(comap (Submodule.subtype (Submodule.restrictScalars ℤ (span ℝ s))) (span ℤ s))
Tactic: rw [Set.finrank, Set.finrank, ← f.finrank_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = Fintype.card ι
have rw : finrank.{0, u_1} ℤ ↥L = Fintype.card ι
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
rw : finrank.{0, u_1} ℤ ↥L = Fintype.card ι
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = Fintype.card ι
have rw₁ : finrank.{0, u_1} ℝ (ι → ℝ) = Fintype.card ι
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
rw : finrank.{0, u_1} ℤ ↥L = Fintype.card ι
rw₁ : finrank.{0, u_1} ℝ (ι → ℝ) = Fintype.card ι
⊢ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = Fintype.card ι
have rw₂ : Fintype.card ι = Fintype.card ι
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
e : F →ₗ[K] E
he : (↑L : Set E) ⊆ (↑e.range : Set E)
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L e) : Set F)) ⊤
have rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
e : F →ₗ[K] E
he : (↑L : Set E) ⊆ (↑e.range : Set E)
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L e) : Set F)) ⊤
have rw₁ : comap e (span K (↑L : Set E)) = ⊤
Tactic: rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
e : F →ₗ[K] E
he : (↑L : Set E) ⊆ (↑e.range : Set E)
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : comap e (span K (↑L : Set E)) = ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L e) : Set F)) ⊤
have rw₂ : comap e ⊤ = ⊤
Tactic: rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
hL : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
e : F →ₗ[K] E
he : (↑L : Set E) ⊆ (↑e.range : Set E)
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑e : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
rw₁ : comap e (span K (↑L : Set E)) = ⊤
rw₂ : comap e ⊤ = ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L e) : Set F)) ⊤
have rw₃ : Eq.{u_3 + 1} (α := Submodule K F) ⊤ ⊤
Tactic: rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace K F
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice K L
e : F ≃L[K] E
rw : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
⊢ Eq (α := Submodule K F) (span K (↑(ZLattice.comap K L (↑(↑e : F ≃ₗ[K] E) : F →ₗ[K] E)) : Set F)) ⊤
have rw₁ : Eq.{u_3 + 1} (α := Submodule K F) (span K ((⇑(↑e : F ≃ₗ[K] E) : (a : F) → E) ⁻¹' (↑L : Set E))) ⊤
Tactic: rw [ZLattice.coe_comap, LinearEquiv.coe_coe, e.coe_toLinearEquiv, ← e.image_symm_eq_preimage,
      ← ContinuousLinearEquiv.coe_toLinearEquiv, ← LinearEquiv.coe_coe, ← Submodule.map_span,
      IsZLattice.span_top, Submodule.map_top, e.symm.range]