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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
i : ι
⊢ HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) (v + m) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
have h₁ : HSub.hSub (α := K) (β := K)
    ((HAdd.hAdd (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) v : ι →₀ K)
            ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) :
          (a : ι) → K)
        i :
      K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
  (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                  LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                    (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
              (Subtype.mk (p := fun (x : E) ↦
                Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x) v
                h) :
            ι →₀ ℤ) :
          (a : ι) → ℤ)
        i) :
    K)
Tactic: rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
i : ι
h₁ :
  HSub.hSub (α := K) (β := K)
      ((HAdd.hAdd (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) v : ι →₀ K)
              ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) :
            (a : ι) → K)
          i :
        K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
⊢ HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) (v + m) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
have h₂ : HSub.hSub (β := K)
    (HAdd.hAdd (α := (a : ι) → K) (β := (a : ι) → K) (⇑((b.repr : (a : E) → ι →₀ K) v : ι →₀ K) : (a : ι) → K)
      (⇑((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
  (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                  LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                    (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
              (Subtype.mk (p := fun (x : E) ↦
                Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x) v
                h) :
            ι →₀ ℤ) :
          (a : ι) → ℤ)
        i) :
    K)
Tactic: rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
⊢ fract b (v + m) = fract b m
have refine : ∀ (i : ι),
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b (v + m)) : ι →₀ K) : (a : ι) → K) i : K)
    ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
Tactic: classical
  refine (Basis.ext_elem_iff b).mpr fun i => ?_
  simp_rw [repr_fract_apply, Int.fract_eq_fract]
  use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
  rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
refine :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b (v + m)) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
⊢ fract b (v + m) = fract b m
have refine₁ : ∀ (i : ι),
  ∃ (z : ℤ),
    HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) (v + m) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
      (↑z : K)
Tactic: classical
  refine (Basis.ext_elem_iff b).mpr fun i => ?_
  simp_rw [repr_fract_apply, Int.fract_eq_fract]
  use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
  rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
refine :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b (v + m)) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
refine₁ :
  ∀ (i : ι),
    ∃ (z : ℤ),
      HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) (v + m) : ι →₀ K) : (a : ι) → K) i : K)
          ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
        (↑z : K)
⊢ fract b (v + m) = fract b m
have h₁ : ∀ (i : ι),
  HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) (v + m) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
    (↑(((((Basis.repr (Basis.restrictScalars ℤ b) :
                    LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ)
                      (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (ι →₀ ℤ)) :
                  (a : ↥(span ℤ (Set.range (⇑b : (a : ι) → E)))) → ι →₀ ℤ)
                (Subtype.mk (p := fun (x : E) ↦
                  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x)
                  v h) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      K)
Tactic: classical
  refine (Basis.ext_elem_iff b).mpr fun i => ?_
  simp_rw [repr_fract_apply, Int.fract_eq_fract]
  use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
  rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
    ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
⊢ fract b (m + v) = fract b m
have rw : fract b (v + m) = fract b m
Tactic: rw [add_comm, fract_zSpan_add b m h]
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
rw : fract b (v + m) = fract b m
⊢ fract b (m + v) = fract b m
have rw₁ : fract b m = fract b m
Tactic: rw [add_comm, fract_zSpan_add b m h]
-- 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 ι
m n : E
⊢ fract b m = fract b n ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have rw : (∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
Tactic: rw [eq_comm, Basis.ext_elem_iff b]
-- 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 ι
m n : E
⊢ (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have simp_rw : (∀ (i : ι),
    Eq.{u_3 + 1} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i) : K)
      (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)) ↔
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
Tactic: simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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 ι
m n : E
simp_rw :
  (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i) : K)
        (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
⊢ (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have simp_rw₁ : (∀ (i : ι),
    ∃ (z : ℤ),
      HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
          ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
        (↑z : K)) ↔
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
Tactic: simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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 ι
m n : E
simp_rw :
  (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i) : K)
        (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₁ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
          (↑z : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
⊢ (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have simp_rw₂ : (∀ (i : ι),
    ∃ (z : ℤ),
      (↑z : K) =
        HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
          ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
Tactic: simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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 ι
m n : E
simp_rw :
  (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i) : K)
        (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₁ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
          (↑z : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₂ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
⊢ (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have simp_rw₃ : (∀ (i : ι),
    ∃ (z : ℤ),
      (↑z : K) =
        HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
          ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
  ∀ (i : ι),
    Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
      ((((b.repr : (a : E) → ι →₀ K) (-m + n) : ι →₀ K) : (a : ι) → K) i : K)
Tactic: simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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 ι
m n : E
simp_rw :
  (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) (Int.fract ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i) : K)
        (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₁ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K) =
          (↑z : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₂ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
simp_rw₃ :
  (∀ (i : ι),
      ∃ (z : ℤ),
        (↑z : K) =
          HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)
            ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) ↔
    ∀ (i : ι),
      Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
        ((((b.repr : (a : E) → ι →₀ K) (-m + n) : ι →₀ K) : (a : ι) → K) i : K)
⊢ (∀ (i : ι),
      Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
        ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have simp_rw₄ : (∀ (i : ι),
    ∃ (z : ℤ),
      (↑z : K) =
        HAdd.hAdd (α := K) (β := K) (-(((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
          ((((b.repr : (a : E) → ι →₀ K) n : ι →₀ K) : (a : ι) → K) i : K)) ↔
  ∀ (i : ι),
    Membership.mem (α := K) (γ := Set K) (Set.range (ι := ℤ) (⇑(algebraMap ℤ K) : (a : ℤ) → K))
      ((((b.repr : (a : E) → ι →₀ K) (-m + n) : ι →₀ K) : (a : ι) → K) i : K)
Tactic: simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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 ι
m n : E
⊢ fract b m = fract b n ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have rw : fract b n = fract b m ↔
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
Tactic: classical
  rw [eq_comm, Basis.ext_elem_iff b]
  simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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 ι
m n : E
rw :
  fract b n = fract b m ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
⊢ fract b m = fract b n ↔
    Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
have rw₁ : (∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b n) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)) ↔
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-m + n)
Tactic: classical
  rw [eq_comm, Basis.ext_elem_iff b]
  simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
    sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
    Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]
-- 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‖ =
    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))
have rw : ‖fract b m‖ = ‖fract b m‖
Tactic: rw [b.sum_repr]