-- 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₁ :
  ‖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))
b₂ :
  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))
b₃ :
  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))
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)
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) ≤ 1
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_3} (E := K) 1
h :
  ∀ (i : ι),
    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)
h₁ :
  ∀ (i : ι),
    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)
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)

Tactic:
classical
  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 _ => ?_
  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
  rw [(norm_one.symm : 1 = ‖(1 : K)‖)]
  apply norm_le_norm_of_abs_le_abs
  rw [abs_one, Int.abs_fract]
  exact le_of_lt (Int.fract_lt_one _)

Premises used: le_of_lt, NormOneClass.norm_one, norm_le_norm_of_abs_le_abs, Int.abs_fract, ZSpan.fract, Int.fract_lt_one, Finset.sum_le_sum, abs_one, Eq.symm, norm_sum_le