awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
⊢ ∀ (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

Premises used: Int.cast_abs, pi_norm_le_iff_of_nonneg, LT.lt.le, Int.norm_eq_abs, Int.le_floor, Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 : ∀ (i : I), |x i| ≤ ⌊r⌋
⊢ Membership.mem (γ := Finset (I → ℤ))
    (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑⌊r⌋.toNat : ℤ)) (↑⌊r⌋.toNat : ℤ)) x

Tactic:
simpa only [Int.ofNat_toNat, Fintype.mem_piFinset, Finset.mem_Icc, ← abs_le, hr'']

Premises used: Fintype.mem_piFinset, abs_le, Finset.mem_Icc, Int.ofNat_toNat
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 → ℤ)
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)
⊢ ∑ 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'']
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 : I → ℤ
h_1 :
  Membership.mem (γ := Finset (I → ℤ))
    (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)) i
h_2 : i ∉ u
⊢ 0 ≤ norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) i) : E) ^ r

Tactic:
positivity
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 : ℤ)
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)
⊢ ∑ 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:
refine (Finset.sum_le_sum_of_subset_of_nonneg hn (by intros; positivity)).trans ?_

Premises used: Finset.sum_le_sum_of_subset_of_nonneg, LE.le.trans
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 : ℤ)
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)
⊢ ∑ 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:
simp only [Submodule.norm_coe]

Premises used: Submodule.norm_coe
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 : ℤ)
⊢ ∑ p ∈ Fintype.piFinset (δ := fun (x : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := ↥L) (∑ i : I, HSMul.hSMul (β := ↥L) (p i) ((b : (a : I) → ↥L) i : ↥L)) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑(Fintype.card I) : ℝ) * HPow.hPow (α := ℝ) 3 (Fintype.card I - 1) * normBound b ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(Fintype.card I) : ℝ) 1 + r)

Tactic:
sum_piFinset_Icc_rpow_le b rfl n r hr

Premises used: ZLattice.sum_piFinset_Icc_rpow_le, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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_1 : 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 : ℤ)
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)
⊢ ∑ 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:
convert! sum_piFinset_Icc_rpow_le b rfl n r hr with x

Premises used: ZLattice.sum_piFinset_Icc_rpow_le, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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 : I → ℤ
h_1 :
  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:
simp [e, Finsupp.linearCombination]

Premises used: Finsupp.linearCombination
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
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)
⊢ ∃ 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]

Premises used: Nat.cast, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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)
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)
⊢ ∃ 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
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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)

Tactic:
⟨B, hB, fun r hr s ↦ (H r hr s).trans ?_⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
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)
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
refine ⟨B, hB, fun r hr s ↦ (H r hr s).trans ?_⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
pos :
  A * (B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)) ≤
    B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ 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]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
⊢ 0 ≤ B ^ r

Tactic:
positivity
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
⊢ LE.le (α := ℝ) 0 (∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))

Tactic:
positivity
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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)

Tactic:
exact mul_le_of_le_one_left (mul_nonneg (by positivity) (by positivity)) hA'

Premises used: mul_nonneg, mul_le_of_le_one_left
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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)

Tactic:
⟨A⁻¹ * B, mul_pos (inv_pos.mpr hA) hB, fun r hr s ↦ (H r hr s).trans ?_⟩

Premises used: Iff.mpr, HMul.hMul, inv_pos, mul_pos, Inv.inv, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
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)
⊢ ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ 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 ?_⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
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))
⊢ 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:
rw [Real.mul_rpow (inv_pos.mpr hA).le hB.le, mul_assoc, mul_assoc]

Premises used: Iff.mpr, mul_assoc, Real.mul_rpow, inv_pos, LT.lt.le
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
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
neg : A ≤ A⁻¹ ^ r
⊢ 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:
gcongr