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_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)
⊢ 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)

Tactic:
LinearMap.continuous_of_finiteDimensional f

Premises used: LinearMap.continuous_of_finiteDimensional
-- 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)
⊢ 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)

Tactic:
exact LinearMap.continuous_of_finiteDimensional f

Premises used: LinearMap.continuous_of_finiteDimensional
-- 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:
have : DiscreteTopology L₀ := by
    refine DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)
    exact LinearMap.continuous_of_finiteDimensional f
-- 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 : 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))
rw₄ rw₅ : Eq (α := Submodule ℝ E) (span ℝ (↑L : Set E)) (span ℝ (↑L : Set E))
⊢ Eq (α := Submodule ℝ ↥(span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(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]

Premises used: Submodule.map_top, Function.Injective.eq_iff, Submodule.injective_subtype, Submodule.map_span, Submodule.range_subtype, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_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₀
⊢ 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]⟩
-- 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 : DiscreteTopology.{u_3} ↥L₀
this : IsZLattice ℝ L₀
⊢ Module.Finite.{0, u_3} ℤ ↥L₀

Tactic:
ZLattice.module_finite ℝ L₀

Premises used: Real, Set.Mem, ZLattice.module_finite
-- 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 : DiscreteTopology.{u_3} ↥L₀
this : IsZLattice ℝ L₀
⊢ Module.Finite.{0, u_3} ℤ ↥L₀

Tactic:
exact ZLattice.module_finite ℝ L₀

Premises used: Real, ZLattice.module_finite
-- 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:
have : Module.Finite ℤ L := module_finite K L
-- 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
this : Module.Finite.{0, u_2} ℤ ↥L
have : ∀ (this : Module ℚ E), Free.{0, u_2} ℤ ↥L
⊢ Free.{0, u_2} ℤ ↥L

Tactic:
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
-- 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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this : Module ℚ E
⊢ IsAddTorsionFree E

Tactic:
have : IsAddTorsionFree E := .of_module_rat _
-- 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
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this : IsAddTorsionFree E
⊢ Free.{0, u_2} ℤ ↥L

Tactic:
infer_instance
-- 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
have : ∀ (this : Module ℚ E), Free.{0, u_3} ℤ ↥L
⊢ Free.{0, u_3} ℤ ↥L

Tactic:
have : Module ℚ E := Module.compHom E (algebraMap ℚ ℝ)
-- 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
this : Module ℚ E
⊢ IsAddTorsionFree E

Tactic:
have : IsAddTorsionFree E := .of_module_rat _
-- 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
this_1 : Module ℚ E
this : IsAddTorsionFree E
⊢ Free.{0, u_3} ℤ ↥L

Tactic:
infer_instance
-- 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
⊢ Module.Finite.{0, u_2} ℤ ↥L

Tactic:
have : Module.Finite ℤ L := module_finite K L
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this : Module.Finite.{0, u_2} ℤ ↥L
have : ∀ (this : Module ℚ E), finrank.{0, u_2} ℤ ↥L = finrank K E
⊢ finrank.{0, u_2} ℤ ↥L = finrank K E

Tactic:
have : Module ℚ E := Module.compHom E (algebraMap ℚ K)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this : Module ℚ E
⊢ IsAddTorsionFree E

Tactic:
have : IsAddTorsionFree E := .of_module_rat _
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Module ℚ E
this : 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)
⊢ LinearIndependent ℤ b

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

Tactic:
congrArg (map (Submodule.subtype L)) b₀.span_eq

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

Tactic:
convert! congrArg (map (Submodule.subtype L)) b₀.span_eq

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

Tactic:
rw [map_span, Set.range_comp]

Premises used: Set.range_comp, Submodule.map_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
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
⊢ 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:
rfl