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
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)
⊢ fract b x ∈ (↑L : Set E)
have refine_1 : x + -(↑(floor b x) : E) ∈ L
Tactic: rw [fract, SetLike.mem_coe, sub_eq_add_neg]
-- 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
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)
⊢ x + -(↑(floor b x) : E) ∈ L
have refine_1 : (↑(span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))) : Set E) ⊆ (↑L : Set E)
Tactic: refine Submodule.add_mem _ h_mem
        (neg_mem (Set.mem_of_subset_of_mem ?_ (Subtype.mem (floor b x))))
-- 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
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 ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))) : Set E) ⊆ (↑L : Set E)
have refine_1 : span ℤ s ≤ L
Tactic: rw [SetLike.coe_subset_coe, Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
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))
⊢ (L ⊓ LinearMap.ker (M₂ := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ s)) (mkQ (span ℤ s))).FG
have refine_2 : Submodule.FG (span ℤ s)
Tactic: rw [ker_mkQ, inf_of_le_right (span_le.mpr h_incl)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
⊢ (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
have 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)
Tactic: rw [← LinearMap.coe_restrictScalars ℤ f, ← Submodule.map_coe (f.restrictScalars ℤ),
      Submodule.map_comap_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
⊢ Module.Finite.{0, u_3} ℤ ↥L
have h_img : (⇑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⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : Module.Finite.{0, u_3} ℤ ↥L₀
⊢ Module.Finite.{0, u_3} ℤ ↥L
have 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
Tactic: have : L₀.map (f.restrictScalars ℤ) = L :=
      SetLike.ext'_iff.mpr h_img
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
⊢ Module.Finite.{0, u_3} ℤ ↥L
have suffices : 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 ℤ)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
⊢ DiscreteTopology.{u_3} ↥L₀
have 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)
Tactic: refine DiscreteTopology.preimage_of_continuous_injective (L : Set E) ?_ (injective_subtype _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
⊢ Module.Finite.{0, u_3} ℤ ↥L₀
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : DiscreteTopology.{u_3} ↥L₀
⊢ Eq (α := Submodule ℝ ↥(span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) ⊤
have 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))) ⊤
Tactic: rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : DiscreteTopology.{u_3} ↥L₀
rw :
  Submodule.map (Submodule.subtype (span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) =
    Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤
⊢ Eq (α := Submodule ℝ ↥(span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) ⊤
have 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))) ⊤)
Tactic: rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : DiscreteTopology.{u_3} ↥L₀
rw :
  Submodule.map (Submodule.subtype (span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) =
    Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤
rw₁ :
  Eq (α := Submodule ℝ E)
    (span ℝ
      ((⇑(Submodule.subtype (span ℝ (↑L : Set E))) : (a : ↥(span ℝ (↑L : Set E))) → E) ''
        (↑L₀ : Set ↥(span ℝ (↑L : Set E)))))
    (Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤)
⊢ Eq (α := Submodule ℝ ↥(span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) ⊤
have 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))))
Tactic: rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E_1 : Type u_2
inst_5 : NormedAddCommGroup E_1
inst_6 : NormedSpace K E_1
inst_7 : FiniteDimensional K E_1
inst_8 : ProperSpace E_1
L_1 : Submodule ℤ E_1
inst_9 : DiscreteTopology.{u_2} ↥L_1
E : Type u_3
inst_10 : NormedAddCommGroup E
inst_11 : NormedSpace ℝ E
inst_12 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_13 : DiscreteTopology.{u_3} ↥L
f : ↥(span ℝ (↑L : Set E)) →ₗ[ℝ] E := Submodule.subtype (span ℝ (↑L : Set E))
L₀ : Submodule ℤ ↥(span ℝ (↑L : Set E)) :=
  comap
    ((↑ℤ :
        {S : Type} →
          {M M₂ : Type u_3} →
            [inst : Semiring ℤ] →
              [inst_14 : Semiring S] →
                [inst_15 : AddCommMonoid M] →
                  [inst_16 : AddCommMonoid M₂] →
                    [inst_17 : Module ℤ M] →
                      [inst_18 : Module ℤ M₂] →
                        [inst_19 : Module S M] →
                          [inst_20 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
      f)
    L
h_img : (⇑f : (a : ↥(span ℝ (↑L : Set E))) → E) '' (↑L₀ : Set ↥(span ℝ (↑L : Set E))) = (↑L : Set E)
this : DiscreteTopology.{u_3} ↥L₀
rw :
  Submodule.map (Submodule.subtype (span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) =
    Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤
rw₁ :
  Eq (α := Submodule ℝ E)
    (span ℝ
      ((⇑(Submodule.subtype (span ℝ (↑L : Set E))) : (a : ↥(span ℝ (↑L : Set E))) → E) ''
        (↑L₀ : Set ↥(span ℝ (↑L : Set E)))))
    (Submodule.map (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))) ⊤)
rw₂ :
  Eq (α := Submodule ℝ E)
    (span ℝ
      ((⇑(Submodule.subtype (span ℝ (↑L : Set E))) : (a : ↥(span ℝ (↑L : Set E))) → E) ''
        (↑L₀ : Set ↥(span ℝ (↑L : Set E)))))
    (LinearMap.range (M := ↥(span ℝ (↑L : Set E))) (Submodule.subtype (span ℝ (↑L : Set E))))
⊢ Eq (α := Submodule ℝ ↥(span ℝ (↑L : Set E))) (span ℝ (↑L₀ : Set ↥(span ℝ (↑L : Set E)))) ⊤
have 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))
Tactic: rw [← (Submodule.map_injective_of_injective (injective_subtype _)).eq_iff, Submodule.map_span,
      Submodule.map_top, range_subtype, h_img]