awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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)
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 _ => ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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) ≤
    norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have h : norm.{u_1} (E := E) ((b : (a : ι) → E) i : E) = 1 * norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
Tactic: convert! mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ 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)
have suffices : norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
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
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤ 1
have 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
Tactic: rw [(norm_one.symm : 1 = ‖(1 : K)‖)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ norm.{u_3} (E := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K) ≤
    norm.{u_3} (E := K) 1
have h : LE.le.{u_3} (α := K) (|Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)| : K) (|1| : K)
Tactic: apply norm_le_norm_of_abs_le_abs
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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)
have h : 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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))
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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))
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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))
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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))
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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))
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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))
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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)
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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)
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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)
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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)
⊢ ‖fract b m‖ ≤ ∑ i : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) i : E)
have 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)
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 _)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 : ι
⊢ 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)
have 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)
Tactic: rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]