awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r) ≤
    (A⁻¹ * B) ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have neg : A * (B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)) ≤
  A⁻¹ ^ r * (B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
Tactic: rw [Real.mul_rpow (inv_pos.mpr hA).le hB.le, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ A * (B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)) ≤
    A⁻¹ ^ r * (B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
have neg : A ≤ A⁻¹ ^ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ A ≤ A⁻¹ ^ r
have neg : A ≤ A ^ (-1 * r)
Tactic: rw [← Real.rpow_neg_one, ← Real.rpow_mul hA.le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ A ≤ A ^ (-1 * r)
have neg : 1 ≤ -1 * r
Tactic: refine Real.self_le_rpow_of_one_le (not_le.mp hA').le ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ 1 ≤ -1 * r
have neg : r ≤ -1
Tactic: simp only [neg_mul, one_mul, le_neg (b := r)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ r ≤ -1
have neg : LE.le (α := ℝ) (-(↑d : ℝ)) (-1)
Tactic: refine hr.le.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
have inl : Subsingleton.{u_1 + 1} ↥L → Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
Tactic: cases subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
inl : Subsingleton.{u_1 + 1} ↥L → Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
have inr : Nontrivial.{u_1} ↥L → Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
Tactic: cases subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
have inr : ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r
Tactic: refine Summable.of_norm_bounded_eventually
    (.mul_left ((1 / 2) ^ r) (summable_norm_rpow L r hr)) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
⊢ ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r
have H : IsClosed (↑L : Set E)
Tactic: have H : IsClosed (X := E) L := @AddSubgroup.isClosed_of_discrete _ _ _ _ _
    L.toAddSubgroup (inferInstanceAs (DiscreteTopology L))
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
⊢ ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r
have inr : Subset (α := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
  ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
    (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
Tactic: refine ((Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
    (Metric.isBounded_closedBall (x := (0 : E)) (r := 2 * ‖x‖)) H).preimage_embedding
    (.subtype _)).subset ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have pos : ∀ (ht₁ : ‖t‖ = 0),
  Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
Tactic: by_cases ht₁ : ‖t‖ = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
pos :
  ∀ (ht₁ : ‖t‖ = 0),
    Membership.mem (γ := Set ↥L)
      ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
        (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
      t
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have neg : ∀ (ht₁ : ¬‖t‖ = 0),
  Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
Tactic: by_cases ht₁ : ‖t‖ = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have pos : ∀ (ht₂ : ‖(↑t : E) - x‖ = 0),
  Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
Tactic: by_cases ht₂ : ‖t - x‖ = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
pos :
  ∀ (ht₂ : ‖(↑t : E) - x‖ = 0),
    Membership.mem (γ := Set ↥L)
      ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
        (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
      t
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have neg : ∀ (ht₂ : ¬‖(↑t : E) - x‖ = 0),
  Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
Tactic: by_cases ht₂ : ‖t - x‖ = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have this : 0 < finrank.{0, u_1} ℤ ↥L
Tactic: have : 0 < Module.finrank ℤ L := Module.finrank_pos
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
have rw : (2⁻¹ * ‖t‖) ^ r < ‖(↑t : E) - x‖ ^ r
Tactic: rw [← Real.rpow_lt_rpow_iff_of_neg (by positivity) (by positivity) (hr.trans (by simpa))]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have this₁ : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
Tactic: have : ‖t - x‖ < 2⁻¹ * ‖t‖ := by
    rw [← Real.rpow_lt_rpow_iff_of_neg (by positivity) (by positivity) (hr.trans (by simpa))]
    simpa [Real.mul_rpow, abs_eq_self.mpr (show 0 ≤ ‖t - x‖ ^ r by positivity)] using ht
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have this₁ : ‖(↑t : E)‖ - ‖x‖ < 2⁻¹ * ‖t‖
Tactic: have := (norm_sub_norm_le _ _).trans_lt this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - ‖x‖ < 2⁻¹ * ‖t‖
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t
have this₁ : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
Tactic: rw [sub_lt_iff_lt_add, ← sub_lt_iff_lt_add', AddSubgroupClass.coe_norm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
⊢ ‖(↑t : E)‖ ≤ 2 * ‖x‖
have linarith : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
linarith : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
⊢ ‖(↑t : E)‖ ≤ 2 * ‖x‖
have linarith₁ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
linarith : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
linarith₁ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖(↑t : E)‖ ≤ 2 * ‖x‖
have linarith₂ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
linarith : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
linarith₁ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 2 1 = 2
⊢ ‖(↑t : E)‖ ≤ 2 * ‖x‖
have linarith₃ : 2 * ‖x‖ < ‖(↑t : E)‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
linarith : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
linarith₁ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 * ‖x‖ < ‖(↑t : E)‖ → GT.gt (α := ℝ) 2 0
linarith₄ : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
linarith₅ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₇ : 2 * ‖x‖ < ‖(↑t : E)‖ → GT.gt (α := ℝ) 2 0
⊢ ‖(↑t : E)‖ ≤ 2 * ‖x‖
have linarith₈ : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 * ‖(↑t : E)‖ - HMul.hMul (α := ℝ) 1 1 * (1 * ‖(↑t : E)‖) - 2 * ‖x‖ + (2 * ‖x‖ - ‖(↑t : E)‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n + c / n * n) • x = c • x
⊢ (c % n) • x = c • x
have rwa : ∀ (this : (c % n) • x + (c / n * n) • x = c • x), (c % n) • x = c • x
Tactic: rwa [add_nsmul, mul_nsmul, h, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n + c / n * n) • x = c • x
rwa : ∀ (this : (c % n) • x + (c / n * n) • x = c • x), (c % n) • x = c • x
⊢ (c % n) • x = c • x
have rwa₁ : ∀ (this : (c % n) • x + n • (c / n) • x = c • x), (c % n) • x = c • x
Tactic: rwa [add_nsmul, mul_nsmul, h, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n + c / n * n) • x = c • x
rwa : ∀ (this : (c % n) • x + (c / n * n) • x = c • x), (c % n) • x = c • x
rwa₁ : ∀ (this : (c % n) • x + n • (c / n) • x = c • x), (c % n) • x = c • x
⊢ (c % n) • x = c • x
have rwa₂ : ∀ (this : (c % n) • x + 0 = c • x), (c % n) • x = c • x
Tactic: rwa [add_nsmul, mul_nsmul, h, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n + c / n * n) • x = c • x
rwa : ∀ (this : (c % n) • x + (c / n * n) • x = c • x), (c % n) • x = c • x
rwa₁ : ∀ (this : (c % n) • x + n • (c / n) • x = c • x), (c % n) • x = c • x
rwa₂ : ∀ (this : (c % n) • x + 0 = c • x), (c % n) • x = c • x
⊢ (c % n) • x = c • x
have rwa₃ : ∀ (this : (c % n) • x = c • x), (c % n) • x = c • x
Tactic: rwa [add_nsmul, mul_nsmul, h, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
⊢ (c % n) • x = c • x
have suffices : (c % n + c / n * n) • x = c • x
Tactic: suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
⊢ (c % n + c / n * n) • x = c • x
have rw : c • x = c • x
Tactic: rw [Nat.mod_add_div']
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (hypothesis)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
⊢ Module (ZMod n) M
have h_mod : ∀ (c : ℕ) (x : M), (c % n) • x = c • x
Tactic: have h_mod (c : ℕ) (x : M) : (c % n) • x = c • x := by
    suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this
    rw [Nat.mod_add_div']
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (hypothesis)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst : NeZero n
inst_1 : AddCommMonoid M
h : ∀ (x : M), n • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % n) • x = c • x
⊢ Module (ZMod n) M
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- Lean 4 proof step from Mathlib.Algebra.Module.ZMod (goal)
Goal:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst : AddCommGroup M
inst_1 : AddCommGroup M₁
inst_2 : FunLike F M M₁
inst_3 : AddMonoidHomClass F M M₁
inst_4 : Module (ZMod n) M
inst_5 : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ (f : (a : M) → M₁) (c • x) = HSMul.hSMul (β := M₁) c ((f : (a : M) → M₁) x : M₁)
have rw : (f : (a : M) → M₁) (HSMul.hSMul (α := ZMod n) (↑c.cast : ZMod n) x) =
  HSMul.hSMul (α := ZMod n) (β := M₁) (↑c.cast : ZMod n) ((f : (a : M) → M₁) x : M₁)
Tactic: rw [← ZMod.intCast_zmod_cast c]