awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
h_1 : n ∈ s.support
⊢ LE.le (α := ℝ) (if s.prodPrimes.gcd n = 1 then 1 else 0) (∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)

Tactic:
exact hμ (Nat.gcd s.prodPrimes n)

Premises used: Nat.gcd, BoundingSieve.prodPrimes
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d

Tactic:
case caseA =>
    rw [siftedSum_eq_sum_support_mul_ite]
    gcongr with n
    exact hμ (Nat.gcd s.prodPrimes n)

Premises used: BoundingSieve.siftedSum_eq_sum_support_mul_ite
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
simp_rw :
  Eq (α := ℝ) (∑ x ∈ s.support, ∑ i ∈ (s.prodPrimes.gcd x).divisors, s.weights x * muPlus i)
    (∑ x ∈ s.support, ∑ a ∈ s.prodPrimes.divisors with a ∣ x, s.weights x * muPlus a)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
    (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)

Tactic:
simp_rw [mul_sum, ← sum_filter]

Premises used: Finset.mul_sum, Finset.sum_filter
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
e_f :
  ∀ (n : ℕ),
    Eq (α := ℝ) (∑ i ∈ (s.prodPrimes.gcd n).divisors, s.weights n * muPlus i)
      (∑ a ∈ s.prodPrimes.divisors with a ∣ n, s.weights n * muPlus a)
⊢ Eq (α := ℝ) (∑ x ∈ s.support, ∑ i ∈ (s.prodPrimes.gcd x).divisors, s.weights x * muPlus i)
    (∑ x ∈ s.support, ∑ a ∈ s.prodPrimes.divisors with a ∣ x, s.weights x * muPlus a)

Tactic:
congr with n
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
e_f : (s.prodPrimes.gcd n).divisors = {a ∈ s.prodPrimes.divisors | a ∣ n}
⊢ Eq (α := ℝ) (∑ i ∈ (s.prodPrimes.gcd n).divisors, s.weights n * muPlus i)
    (∑ a ∈ s.prodPrimes.divisors with a ∣ n, s.weights n * muPlus a)

Tactic:
congr
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
e_f : {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} = {a ∈ s.prodPrimes.divisors | a ∣ n}
⊢ (s.prodPrimes.gcd n).divisors = {a ∈ s.prodPrimes.divisors | a ∣ n}

Tactic:
rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]

Premises used: Nat.gcd_dvd_left, BoundingSieve.prodPrimes_ne_zero, Nat.divisors_filter_dvd_of_dvd
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
e_f : ∀ (x : ℕ), x ∈ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} ↔ x ∈ {a ∈ s.prodPrimes.divisors | a ∣ n}
⊢ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} = {a ∈ s.prodPrimes.divisors | a ∣ n}

Tactic:
ext x
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n x : ℕ
⊢ x ∈ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} ↔ x ∈ {a ∈ s.prodPrimes.divisors | a ∣ n}

Tactic:
simp +contextual [dvd_gcd_iff]

Premises used: Nat.dvd_gcd_iff
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
    (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)

Tactic:
case caseB =>
    simp_rw [mul_sum, ← sum_filter]
    congr with n
    congr
    · rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]
      ext x; simp +contextual [dvd_gcd_iff]

Premises used: Nat.dvd_gcd_iff, Nat.gcd_dvd_left, Finset.mul_sum, BoundingSieve.prodPrimes_ne_zero, Nat.divisors_filter_dvd_of_dvd, Finset.sum_filter
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
rw :
  Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)

Tactic:
rw [sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
simp_rw :
  Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ n ∈ s.support, if x ∣ n then s.weights n else 0)
simp_rw₁ :
  Eq (α := ℝ) (∑ x ∈ s.prodPrimes.divisors, ∑ a ∈ s.support with x ∣ a, s.weights a * muPlus x)
    (∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ a ∈ s.support with x ∣ a, s.weights a)
simp_rw₂ :
  Eq (α := ℝ) (∑ x ∈ s.prodPrimes.divisors, ∑ a ∈ s.support with x ∣ a, s.weights a * muPlus x)
    (∑ x ∈ s.prodPrimes.divisors, ∑ i ∈ s.support with x ∣ i, muPlus x * s.weights i)
⊢ Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)

Tactic:
simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]

Premises used: Finset.mul_sum, BoundingSieve.multSum, mul_comm, Finset.sum_filter
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
case case₁ case₂ :
  Eq (α := ℝ) (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)

Tactic:
case caseC =>
    rw [sum_comm]
    simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]

Premises used: Finset.mul_sum, BoundingSieve.multSum, mul_comm, Finset.sum_comm, Finset.sum_filter
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
rw :
  Eq (α := ℝ) (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
    (∑ x ∈ s.prodPrimes.divisors,
      (s.totalMass * HMul.hMul (β := ℝ) (muPlus x) ((s.nu : (a : ℕ) → ℝ) x : ℝ) + muPlus x * rem (s := s) x))
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d =
    s.totalMass * mainSum (s := s) muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem (s := s) d

Tactic:
rw [mainSum, mul_sum, ← sum_add_distrib]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, BoundingSieve.mainSum
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
e_f :
  ∀ (d : ℕ),
    muPlus d * multSum (s := s) d =
      s.totalMass * HMul.hMul (β := ℝ) (muPlus d) ((s.nu : (a : ℕ) → ℝ) d : ℝ) + muPlus d * rem (s := s) d
⊢ Eq (α := ℝ) (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
    (∑ x ∈ s.prodPrimes.divisors,
      (s.totalMass * HMul.hMul (β := ℝ) (muPlus x) ((s.nu : (a : ℕ) → ℝ) x : ℝ) + muPlus x * rem (s := s) x))

Tactic:
congr with d
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
⊢ muPlus d * multSum (s := s) d =
    s.totalMass * HMul.hMul (β := ℝ) (muPlus d) ((s.nu : (a : ℕ) → ℝ) d : ℝ) +
      muPlus d * (multSum (s := s) d - HMul.hMul (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) s.totalMass)

Tactic:
ring
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
bc : ∀ d ∈ s.prodPrimes.divisors, muPlus d * rem (s := s) d ≤ |muPlus d| * |rem (s := s) d|
⊢ s.totalMass * mainSum (s := s) muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem (s := s) d ≤
    s.totalMass * mainSum (s := s) muPlus + ∑ d ∈ s.prodPrimes.divisors, |muPlus d| * |rem (s := s) d|

Tactic:
gcongr _ + ∑ d ∈ _, ?_ with d
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
h_1 : d ∈ s.prodPrimes.divisors
bc : muPlus d * rem (s := s) d ≤ |muPlus d * rem (s := s) d|
⊢ muPlus d * rem (s := s) d ≤ |muPlus d| * |rem (s := s) d|

Tactic:
rw [← abs_mul]

Premises used: abs_mul
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
h_1 : d ∈ s.prodPrimes.divisors
⊢ muPlus d * rem (s := s) d ≤ |muPlus d * rem (s := s) d|

Tactic:
le_abs_self (muPlus d * s.rem d)

Premises used: le_abs_self, HMul.hMul, BoundingSieve.rem
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
d : ℕ
h_1 : d ∈ s.prodPrimes.divisors
⊢ muPlus d * rem (s := s) d ≤ |muPlus d * rem (s := s) d|

Tactic:
exact le_abs_self (muPlus d * s.rem d)

Premises used: le_abs_self, HMul.hMul, BoundingSieve.rem
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : Membership.mem (γ := Finset (β → ℤ)) T v
rw : ∀ (hv : 0 ≤ v ∧ v ≤ B'), N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P
⊢ Membership.mem (γ := Finset (α → ℤ)) S (A *ᵥ v)

Tactic:
rw [mem_Icc] at hv ⊢

Premises used: Finset.mem_Icc
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
⊢ A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j

Tactic:
have mulVec_def : A.mulVec v =
      fun i ↦ Finset.sum univ fun j : β ↦ A i j * v j := rfl
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
rw :
  (LE.le.{u_1} (α := α → ℤ) N fun (i : α) ↦ ∑ j : β, A i j * v j) ∧
    LE.le.{u_1} (α := α → ℤ) (fun (i : α) ↦ ∑ j : β, A i j * v j) P
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P

Tactic:
rw [mulVec_def]
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
⊢ (LE.le.{u_1} (α := α → ℤ) N fun (i : α) ↦ ∑ j : β, A i j * v j) ∧
    LE.le.{u_1} (α := α → ℤ) (fun (i : α) ↦ ∑ j : β, A i j * v j) P

Tactic:
⟨fun i ↦ ?_, fun i ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
refine_1 : ∀ (i : α), LE.le (α := (fun (i : α) ↦ ℤ) i) (N i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i)
refine_2 : ∀ (i : α), LE.le (α := (fun (i : α) ↦ ℤ) i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i) (P i)
⊢ (LE.le.{u_1} (α := α → ℤ) N fun (i : α) ↦ ∑ j : β, A i j * v j) ∧
    LE.le.{u_1} (α := α → ℤ) (fun (i : α) ↦ ∑ j : β, A i j * v j) P

Tactic:
refine ⟨fun i ↦ ?_, fun i ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
refine_1 : LE.le (α := ℤ) (∑ x : β, -((↑B : ℤ) * (A i x)⁻)) (∑ j : β, A i j * v j)
⊢ LE.le (α := (fun (i : α) ↦ ℤ) i) (N i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i)

Tactic:
simp only [mul_neg]

Premises used: mul_neg
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
refine_1 : ∀ (j : β), Membership.mem (γ := Finset β) univ j → -((↑B : ℤ) * (A i j)⁻) ≤ A i j * v j
⊢ LE.le (α := ℤ) (∑ x : β, -((↑B : ℤ) * (A i x)⁻)) (∑ j : β, A i j * v j)

Tactic:
gcongr ∑ _ : β, ?_ with j _
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
refine_1 : -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ A i j * v j

Tactic:
rw [← mul_comm (v j)]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
refine_1 : ∀ (hsign : 0 ≤ A i j), -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
refine_1₁ : ∀ (hsign : A i j ≤ 0), -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j

Tactic:
rcases le_total 0 (A i j) with hsign | hsign

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
refine_2 : ∀ (j : β), Membership.mem (γ := Finset β) univ j → A i j * v j ≤ (↑B : ℤ) * (A i j)⁺
⊢ LE.le (α := ℤ) (∑ j : β, A i j * v j) (∑ j : β, (↑B : ℤ) * (A i j)⁺)

Tactic:
gcongr ∑ _ : β, ?_ with j _
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
refine_2 : v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
⊢ A i j * v j ≤ (↑B : ℤ) * (A i j)⁺

Tactic:
rw [← mul_comm (v j)]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
refine_2 : ∀ (hsign : 0 ≤ A i j), v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
refine_2₁ : ∀ (hsign : A i j ≤ 0), v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺

Tactic:
rcases le_total 0 (A i j) with hsign | hsign

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
refine_1 : -HMul.hMul (α := ℤ) (↑B : ℤ) 0 ≤ v j * A i j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j

Tactic:
rw [negPart_eq_zero.2 hsign]

Premises used: Iff.mpr, negPart_eq_zero
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
⊢ -HMul.hMul (α := ℤ) (↑B : ℤ) 0 ≤ v j * A i j

Tactic:
mul_nonneg (hv.1 j) hsign

Premises used: mul_nonneg, And.left, Int.neg, Int.negOfNat
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
⊢ -HMul.hMul (α := ℤ) (↑B : ℤ) 0 ≤ v j * A i j

Tactic:
exact mul_nonneg (hv.1 j) hsign

Premises used: mul_nonneg, And.left
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
refine_1 : -((↑B : ℤ) * -A i j) ≤ v j * A i j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j

Tactic:
rw [negPart_eq_neg.2 hsign]

Premises used: Iff.mpr, negPart_eq_neg
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
refine_1 : (↑B : ℤ) * A i j ≤ v j * A i j
⊢ -((↑B : ℤ) * -A i j) ≤ v j * A i j

Tactic:
simp only [mul_neg, neg_neg]

Premises used: neg_neg, mul_neg
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ (↑B : ℤ) * A i j ≤ v j * A i j

Tactic:
mul_le_mul_of_nonpos_right (hv.2 j) hsign

Premises used: mul_le_mul_of_nonpos_right, And.right
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ (↑B : ℤ) * A i j ≤ v j * A i j

Tactic:
exact mul_le_mul_of_nonpos_right (hv.2 j) hsign

Premises used: mul_le_mul_of_nonpos_right, And.right
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
refine_2 : v j * A i j ≤ (↑B : ℤ) * A i j
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺

Tactic:
rw [posPart_eq_self.2 hsign]

Premises used: Iff.mpr, posPart_eq_self
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
refine_2 : v j ≤ (↑B : ℤ)
⊢ v j * A i j ≤ (↑B : ℤ) * A i j

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
⊢ v j ≤ (↑B : ℤ)

Tactic:
apply hv.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
refine_2 : v j * A i j ≤ HMul.hMul (α := ℤ) (↑B : ℤ) 0
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺

Tactic:
rw [posPart_eq_zero.2 hsign]

Premises used: Iff.mpr, posPart_eq_zero
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ v j * A i j ≤ HMul.hMul (α := ℤ) (↑B : ℤ) 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos (hv.1 j) hsign

Premises used: And.left, Int.mul, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ v j * A i j ≤ HMul.hMul (α := ℤ) (↑B : ℤ) 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos (hv.1 j) hsign

Premises used: And.left, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq β
rw : ∏ i : β, card (α := ℤ) (Icc (0 i) (↑B : ℤ)) = (B + 1) ^ n
⊢ card.{u_2} (α := β → ℤ) T = (B + 1) ^ n

Tactic:
rw [Pi.card_Icc 0 B']
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq β
⊢ ∏ i : β, card (α := ℤ) (Icc (0 i) (↑B : ℤ)) = (B + 1) ^ n

Tactic:
simp only [Pi.zero_apply, card_Icc, sub_zero, toNat_natCast_add_one, prod_const, card_univ]

Premises used: Finset.card_univ, Int.toNat_natCast_add_one, sub_zero, Pi.zero_apply, Finset.prod_const, Int.card_Icc
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
h : ∀ (i_1 : β), Membership.mem (γ := Finset β) univ i_1 → (↑B : ℤ) * -(A i i_1)⁻ ≤ 0
⊢ LE.le (α := ℤ) (N i) 0

Tactic:
apply Finset.sum_nonpos

Premises used: Finset.sum_nonpos
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
j : β
h : Membership.mem (γ := Finset β) univ j → (↑B : ℤ) * -(A i j)⁻ ≤ 0
⊢ Membership.mem (γ := Finset β) univ j → (↑B : ℤ) * -(A i j)⁻ ≤ 0

Tactic:
_
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
j : β
h_1 : Membership.mem (γ := Finset β) univ j
h : 0 ≤ (↑B : ℤ) * (A i j)⁻
⊢ (↑B : ℤ) * -(A i j)⁻ ≤ 0

Tactic:
simp only [mul_neg, Left.neg_nonpos_iff]

Premises used: Left.neg_nonpos_iff, mul_neg
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
⊢ 0 ≤ (↑B : ℤ) * (A i j)⁻

Tactic:
positivity
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
apply : ∀ (i_1 : β), Membership.mem (γ := Finset β) univ i_1 → 0 ≤ (↑B : ℤ) * (A i i_1)⁺
⊢ 0 ≤ HAdd.hAdd (α := ℤ) (P i) 1

Tactic:
apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))