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
c : K
hc : c ≠ 0
⊢ Eq.{u_1 + 1} (α := Submodule ℤ E) (span ℤ (Set.range fun (i : ι) ↦ HSMul.hSMul (β := E) c ((b : (a : ι) → E) i : E)))
    (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯) : (a : ι) → E)))
have h : ∀ (x : ι), HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E) = (b.isUnitSMul (w := fun (x : ι) ↦ c) sorry : (a : ι) → E) x
Tactic: congr!
-- 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
c : K
hc : c ≠ 0
x : ι
⊢ HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E) = (b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯ : (a : ι) → E) x
have h : HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E) = HSMul.hSMul (β := E) c ((b : (a : ι) → E) x : E)
Tactic: rw [Basis.isUnitSMul_apply]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace K F
f : E ≃ₗ[K] F
⊢ (⇑f : (a : E) → F) '' fundamentalDomain b = fundamentalDomain (b.map f)
have h : ∀ (x : F), Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔ x ∈ fundamentalDomain (b.map f)
Tactic: ext x
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔ x ∈ fundamentalDomain (b.map f)
have h : Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' fundamentalDomain b) x ↔
  Membership.mem (γ := Set F) ((⇑f.toEquiv : (a : E) → F) '' fundamentalDomain b) x
Tactic: rw [mem_fundamentalDomain, Basis.map_repr, LinearEquiv.trans_apply, ← mem_fundamentalDomain,
    show f.symm x = f.toEquiv.symm x by rfl, ← Set.mem_image_equiv]
-- 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
ι' : Type u_4
e : ι ≃ ι'
⊢ fundamentalDomain (b.reindex e) = fundamentalDomain b
have h : ∀ (x : E), x ∈ fundamentalDomain (b.reindex e) ↔ x ∈ fundamentalDomain b
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Fintype ι
⊢ Eq.{u_2 + 1} (α := Set (ι → ℝ)) (fundamentalDomain (ι := ι) (K := ℝ) (Pi.basisFun ℝ ι))
    (Set.pi (α := fun (x : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1)
have h : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) (fundamentalDomain (ι := ι) (K := ℝ) (Pi.basisFun ℝ ι)) x ↔
    Membership.mem (γ := Set (ι → ℝ)) (Set.pi (α := fun (x : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1) x
Tactic: ext
-- 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 : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
⊢ (↑(floor b m) : E) = m
have apply : ∀ (i : ι),
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
Tactic: apply b.ext_elem
-- 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 : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
⊢ ∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
have simp_rw : ∀ (i : ι),
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
Tactic: simp_rw [repr_floor_apply 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 : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
i : ι
⊢ Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
have obtain : ∀ (z : ℤ)
  (hz :
    Eq (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)),
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
Tactic: obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h 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 ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
i : ι
z : ℤ
hz : Eq (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
have rw : Eq (α := K) ((↑(Int.floor (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
  ((algebraMap ℤ K : (a : ℤ) → K) z : K)
Tactic: rw [← hz]
-- 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 : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
⊢ (↑(ceil b m) : E) = m
have apply : ∀ (i : ι),
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(ceil b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
Tactic: apply b.ext_elem
-- 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 : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
⊢ ∀ (i : ι),
    Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (↑(ceil b m) : E) : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
have simp_rw : ∀ (i : ι),
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.ceil.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
Tactic: simp_rw [repr_ceil_apply 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 : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
i : ι
⊢ Eq.{u_3 + 1} (α := K)
    ((↑(Int.ceil.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
have obtain : ∀ (z : ℤ)
  (hz :
    Eq (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)
      ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)),
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.ceil.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
Tactic: obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h 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 ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
i : ι
z : ℤ
hz : Eq (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((↑(Int.ceil.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
    ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
have rw : Eq (α := K) ((↑(Int.ceil (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
  ((algebraMap ℤ K : (a : ℤ) → K) z : K)
Tactic: rw [← hz]
-- 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 : E
i : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
have rw : Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (m - (↑(floor b m) : E)) : ι →₀ K) : (a : ι) → K) i : K)
  (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
Tactic: rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.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 ι
m : E
i : ι
rw :
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (m - (↑(floor b m) : E)) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
have rw₁ : Eq.{u_3 + 1} (α := K)
  ((HSub.hSub (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K)
          ((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) :
        (a : ι) → K)
      i :
    K)
  (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
Tactic: rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.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 ι
m : E
i : ι
rw :
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (m - (↑(floor b m) : E)) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₁ :
  Eq.{u_3 + 1} (α := K)
    ((HSub.hSub (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K)
            ((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) :
          (a : ι) → K)
        i :
      K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
have rw₂ : HSub.hSub (α := (a : ι) → K) (β := (a : ι) → K) (⇑((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K)
    (⇑((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i =
  Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
Tactic: rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.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 ι
m : E
i : ι
rw :
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (m - (↑(floor b m) : E)) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₁ :
  Eq.{u_3 + 1} (α := K)
    ((HSub.hSub (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K)
            ((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) :
          (a : ι) → K)
        i :
      K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₂ :
  HSub.hSub (α := (a : ι) → K) (β := (a : ι) → K) (⇑((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K)
      (⇑((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i =
    Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
have rw₃ : HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
    ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K) =
  Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
Tactic: rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.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 ι
m : E
i : ι
rw :
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (m - (↑(floor b m) : E)) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₁ :
  Eq.{u_3 + 1} (α := K)
    ((HSub.hSub (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K)
            ((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) :
          (a : ι) → K)
        i :
      K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₂ :
  HSub.hSub (α := (a : ι) → K) (β := (a : ι) → K) (⇑((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K)
      (⇑((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i =
    Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
rw₃ :
  HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K) =
    Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
have rw₄ : HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K) =
  Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
Tactic: rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.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 ι
m : E
i : ι
rw :
  Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (m - (↑(floor b m) : E)) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₁ :
  Eq.{u_3 + 1} (α := K)
    ((HSub.hSub (α := ι →₀ K) (β := ι →₀ K) ((b.repr : (a : E) → ι →₀ K) m : ι →₀ K)
            ((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) :
          (a : ι) → K)
        i :
      K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
rw₂ :
  HSub.hSub (α := (a : ι) → K) (β := (a : ι) → K) (⇑((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K)
      (⇑((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i =
    Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
rw₃ :
  HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
      ((((b.repr : (a : E) → ι →₀ K) (↑(floor b m) : E) : ι →₀ K) : (a : ι) → K) i : K) =
    Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
rw₄ :
  HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
      ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K) =
    Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i)
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) i : K)
    (Int.fract ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i) : K)
have rw₅ : HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K) =
  HSub.hSub (α := K) (β := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)
    ((↑(Int.floor.{u_3} (α := K) ((((b.repr : (a : E) → ι →₀ K) m : ι →₀ K) : (a : ι) → K) i : K)) : K) : K)
Tactic: rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.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 ι
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: refine (Basis.ext_elem_iff b).mpr 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
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)
have simp_rw : ∃ (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: simp_rw [repr_fract_apply, Int.fract_eq_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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
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)
have h₁ : 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: use (b.restrictScalars ℤ).repr ⟨v, h⟩ i