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 ι
q : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x x_1 : E
h : x ≈ x_1
⊢ Eq (α := (↑(fundamentalDomain b) : Type u_1)) (fractRestrict b x) (fractRestrict b x_1)
have refine_1 : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-x + x_1)
Tactic: rw [Subtype.mk.injEq, fractRestrict_apply, fractRestrict_apply, 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 ι
x y : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
⊢ Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn x (fractRestrict b) ⋯)
      (Quotient.liftOn y (fractRestrict b) ⋯) →
    x = y
have refine_2 : ∀ (a b_1 : E),
  Eq (α := (↑(fundamentalDomain b) : Type u_1))
      (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦a⟧
        (fractRestrict b) sorry)
      (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦b_1⟧
        (fractRestrict b) sorry) →
    Eq (α :=
      HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦a⟧
      ⟦b_1⟧
Tactic: induction x, y using Quotient.inductionOn₂
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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 ι
a b_1 : E
hxy :
  Eq (α := (↑(fundamentalDomain b) : Type u_1))
    (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦a⟧
      (fractRestrict b) ⋯)
    (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦b_1⟧
      (fractRestrict b) ⋯)
⊢ Eq (α := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⟦a⟧ ⟦b_1⟧
have hxy₁ : fract b a = fract b b_1
Tactic: rw [Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Subtype.mk.injEq] at hxy
Cleared hypotheses: hxy
-- 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 ι
a b_1 : E
hxy : fract b a = fract b b_1
⊢ Eq (α := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⟦a⟧ ⟦b_1⟧
have refine_2 : ((span ℤ (Set.range (⇑b : (a : ι) → E))).quotientRel : E → E → Prop) a b_1
Tactic: apply Quotient.sound'
-- 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 ι
a b_1 : E
hxy : fract b a = fract b b_1
⊢ ((span ℤ (Set.range (⇑b : (a : ι) → E))).quotientRel : E → E → Prop) a b_1
have refine_2 : Membership.mem (γ := AddSubgroup E)
  (toAddSubgroup (module_M := AddCommGroup.toIntModule E)
    (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
  (-a + b_1)
Tactic: rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← 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 ι
a b_1 : E
hxy : fract b a = fract b b_1
refine_2 :
  Membership.mem (γ := AddSubgroup E)
    (toAddSubgroup (module_M := AddCommGroup.toIntModule E)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (-a + b_1)
⊢ ((span ℤ (Set.range (⇑b : (a : ι) → E))).quotientRel : E → E → Prop) a b_1
have refine_2₁ : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-a + b_1)
Tactic: rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← 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 ι
x : (↑(fundamentalDomain b) : Type u_1)
⊢ ∃ (a : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Quotient.liftOn a (fractRestrict b) ⋯ = x
have refine_3 : ∀ (a : E),
  ∃ (a_1 : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn a_1 (fractRestrict b) sorry) (fractRestrict b a)
Tactic: obtain ⟨a, rfl⟩ := fractRestrict_surjective b x
Cleared hypotheses: 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
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x : (↑(fundamentalDomain b) : Type u_1)
⊢ Eq (α := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ((Equiv.symm (quotientEquiv b) :
          (a : (↑(fundamentalDomain b) : Type u_1)) → E ⧸ span ℤ (Set.range (⇑b : (a : ι) → E)))
        x :
      HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (Submodule.Quotient.mk (↑x : E) :
      HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
have rw : (↑x : E) = fract b (↑x : E)
Tactic: rw [Equiv.symm_apply_eq, quotientEquiv_apply_mk b ↑x, Subtype.ext_iff, fractRestrict_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
⊢ DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
have intro : ∀ (val : Fintype ι), DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
⊢ DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
have intro : Eq (α := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
  (Subtype.val (p := fun (x : ι → ℝ) ↦
      Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
        x) ⁻¹'
    Metric.ball 0 1)
  {0}
Tactic: refine discreteTopology_iff_isOpen_singleton_zero.mpr ⟨Metric.ball 0 1, Metric.isOpen_ball, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
⊢ Eq (α := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
    (Subtype.val (p := fun (x : ι → ℝ) ↦
        Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
          x) ⁻¹'
      Metric.ball 0 1)
    {0}
have intro : ∀ (x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))),
  Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
      (Subtype.val (p := fun (x : ι → ℝ) ↦
          Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
            x) ⁻¹'
        Metric.ball 0 1)
      x ↔
    Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))) {0} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
      (Subtype.val (p := fun (x : ι → ℝ) ↦
          Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
            x) ⁻¹'
        Metric.ball 0 1)
      x ↔
    Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))) {0} x
have intro : (∀ (i : ι), ‖(↑x : ι → ℝ) i‖ < 1) ↔ x = 0
Tactic: rw [Set.mem_preimage, mem_ball_zero_iff, pi_norm_lt_iff zero_lt_one, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ (∀ (i : ι), ‖(↑x : ι → ℝ) i‖ < 1) ↔ x = 0
have intro : (∀ (i : ι), |(↑x : ι → ℝ) i| < 1) ↔ ∀ (x_1 : ι), (↑x : ι → ℝ) x_1 = 0
Tactic: simp_rw [← coe_eq_zero, funext_iff, Pi.zero_apply, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ (∀ (i : ι), |(↑x : ι → ℝ) i| < 1) ↔ ∀ (x_1 : ι), (↑x : ι → ℝ) x_1 = 0
have intro : ∀ (i : ι), |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
Tactic: refine forall_congr' (fun i => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro : ∀ (y : ℤ) (hy : (↑y : ℝ) = (↑x : ι → ℝ) i), |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
Tactic: rsuffices ⟨y, hy⟩ : ∃ (y : ℤ), (y : ℝ) = (x : ι → ℝ) i
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
intro : ∀ (y : ℤ) (hy : (↑y : ℝ) = (↑x : ι → ℝ) i), |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have rsuffices : ∃ (y : ℤ), (↑y : ℝ) = (↑x : ι → ℝ) i
Tactic: rsuffices ⟨y, hy⟩ : ∃ (y : ℤ), (y : ℝ) = (x : ι → ℝ) i
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
Tactic: rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro₁ : LT.lt (α := ℝ) (↑|y| : ℝ) 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
Tactic: rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₁ : LT.lt (α := ℝ) (↑|y| : ℝ) 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro₂ : LT.lt (α := ℝ) (↑|y| : ℝ) (↑1 : ℝ) ↔ Eq (α := ℝ) (↑y : ℝ) 0
Tactic: rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₁ : LT.lt (α := ℝ) (↑|y| : ℝ) 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₂ : LT.lt (α := ℝ) (↑|y| : ℝ) (↑1 : ℝ) ↔ Eq (α := ℝ) (↑y : ℝ) 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro₃ : |y| < 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
Tactic: rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₁ : LT.lt (α := ℝ) (↑|y| : ℝ) 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₂ : LT.lt (α := ℝ) (↑|y| : ℝ) (↑1 : ℝ) ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₃ : |y| < 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro₄ : y = 0 ↔ Eq (α := ℝ) (↑y : ℝ) 0
Tactic: rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₁ : LT.lt (α := ℝ) (↑|y| : ℝ) 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₂ : LT.lt (α := ℝ) (↑|y| : ℝ) (↑1 : ℝ) ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₃ : |y| < 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₄ : y = 0 ↔ Eq (α := ℝ) (↑y : ℝ) 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
have intro₅ : y = 0 ↔ y = 0
Tactic: rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
⊢ fundamentalDomain b ⊆ parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have rw : ∀ (a : E),
  (∀ (i : ι),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
        ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)) →
    ∀ (i : ι),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1)
        ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)
Tactic: rw [fundamentalDomain, parallelepiped_basis_eq, Set.setOf_subset_setOf]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
x : E
hx : x ∈ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
⊢ Membership.mem (α := ι → ℝ) (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
    ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ)
have rwa : ∀ (hx : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x),
  Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
    (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ)
Tactic: rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
x : E
hx : x ∈ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
rwa :
  ∀ (hx : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x),
    Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ)
⊢ Membership.mem (α := ι → ℝ) (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
    ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ)
have rwa₁ : ∀
  (hx :
    ∀ (i : ι),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ))
  (i : ι),
  Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
    ((((Basis.repr (Pi.basisFun ℝ ι) : (a : ι → ℝ) → ι →₀ ℝ) ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ) : ι →₀ ℝ) :
          (a : ι) → ℝ)
        i :
      ℝ)
Tactic: rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
⊢ DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
have h : Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
Tactic: have h : Set.MapsTo b.equivFun (span ℤ (Set.range b)) (span ℤ (Set.range (Pi.basisFun ℝ ι))) := by
    intro _ hx
    rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
have convert_1 : DiscreteTopology.{u_2}
  (↑(↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) : Type u_2)
Tactic: convert! DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
convert_1 :
  DiscreteTopology.{u_2}
    (↑(↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) : Type u_2)
⊢ DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
have convert_2 : Function.Injective
  (Set.MapsTo.restrict (⇑b.equivFun : (a : E) → ι → ℝ)
    (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) h)
Tactic: convert! DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
⊢ (s ∩ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)).Finite
have this : DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
Tactic: have : DiscreteTopology (span ℤ (Set.range b)) := inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
⊢ (s ∩ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)).Finite
have refine : IsClosed (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
Tactic: refine Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete hs ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
⊢ MeasurableSet (fundamentalDomain b)
have intro : ∀ (val : Fintype ι), MeasurableSet (fundamentalDomain b)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
⊢ MeasurableSet (fundamentalDomain b)
have this : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
⊢ MeasurableSet (fundamentalDomain b)
have intro : MeasurableSet.{u_1} (α := E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D)
Tactic: rw [(_ : fundamentalDomain b = b.equivFun.toLinearMap ⁻¹' D)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
intro : MeasurableSet.{u_1} (α := E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D)
⊢ MeasurableSet (fundamentalDomain b)
have rw : fundamentalDomain b = (⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D
Tactic: rw [(_ : fundamentalDomain b = b.equivFun.toLinearMap ⁻¹' D)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
⊢ MeasurableSet.{u_1} (α := E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D)
have intro : MeasurableSet D
Tactic: refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional _).measurable ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
⊢ fundamentalDomain b = (⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D
have h : ∀ (x : E),
  x ∈ fundamentalDomain b ↔ Membership.mem (γ := Set E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D) x
Tactic: ext