awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have hd : d ≠ 0
Tactic: have hd : d ≠ 0 := by simp [d]
-- 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 > 0,
    ∃ B > 0,
      ∀ r < -(↑d : ℝ),
        ∀ (s : Finset ↥L),
          ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have refine : ∀ (r : ℝ) (hr : r < -(↑d : ℝ)) (u : Finset ↥L),
  ∑ z ∈ u, ‖z‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: refine ⟨2 * d * 3 ^ (d - 1), by positivity, ε, normBound_pos b, fun r hr u ↦ ?_⟩
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
u : Finset ↥L
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
⊢ ∑ z ∈ u, ‖z‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have obtain : ∀ (u : Finset (I → ℤ)),
  ∑ z ∈ Finset.image (⇑e.toAddEquiv.toEmbedding : (a : I → ℤ) → ↥L) u, ‖z‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: obtain ⟨u, rfl⟩ : ∃ u' : Finset _, u = u'.image e.toEmbedding :=
      ⟨u.image e.symm.toEmbedding, Finset.coe_injective
        (by simpa using (e.image_symm_image _).symm)⟩
Cleared hypotheses: u
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
⊢ ∑ z ∈ Finset.image (⇑e.toAddEquiv.toEmbedding : (a : I → ℤ) → ↥L) u, ‖z‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have dsimp : ∑ z ∈ Finset.image (⇑e : (a : I → ℤ) → ↥L) u, ‖(↑z : E)‖ ^ r ≤
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
    ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: dsimp
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
⊢ ∑ z ∈ Finset.image (⇑e : (a : I → ℤ) → ↥L) u, ‖(↑z : E)‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have simp : ∑ x ∈ u, norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) x) : E) ^ r ≤
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
    ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: simp only [EmbeddingLike.apply_eq_iff_eq, implies_true, Set.injOn_of_eq_iff_eq,
      Finset.sum_image, ge_iff_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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
⊢ ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
have obtain : ∀ (r : ℝ) (hr : 0 < r) (hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r),
  ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
Tactic: obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 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
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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
⊢ ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
have refine : ∀ (x : I → ℤ) (hx : x ∈ u),
  Membership.mem (γ := Finset (I → ℤ))
    (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑⌊r⌋.toNat : ℤ)) (↑⌊r⌋.toNat : ℤ)) x
Tactic: refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
-- 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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
⊢ max ⌊r⌋ 0 = ⌊r⌋
have rw : 0 ≤ ⌊r⌋
Tactic: rw [sup_eq_left]
-- 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
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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
⊢ Membership.mem (γ := Finset (I → ℤ))
    (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑⌊r⌋.toNat : ℤ)) (↑⌊r⌋.toNat : ℤ)) x
have hr'' : max ⌊r⌋ 0 = ⌊r⌋
Tactic: have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; positivity
-- 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
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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
hr'' : max ⌊r⌋ 0 = ⌊r⌋
⊢ Membership.mem (γ := Finset (I → ℤ))
    (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑⌊r⌋.toNat : ℤ)) (↑⌊r⌋.toNat : ℤ)) x
have this₁ : Membership.mem (γ := Set (I → ℤ)) (Metric.closedBall 0 r) x
Tactic: have := hr' hx
-- 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this_1 : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
hr'' : max ⌊r⌋ 0 = ⌊r⌋
this : Membership.mem (γ := Set (I → ℤ)) (Metric.closedBall 0 r) x
⊢ Membership.mem (γ := Finset (I → ℤ))
    (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑⌊r⌋.toNat : ℤ)) (↑⌊r⌋.toNat : ℤ)) x
have this₁ : ∀ (i : I), |x i| ≤ ⌊r⌋
Tactic: simp only [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg hr.le,
        Int.norm_eq_abs, ← Int.cast_abs, ← Int.le_floor] 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
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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
⊢ ∑ x ∈ u, norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) x) : E) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have obtain : ∀ (n : ℕ) (hn : u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)),
  ∑ x ∈ u, norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) x) : E) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, u ⊆ Fintype.piFinset fun _ : I ↦ Finset.Icc (-n : ℤ) n := by
      obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0
      refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
      have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; positivity
      have := hr' hx
      simp only [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg hr.le,
        Int.norm_eq_abs, ← Int.cast_abs, ← Int.le_floor] at this
      simpa only [Int.ofNat_toNat, Fintype.mem_piFinset, Finset.mem_Icc, ← abs_le, hr'']
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
⊢ ∑ x ∈ u, norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) x) : E) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have refine : ∑ i ∈ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ),
    norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) i) : E) ^ r ≤
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
    ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: refine (Finset.sum_le_sum_of_subset_of_nonneg hn (by intros; positivity)).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
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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
⊢ ∑ i ∈ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) i) : E) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have simp : ∑ x ∈ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ),
    norm (E := ↥L) ((e : (a : I → ℤ) → ↥L) x : ↥L) ^ r ≤
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
    ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: simp only [Submodule.norm_coe]
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
⊢ ∑ x ∈ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm (E := ↥L) ((e : (a : I → ℤ) → ↥L) x : ↥L) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have h : ∀ (x : I → ℤ),
  Membership.mem (γ := Finset (I → ℤ))
      (Fintype.piFinset (δ := fun (x : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)) x →
    Eq (α := ↥L) ((e : (a : I → ℤ) → ↥L) x : ↥L) (∑ i : I, HSMul.hSMul (β := ↥L) (x i) ((b : (a : I) → ↥L) i : ↥L) : ↥L)
Tactic: convert! sum_piFinset_Icc_rpow_le b rfl n r hr with x
-- 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 > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have inr : ∀ (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)),
  ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: obtain ⟨A, hA, B, hB, H⟩ : ∃ A > (0 : ℝ), ∃ B > (0 : ℝ), ∀ r < (-d : ℝ), ∀ s : Finset L,
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' k : ℕ, (k : ℝ) ^ (d - 1 + r) := by
    refine ⟨2 * d * 3 ^ (d - 1), by positivity, ε, normBound_pos b, fun r hr u ↦ ?_⟩
    let e : (I → ℤ) ≃ₗ[ℤ] L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite _ _ _).symm
    obtain ⟨u, rfl⟩ : ∃ u' : Finset _, u = u'.image e.toEmbedding :=
      ⟨u.image e.symm.toEmbedding, Finset.coe_injective
        (by simpa using (e.image_symm_image _).symm)⟩
    dsimp
    simp only [EmbeddingLike.apply_eq_iff_eq, implies_true, Set.injOn_of_eq_iff_eq,
      Finset.sum_image, ge_iff_le]
    obtain ⟨n, hn⟩ : ∃ n : ℕ, u ⊆ Fintype.piFinset fun _ : I ↦ Finset.Icc (-n : ℤ) n := by
      obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0
      refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
      have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; positivity
      have := hr' hx
      simp only [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg hr.le,
        Int.norm_eq_abs, ← Int.cast_abs, ← Int.le_floor] at this
      simpa only [Int.ofNat_toNat, Fintype.mem_piFinset, Finset.mem_Icc, ← abs_le, hr'']
    refine (Finset.sum_le_sum_of_subset_of_nonneg hn (by intros; positivity)).trans ?_
    dsimp
    simp only [Submodule.norm_coe]
    convert! sum_piFinset_Icc_rpow_le b rfl n r hr with x
    simp [e, Finsupp.linearCombination]
-- 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)
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have pos : ∀ (hA' : A ≤ 1),
  ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: by_cases hA' : A ≤ 1
-- 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)
pos :
  ∀ (hA' : A ≤ 1),
    ∃ A > 0,
      ∀ r < -(↑d : ℝ),
        ∀ (s : Finset ↥L),
          ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have neg : ∀ (hA' : ¬A ≤ 1),
  ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: by_cases hA' : A ≤ 1
-- 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
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have pos : ∀ (r : ℝ) (hr : r < -(↑d : ℝ)) (s : Finset ↥L),
  A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r) ≤
    B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: refine ⟨B, hB, fun r hr s ↦ (H r hr s).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
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) ≤
    B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have pos : A * (B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)) ≤
  B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: rw [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
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have neg : ∀ (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)
Tactic: refine ⟨A⁻¹ * B, mul_pos (inv_pos.mpr hA) hB, fun r hr s ↦ (H r hr s).trans ?_⟩