-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem norm_fract_le [HasSolidNorm K] (m : E) : ‖fract b m‖ ≤ ∑ i, ‖b i‖

Proof state:
case h.e'_4
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract ((b.repr m) i)‖ ≤ 1
⊢ ‖b i‖ = 1 * ‖b i‖

Tactic:
exact (one_mul _).symm

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract ((b.repr m) i)‖ ≤ ‖1‖

Tactic:
apply norm_le_norm_of_abs_le_abs

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ |Int.fract ((b.repr m) i)| ≤ |1|

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i : ι, ‖b i‖

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

Result:
no goals

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ |Int.fract ((b.repr m) i)| ≤ |1|

Tactic:
rw [abs_one, Int.abs_fract]

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ Int.fract ((b.repr m) i) ≤ 1

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i : ι, ‖b i‖

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 _ => ?_

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract ((b.repr m) i)‖ * ‖b i‖ ≤ ‖b i‖

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract ((b.repr m) i)‖ ≤ 1

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

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract ((b.repr m) i)‖ ≤ ‖1‖

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ∑ i : ι, ‖Int.fract ((b.repr m) i) • b i‖ = ∑ i : ι, ‖Int.fract ((b.repr m) i)‖ * ‖b i‖

Tactic:
simp_rw [norm_smul]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract ((b.repr m) i)‖ ≤ 1
⊢ ‖Int.fract ((b.repr m) i)‖ * ‖b i‖ ≤ ‖b i‖

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

Result:
case h.e'_4
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract ((b.repr m) i)‖ ≤ 1
⊢ ‖b i‖ = 1 * ‖b i‖

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ = ‖∑ i : ι, (b.repr (fract b m)) i • b i‖

Tactic:
rw [b.sum_repr]

Result:
no goals

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ Int.fract ((b.repr m) i) ≤ 1

Tactic:
exact le_of_lt (Int.fract_lt_one _)

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖∑ i : ι, (b.repr (fract b m)) i • b i‖ = ‖∑ i : ι, Int.fract ((b.repr m) i) • b i‖

Tactic:
simp_rw [repr_fract_apply]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract ((b.repr m) i)‖ * ‖b i‖ ≤ ‖b i‖

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

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖Int.fract ((b.repr m) i)‖ ≤ 1