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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
⊢ Module.Finite.{0, u_2} ℤ ↥L

Tactic:
have : Module.Finite ℤ L := ZLattice.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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this : Module.Finite.{0, u_2} ℤ ↥L
⊢ Free.{0, u_2} ℤ ↥L

Tactic:
have : Free ℤ L := ZLattice.module_free 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
have : (this : Fintype ι) → Basis ι K E
⊢ Basis ι K E

Tactic:
have : Fintype ι := Fintype.ofEquiv _ e
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))
refine_2 : Fintype.card ι = finrank K E
⊢ Basis ι K E

Tactic:
refine basisOfTopLeSpanOfCardEqFinrank (L.subtype ∘ b) ?_ ?_

Premises used: Function.comp, basisOfTopLeSpanOfCardEqFinrank, Submodule.subtype, DFunLike.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 : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_1 :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.range.{u_2, u_3 + 1} (ι := ι)
              (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₁ :
  LE.le (α := Submodule K E) ⊤
    (span K
      (↑(span ℤ
            (Set.image (α := ↥L) (⇑L.subtype : (a : ↥L) → E) (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) :
        Set E))
refine_1₂ :
  LE.le (α := Submodule K E) ⊤
    (span K (↑(Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L)))) : Set E))
refine_1₃ : LE.le (α := Submodule K E) ⊤ (span K (↑(Submodule.map L.subtype ⊤) : Set E))
refine_1₄ : LE.le (α := Submodule K E) ⊤ (span K (↑L.subtype.range : Set E))
refine_1₅ : LE.le (α := Submodule K E) ⊤ (span K (↑L : Set E))
refine_1₆ : Eq (α := Submodule K E) (span K (↑L : Set E)) ⊤
refine_1₇ refine_1₈ : Eq.{u_2 + 1} (α := Submodule K E) ⊤ ⊤
⊢ LE.le (α := Submodule K E) ⊤
    (span K
      (Set.range.{u_2, u_3 + 1} (ι := ι) (Function.comp (β := ↥L) (⇑L.subtype : (a : ↥L) → E) (⇑b : (a : ι) → ↥L))))

Tactic:
rw [← span_span_of_tower ℤ, Set.range_comp, ← map_span, Basis.span_eq, Submodule.map_top,
      range_subtype, top_le_iff, hs.span_top]

Premises used: Set.range_comp, Submodule.span_span_of_tower, Submodule.map_top, Int, IsZLattice.span_top, top_le_iff, Submodule.map_span, Module.Basis.span_eq, Submodule.range_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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
this_1 : Module.Finite.{0, u_2} ℤ ↥L
this_2 : Free.{0, u_2} ℤ ↥L
e : Equiv.{u_2 + 1, u_3 + 1} (Free.ChooseBasisIndex ℤ ↥L) ι := indexEquiv (Free.chooseBasis ℤ ↥L) b
this : Fintype ι
refine_2 : Fintype.card.{u_2} (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
refine_2₁ : finrank.{0, u_2} ℤ ↥L = finrank K E
refine_2₂ refine_2₃ : finrank K E = finrank K E
⊢ Fintype.card ι = finrank K E

Tactic:
rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank K L]

Premises used: Fintype.card_congr, ZLattice.rank, Module.finrank_eq_card_chooseBasisIndex
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
i : ι
⊢ Eq.{u_2 + 1} (α := E) ((ofZLatticeBasis K L b : (a : ι) → E) i : E) ((↑((b : (a : ι) → ↥L) i) : E) : E)

Tactic:
simp [Basis.ofZLatticeBasis]

Premises used: Module.Basis.ofZLatticeBasis
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
x : ↥L
i : ι
this :
  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 →ₗ[ℤ] ι →₀ ℤ))
⊢ 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)

Tactic:
DFunLike.congr_fun (LinearMap.congr_fun this x) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
x : ↥L
i : ι
this :
  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 →ₗ[ℤ] ι →₀ ℤ))
⊢ 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)

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this x) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
x : ↥L
i : ι
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 →ₗ[ℤ] ι →₀ ℤ))
⊢ 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)

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
-- 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
ι : 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 →ₗ[ℤ] ι →₀ ℤ))

Tactic:
Basis.ext b fun i ↦ ?_

Premises used: Set.Mem, Module.Basis.ext
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
x : ↥L
i : ι
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)
⊢ 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:
refine Basis.ext b fun i ↦ ?_

Premises used: Module.Basis.ext
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
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)))
⊢ 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:
congr
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
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
⊢ 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:
ext
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
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:
simp
-- 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
rw 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))))
⊢ 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:
rw [Submodule.map_span]

Premises used: 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
ι : Type u_3
hs : IsZLattice K L
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
⊢ Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) = L

Tactic:
simp [b.span_eq]

Premises used: 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
ι : 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)))
calc₂ : Submodule.map L.subtype (span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → ↥L))) = L
⊢ span ℤ (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑(ofZLatticeBasis K L b) : (a : ι) → E)) = 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]

Premises used: Module.Basis.ofZLatticeBasis, Int, Submodule.span, Submodule.subtype, Set.image, Set.range, Submodule.map, DFunLike.coe
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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 (↥(span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))))
    (fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ

Tactic:
ZSpan.isAddFundamentalDomain (b.ofZLatticeBasis ℝ) μ

Premises used: Real, Module.Basis.ofZLatticeBasis, ZSpan.isAddFundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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))
h₁ 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))
⊢ IsAddFundamentalDomain (↥L) (fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ

Tactic:
convert! ZSpan.isAddFundamentalDomain (b.ofZLatticeBasis ℝ) μ

Premises used: Real, Module.Basis.ofZLatticeBasis, ZSpan.isAddFundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
x : E
⊢ L = span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))

Tactic:
(b.ofZLatticeBasis_span ℝ).symm

Premises used: Real, Module.Basis.ofZLatticeBasis_span, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
x : E
⊢ L = span ℤ (Set.range.{u_4, u_3 + 1} (ι := ι) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E))

Tactic:
exact (b.ofZLatticeBasis_span ℝ).symm

Premises used: Real, Module.Basis.ofZLatticeBasis_span, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
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
e_1 : ↥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:
(b.ofZLatticeBasis_span ℝ).symm

Premises used: Real, Module.Basis.ofZLatticeBasis_span, Eq.symm