awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
rw rw₁ : ‖fract b m‖ = ‖fract b m‖
⊢ ‖fract b m‖ =
    norm.{u_1} (E := E)
      (∑ i : ι,
        HSMul.hSMul.{u_3, u_1, u_1} (α := K) (β := E)
          ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K) ((b : (a : ι) → E) i : E))

Tactic:
rw [b.sum_repr]

Premises used: Module.Basis.sum_repr
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
⊢ norm.{u_1} (E := E)
      (∑ i : ι,
        HSMul.hSMul.{u_3, u_1, u_1} (α := K) (β := E)
          ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K) ((b : (a : ι) → E) i : E)) =
    norm.{u_1} (E := E)
      (∑ i : ι,
        HSMul.hSMul.{u_3, u_1, u_1} (α := K) (β := E)
          (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ((b : (a : ι) → E) i : E))

Tactic:
simp_rw [repr_fract_apply]

Premises used: ZSpan.repr_fract_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
⊢ norm.{u_1} (E := E)
      (∑ i : ι,
        HSMul.hSMul.{u_3, u_1, u_1} (α := K) (β := E)
          (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ((b : (a : ι) → E) i : E)) ≤
    ∑ i : ι,
      ‖HSMul.hSMul.{u_3, u_1, u_1} (α := K) (β := E)
          (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ((b : (a : ι) → E) i : E)‖

Tactic:
norm_sum_le _ _

Premises used: norm_sum_le
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
⊢ Eq (α := ℝ)
    (∑ i : ι,
      ‖HSMul.hSMul.{u_3, u_1, u_1} (α := K) (β := E)
          (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ((b : (a : ι) → E) i : E)‖)
    (∑ i : ι,
      norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) *
        norm.{u_1} (E := E) ((b : (a : ι) → E) i : E))

Tactic:
simp_rw [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
⊢ LE.le (α := ℝ)
    (∑ i : ι,
      norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) *
        norm.{u_1} (E := E) ((b : (a : ι) → E) i : E))
    (∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E))

Tactic:
Finset.sum_le_sum fun i _ => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
b₁ :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) *
          norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) ≤
        norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
calc
    ‖fract b m‖ = ‖∑ i, b.repr (fract b m) i • b i‖ := by rw [b.sum_repr]
    _ = ‖∑ i, Int.fract (b.repr m i) • b i‖ := by simp_rw [repr_fract_apply]
    _ ≤ ∑ i, ‖Int.fract (b.repr m i) • b i‖ := norm_sum_le _ _
    _ = ∑ i, ‖Int.fract (b.repr m i)‖ * ‖b i‖ := by simp_rw [norm_smul]
    _ ≤ ∑ i, ‖b i‖ := Finset.sum_le_sum fun i _ => ?_

Premises used: ZSpan.fract, Finset.sum_le_sum, norm_sum_le
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
this : norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) *
      norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) ≤
    1 * norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
this : norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
h : norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) = 1 * norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) *
      norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) ≤
    norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
convert! mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)

Premises used: mul_le_mul_of_nonneg_right, norm_nonneg
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
this : norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
⊢ norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) = 1 * norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
(one_mul _).symm

Premises used: Eq.symm, one_mul
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
this : norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
⊢ norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) = 1 * norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
exact (one_mul _).symm

Premises used: Eq.symm, one_mul
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
suffices : norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) *
      norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) ≤
    norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
suffices ‖Int.fract ((b.repr m) i)‖ ≤ 1 by
    convert! mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
    exact (one_mul _).symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw :
  norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤
    norm.{u_3} (E := K) 1
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1

Tactic:
rw [(norm_one.symm : 1 = ‖(1 : K)‖)]

Premises used: NormOneClass.norm_one, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h : LE.le.{u_3} (α := K) (|Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)| : K) (|1| : K)
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤
    norm.{u_3} (E := K) 1

Tactic:
apply norm_le_norm_of_abs_le_abs

Premises used: norm_le_norm_of_abs_le_abs
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h : LE.le.{u_3} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) (1 : K)
⊢ LE.le.{u_3} (α := K) (|Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)| : K) (|1| : K)

Tactic:
rw [abs_one, Int.abs_fract]

Premises used: Int.abs_fract, abs_one
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ LE.le.{u_3} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) (1 : K)

Tactic:
le_of_lt (Int.fract_lt_one _)

Premises used: le_of_lt, Int.fract_lt_one
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
inst_7 : HasSolidNorm K
m : E
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ LE.le.{u_3} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) (1 : K)

Tactic:
exact le_of_lt (Int.fract_lt_one _)

Premises used: le_of_lt, Int.fract_lt_one
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
rw :
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K)
            ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x : K)) :
        K) :
      K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
rw₁ :
  Eq.{u_3 + 1} (α := K) ((↑⌊k⌋ : K) : K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
rw₂ rw₃ : Eq.{u_3 + 1} (α := K) (↑⌊k⌋ : K) (↑⌊k⌋ : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑(floor (Basis.singleton ι K) k) : K) : ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)

Tactic:
rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]

Premises used: Module.Basis.singleton_repr, ZSpan.repr_floor_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
rw :
  Eq.{u_3 + 1} (α := K)
    (Int.fract ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x) : K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
rw₁ : Int.fract k = (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x
rw₂ rw₃ : Int.fract k = Int.fract k
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K)
              (fract.{u_3, u_2, u_3} (ι := ι) (K := K) (Basis.singleton ι K) k) :
            ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)

Tactic:
rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]

Premises used: Module.Basis.singleton_repr, ZSpan.repr_fract_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
inst_7 : HasSolidNorm K
intro : ∀ (val : Fintype ι), IsBounded (fundamentalDomain b)
⊢ IsBounded (fundamentalDomain b)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
inst_7 : HasSolidNorm K
val : Fintype ι
⊢ IsBounded (fundamentalDomain b)

Tactic:
isBounded_iff_forall_norm_le.2 ⟨∑ j, ‖b j‖, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Norm.norm, Finset.univ, isBounded_iff_forall_norm_le, Exists.intro, DFunLike.coe, Finset.sum
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
inst_7 : HasSolidNorm K
val : Fintype ι
intro : ∀ (x : E) (hx : x ∈ fundamentalDomain b), ‖x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)
⊢ IsBounded (fundamentalDomain b)

Tactic:
refine isBounded_iff_forall_norm_le.2 ⟨∑ j, ‖b j‖, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Norm.norm, Finset.univ, isBounded_iff_forall_norm_le, Exists.intro, DFunLike.coe, Finset.sum
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
inst_7 : HasSolidNorm K
val : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
intro : ‖fract b x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)
⊢ ‖x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)

Tactic:
rw [← fract_eq_self.mpr hx]

Premises used: Iff.mpr, ZSpan.fract_eq_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
inst_7 : HasSolidNorm K
val : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖fract b x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)

Tactic:
apply norm_fract_le

Premises used: ZSpan.norm_fract_le
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
rw₆ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) + x = fract b ((↑y : E) + x)
rw₇ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) +ᵥ x = fract b ((↑y : E) +ᵥ x)
rw₈ : y +ᵥ x ∈ fundamentalDomain b ↔ y +ᵥ x = fract b (y +ᵥ x)
rw₉ : y +ᵥ x ∈ fundamentalDomain b ↔ fract b (y +ᵥ x) = y +ᵥ x
rw₁₀ rw₁₁ : fract b (y +ᵥ x) = y +ᵥ x ↔ fract b (y +ᵥ x) = y +ᵥ x
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

Tactic:
rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]

Premises used: Submodule.vadd_def, sub_eq_add_neg, eq_comm, add_comm, Subtype.ext_iff, ZSpan.fract_eq_self, vadd_eq_add, Subtype.mem, ZSpan.fract_zSpan_add, ZSpan.fract_apply, add_right_inj, NegMemClass.coe_neg
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
intro :
  ∀ (val : Fintype ι),
    ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b
⊢ ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
val : Fintype ι
⊢ ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b

Tactic:
⟨-floor b x, ?_, fun y h => ?_⟩

Premises used: ZSpan.floor, ExistsUnique, And.intro, Exists.intro, Neg.neg
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
val : Fintype ι
intro :
  (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b)
    (-floor b x)
intro₁ :
  ∀ (y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (h : (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b) y),
    y = -floor b x
⊢ ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b

Tactic:
refine ⟨-floor b x, ?_, fun y h => ?_⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
val : Fintype ι
⊢ (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b)
    (-floor b x)

Tactic:
(vadd_mem_fundamentalDomain b (-floor b x) x).mpr rfl

Premises used: Iff.mpr, ZSpan.floor, ZSpan.vadd_mem_fundamentalDomain, Neg.neg, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
val : Fintype ι
⊢ (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b)
    (-floor b x)

Tactic:
exact (vadd_mem_fundamentalDomain b (-floor b x) x).mpr rfl

Premises used: Iff.mpr, ZSpan.floor, ZSpan.vadd_mem_fundamentalDomain, Neg.neg, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
val : Fintype ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
h : (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b) y
⊢ y = -floor b x

Tactic:
(vadd_mem_fundamentalDomain b y x).mp h

Premises used: Iff.mp, ZSpan.vadd_mem_fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Finite ι
x : E
val : Fintype ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
h : (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b) y
⊢ y = -floor b x

Tactic:
exact (vadd_mem_fundamentalDomain b y x).mp h

Premises used: Iff.mp, ZSpan.vadd_mem_fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
refine_1 :
  HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) →
    (↑(fundamentalDomain b) : Type u_1)
refine_2 :
  ∀ (x y : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn x (fractRestrict b) ⋯)
        (Quotient.liftOn y (fractRestrict b) ⋯) →
      x = y
refine_3 :
  ∀ (x : (↑(fundamentalDomain b) : Type u_1)),
    ∃ (a : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
      Quotient.liftOn a (fractRestrict b) ⋯ = x
⊢ HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) ≃
    (↑(fundamentalDomain b) : Type u_1)

Tactic:
refine Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩

Premises used: And.intro, Equiv.ofBijective