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
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
refine_1 : span ℤ s ≤ L
⊢ (↑(span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))) : Set E) ⊆ (↑L : Set E)

Tactic:
rw [SetLike.coe_subset_coe, Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, SetLike.coe_subset_coe, Module.Basis.coe_mk
-- 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
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ span ℤ s ≤ L

Tactic:
span_le.mpr h_incl

Premises used: Iff.mpr, Submodule.span_le
-- 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
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ span ℤ s ≤ L

Tactic:
exact span_le.mpr h_incl

Premises used: Iff.mpr, Submodule.span_le
-- 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
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
refine_2 : Submodule.FG (span ℤ s)
⊢ (L ⊓ LinearMap.ker (M₂ := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (mkQ (span ℤ s))).FG

Tactic:
rw [ker_mkQ, inf_of_le_right (span_le.mpr h_incl)]

Premises used: Iff.mpr, inf_of_le_right, Submodule.ker_mkQ, Submodule.span_le
-- 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
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ Submodule.FG (span ℤ s)

Tactic:
fg_span (LinearIndependent.setFinite h_lind)

Premises used: LinearIndependent.setFinite, Submodule.fg_span
-- 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
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ Submodule.FG (span ℤ s)

Tactic:
exact fg_span (LinearIndependent.setFinite h_lind)

Premises used: LinearIndependent.setFinite, Submodule.fg_span
-- 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
inst_10 : IsZLattice K L
⊢ Module.Finite.{0, u_2} ℤ ↥L

Tactic:
.of_fg (ZLattice.FG K L)

Premises used: Set.Mem, ZLattice.FG, Module.Finite.of_fg
-- 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_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
rw :
  L ≤
    LinearMap.range
      ((↑ℤ :
          {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)
⊢ (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)

Tactic:
rw [← LinearMap.coe_restrictScalars ℤ f, ← Submodule.map_coe (f.restrictScalars ℤ),
      Submodule.map_comap_eq_self]

Premises used: LinearMap.restrictScalars, Submodule.map_comap_eq_self, LinearMap.coe_restrictScalars, Int, Submodule.map_coe
-- 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_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
⊢ L ≤
    LinearMap.range
      ((↑ℤ :
          {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)

Tactic:
fun x hx ↦ LinearMap.mem_range.mpr ⟨⟨x, Submodule.subset_span hx⟩, rfl⟩

Premises used: Iff.mpr, Subtype.mk, LinearMap.mem_range, Exists.intro, Submodule.subset_span, 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_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
⊢ L ≤
    LinearMap.range
      ((↑ℤ :
          {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)

Tactic:
exact fun x hx ↦ LinearMap.mem_range.mpr ⟨⟨x, Submodule.subset_span hx⟩, rfl⟩

Premises used: Iff.mpr, LinearMap.mem_range, Exists.intro, 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_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
⊢ (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)

Tactic:
have h_img : f '' L₀ = L := by
    rw [← LinearMap.coe_restrictScalars ℤ f, ← Submodule.map_coe (f.restrictScalars ℤ),
      Submodule.map_comap_eq_self]
    exact fun x hx ↦ LinearMap.mem_range.mpr ⟨⟨x, Submodule.subset_span hx⟩, 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_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 : Module.Finite.{0, u_3} ℤ ↥L₀
⊢ Submodule.map
      ((↑ℤ :
          {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₀ =
    L

Tactic:
have : L₀.map (f.restrictScalars ℤ) = L :=
      SetLike.ext'_iff.mpr h_img
-- 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_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_1 : Module.Finite.{0, u_3} ℤ ↥L₀
this :
  Submodule.map
      ((↑ℤ :
          {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₀ =
    L
⊢ Module.Finite.{0, u_3} ℤ ↥L

Tactic:
convert! this ▸ Module.Finite.map L₀ (f.restrictScalars ℤ)
-- 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_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)
suffices : Module.Finite.{0, u_3} ℤ ↥L₀
⊢ Module.Finite.{0, u_3} ℤ ↥L

Tactic:
suffices Module.Finite ℤ L₀ by
    have : L₀.map (f.restrictScalars ℤ) = L :=
      SetLike.ext'_iff.mpr h_img
    convert! this ▸ Module.Finite.map L₀ (f.restrictScalars ℤ)
-- 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_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)
⊢ DiscreteTopology.{u_3} ↥L₀

Tactic:
DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)

Premises used: Set.Mem, setOf, Submodule.injective_subtype, SetLike.coe, Set.preimage, DiscreteTopology.preimage_of_continuous_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_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)
refine :
  Continuous (X := ↥(span ℝ (↑L : Set E))) (Y := E)
    (⇑((↑ℤ :
            {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) :
      (a : ↥(span ℝ (↑L : Set E))) → E)
⊢ DiscreteTopology.{u_3} ↥L₀

Tactic:
refine DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)

Premises used: Submodule.injective_subtype, SetLike.coe, DiscreteTopology.preimage_of_continuous_injective