awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
i : ι
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)
⊢ 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

Premises used: Int, Iff.mp, Module.Basis.mem_span_iff_repr_mem
-- 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 ι
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)
rw :
  Eq (α := K) ((↑(Int.floor (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
    ((algebraMap ℤ K : (a : ℤ) → K) z : 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:
rw [← hz]
-- 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 ι
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 (α := K) ((↑(Int.floor (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
    ((algebraMap ℤ K : (a : ℤ) → K) z : K)

Tactic:
congr_arg (Int.cast : ℤ → K) (Int.floor_intCast z)

Premises used: Int.cast, Int.floor_intCast, congr_arg
-- 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 ι
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 (α := K) ((↑(Int.floor (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
    ((algebraMap ℤ K : (a : ℤ) → K) z : K)

Tactic:
exact congr_arg (Int.cast : ℤ → K) (Int.floor_intCast z)

Premises used: Int.cast, Int.floor_intCast, congr_arg
-- 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 ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
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)
⊢ (↑(ceil b m) : E) = m

Tactic:
apply b.ext_elem

Premises used: Module.Basis.ext_elem
-- 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 ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
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)
⊢ ∀ (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:
simp_rw [repr_ceil_apply b]

Premises used: ZSpan.repr_ceil_apply
-- 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 ι
m : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) m
i : ι
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)
⊢ 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

Premises used: Int, Iff.mp, Module.Basis.mem_span_iff_repr_mem
-- 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 ι
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)
rw :
  Eq (α := K) ((↑(Int.ceil (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
    ((algebraMap ℤ K : (a : ℤ) → K) z : 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:
rw [← hz]
-- 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 ι
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 (α := K) ((↑(Int.ceil (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
    ((algebraMap ℤ K : (a : ℤ) → K) z : K)

Tactic:
congr_arg (Int.cast : ℤ → K) (Int.ceil_intCast z)

Premises used: Int.cast, Int.ceil_intCast, congr_arg
-- 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 ι
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 (α := K) ((↑(Int.ceil (α := K) ((algebraMap ℤ K : (a : ℤ) → K) z : K)) : K) : K)
    ((algebraMap ℤ K : (a : ℤ) → K) z : K)

Tactic:
exact congr_arg (Int.cast : ℤ → K) (Int.ceil_intCast z)

Premises used: Int.cast, Int.ceil_intCast, congr_arg
-- 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 ι
m : E
⊢ fract b m = m - (↑(floor b m) : E)

Tactic:
rfl

Premises used: ZSpan.fract, rfl
-- 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 ι
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)
rw₅ 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)
⊢ 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)

Tactic:
rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]

Premises used: map_sub, Int.fract, ZSpan.fract, ZSpan.repr_floor_apply, Finsupp.coe_sub, Pi.sub_apply
-- 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 ι
m : E
x : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b (fract b m)) : ι →₀ K) : (a : ι) → K) x : K)
    ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) x : K)

Tactic:
simp only [repr_fract_apply, Int.fract_fract]

Premises used: Int.fract_fract, ZSpan.repr_fract_apply
-- 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 ι
m : E
x : ι
⊢ Eq.{u_3 + 1} (α := K) ((((b.repr : (a : E) → ι →₀ K) (fract b (fract b m)) : ι →₀ K) : (a : ι) → K) x : K)
    ((((b.repr : (a : E) → ι →₀ K) (fract b m) : ι →₀ K) : (a : ι) → K) x : K)

Tactic:
classical simp only [repr_fract_apply, Int.fract_fract]

Premises used: Int.fract_fract, ZSpan.repr_fract_apply
-- 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 ι
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

Tactic:
(Basis.ext_elem_iff b).mpr fun i => ?_

Premises used: Iff.mpr, Module.Basis.ext_elem_iff
-- 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 ι
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

Tactic:
refine (Basis.ext_elem_iff b).mpr fun i => ?_

Premises used: Iff.mpr, Module.Basis.ext_elem_iff
-- 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 ι
m v : E
h : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) v
i : ι
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)
⊢ 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:
simp_rw [repr_fract_apply, Int.fract_eq_fract]

Premises used: Int.fract_eq_fract, ZSpan.repr_fract_apply
-- 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 ι
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) ((((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)
⊢ ∃ (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:
use (b.restrictScalars ℤ).repr ⟨v, h⟩ i

Premises used: Int, Module.Basis.repr, Subtype.mk, Module.Basis.restrictScalars, DFunLike.coe
-- 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 ι
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)
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)
⊢ fract b (v + m) = fract b m

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]

Premises used: Iff.mpr, Algebra.algebraMap, Int.fract_eq_fract, Submodule.coe_mk, map_add, Module.Basis.restrictScalars_repr_apply, Int, eq_intCast, Pi.add_apply, Finsupp.coe_add, ZSpan.repr_fract_apply, Module.Basis.ext_elem_iff, add_tsub_cancel_right
-- 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 ι
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
rw₁ rw₂ : fract b m = fract b m
⊢ fract b (m + v) = fract b m

Tactic:
rw [add_comm, fract_zSpan_add b m h]

Premises used: add_comm, ZSpan.fract_zSpan_add
-- 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 ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b

Tactic:
simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self,
    mem_fundamentalDomain, Set.mem_Ico]

Premises used: Set.mem_Ico, ZSpan.repr_fract_apply, Int.fract_eq_self, Module.Basis.ext_elem_iff, ZSpan.mem_fundamentalDomain
-- 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 ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b

Tactic:
classical simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self,
    mem_fundamentalDomain, Set.mem_Ico]

Premises used: Set.mem_Ico, ZSpan.repr_fract_apply, Int.fract_eq_self, Module.Basis.ext_elem_iff, ZSpan.mem_fundamentalDomain
-- 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 ι
x : E
⊢ fract b x ∈ fundamentalDomain b

Tactic:
fract_eq_self.mp (fract_fract b _)

Premises used: ZSpan.fract_fract, ZSpan.fract_eq_self, Iff.mp
-- 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 ι
⊢ Function.Surjective (β := (↑(fundamentalDomain b) : Type u_1)) (fractRestrict b)

Tactic:
fun x => ⟨↑x, Subtype.ext (fract_eq_self.mpr (Subtype.mem x))⟩

Premises used: Iff.mpr, ZSpan.fract_eq_self, Subtype.mem, Exists.intro, Subtype.val, Function.Surjective, Subtype.ext
-- 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 ι
x : E
⊢ (↑(fractRestrict b x) : E) = fract b x

Tactic:
rfl

Premises used: ZSpan.fract, rfl
-- 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 ι
m n : E
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)
⊢ fract b m = fract b n ↔
    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]

Premises used: eq_comm, Module.Basis.ext_elem_iff
-- 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 ι
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)
rw₁ rw₂ 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)
⊢ fract b m = fract b n ↔
    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]

Premises used: Finsupp.coe_neg, Set.mem_range, Algebra.algebraMap, sub_eq_neg_add, Int.fract_eq_fract, map_add, Int, map_neg, eq_intCast, eq_comm, Pi.add_apply, Finsupp.coe_add, ZSpan.repr_fract_apply, Module.Basis.ext_elem_iff, Pi.neg_apply, Module.Basis.mem_span_iff_repr_mem