awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
j : β
_ : Membership.mem (γ := Finset β) univ j → 0 ≤ (↑B : ℤ) * (A i j)⁺
⊢ Membership.mem (γ := Finset β) univ j → 0 ≤ (↑B : ℤ) * (A i j)⁺

Tactic:
_
-- 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 : α
calc : LE.le (α := ℤ) (N i) 0
calc₁ : 0 ≤ HAdd.hAdd (α := ℤ) (P i) 1
⊢ N i ≤ HAdd.hAdd (α := ℤ) (P i) 1

Tactic:
calc N i
  _ ≤ 0 := by
    apply Finset.sum_nonpos
    intro j _
    simp only [mul_neg, Left.neg_nonpos_iff]
    positivity
  _ ≤ P i + 1 := by
    apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))
    intro j _
    positivity
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
rw :
  Eq (α := ℤ) (∏ i : α, (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
    (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1))
⊢ Eq (α := ℤ) (↑(card.{u_1} (α := α → ℤ) S) : ℤ) (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1))

Tactic:
rw [Pi.card_Icc N P, Nat.cast_prod]

Premises used: Nat.cast_prod
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
e_f :
  Eq.{u_1 + 1} (α := α → ℤ)
    (fun (i : α) ↦ (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
    fun (i : α) ↦ HSub.hSub (α := ℤ) (P i) (N i) + 1
⊢ Eq (α := ℤ) (∏ i : α, (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
    (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1))

Tactic:
congr
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
e_f :
  ∀ (i : α),
    (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ) =
      HSub.hSub (α := ℤ) (P i) (N i) + 1
⊢ Eq.{u_1 + 1} (α := α → ℤ)
    (fun (i : α) ↦ (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
    fun (i : α) ↦ HSub.hSub (α := ℤ) (P i) (N i) + 1

Tactic:
ext i
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
i : α
e_f : HAdd.hAdd (α := ℤ) (P i) 1 - N i = HSub.hSub (α := ℤ) (P i) (N i) + 1
⊢ (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ) =
    HSub.hSub (α := ℤ) (P i) (N i) + 1

Tactic:
rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
i : α
⊢ HAdd.hAdd (α := ℤ) (P i) 1 - N i = HSub.hSub (α := ℤ) (P i) (N i) + 1

Tactic:
add_sub_right_comm (P i) 1 (N i)

Premises used: Norm.norm, HMul.hMul, Finset.univ, HSub.hSub, PosPart.posPart, Fintype.card, HDiv.hDiv, add_sub_right_comm, Nat.cast, HPow.hPow, Max.max, Nat.floor, OfNat.ofNat, Finset.sum, NegPart.negPart, Neg.neg
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
i : α
⊢ HAdd.hAdd (α := ℤ) (P i) 1 - N i = HSub.hSub (α := ℤ) (P i) (N i) + 1

Tactic:
exact add_sub_right_comm (P i) 1 (N i)
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
by_contra! : ∀ (h : ‖A‖ < 1), False
⊢ 1 ≤ ‖A‖

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
apply : A = 0
⊢ False

Tactic:
apply hA
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
a : ∀ (i : α) (j : β), A i j = 0 i j
⊢ A = 0

Tactic:
ext i j
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
a : ∀ (h : ∀ (i : α) (j : β), ‖A i j‖ < 1) (i : α) (j : β), A i j = 0
⊢ A i j = 0

Tactic:
rw [norm_lt_iff Real.zero_lt_one] at h

Premises used: Real.zero_lt_one, Matrix.norm_lt_iff
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ∀ (i : α) (j : β), ‖A i j‖ < 1
i : α
j : β
⊢ ‖A i j‖ < 1

Tactic:
specialize h i j
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : ‖A i j‖ < 1
⊢ LT.lt (α := ℝ) |(↑(A i j) : ℝ)| 1

Tactic:
rw [Int.norm_eq_abs] at h

Premises used: Int.norm_eq_abs
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : LT.lt (α := ℝ) |(↑(A i j) : ℝ)| 1
⊢ |A i j| < 1

Tactic:
norm_cast at h
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |A i j| < 1
⊢ A i j = 0

Tactic:
Int.abs_lt_one_iff.1 h

Premises used: Iff.mp, Int.abs_lt_one_iff
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |A i j| < 1
⊢ A i j = 0

Tactic:
exact Int.abs_lt_one_iff.1 h

Premises used: Iff.mp, Int.abs_lt_one_iff
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
zify : LT.lt (α := ℤ) (↑(card.{u_1} (α := α → ℤ) S) : ℤ) (↑(card.{u_2} (α := β → ℤ) T) : ℤ)
⊢ card.{u_1} (α := α → ℤ) S < card.{u_2} (α := β → ℤ) T

Tactic:
zify
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
rw : LT.lt (α := ℤ) (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1)) (↑((B + 1) ^ n) : ℤ)
⊢ LT.lt (α := ℤ) (↑(card.{u_1} (α := α → ℤ) S) : ℤ) (↑(card.{u_2} (α := β → ℤ) T) : ℤ)

Tactic:
rw [card_T_eq A, card_S_eq]

Premises used: _private.0.Int.Matrix.card_S_eq, _private.0.Int.Matrix.card_T_eq
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
rify :
  ∏ x : α,
      (HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A x x_1)⁺ : ℝ))
          (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A x x_1)⁻ : ℝ))) +
        1) <
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
⊢ LT.lt (α := ℤ) (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1)) (↑((B + 1) ^ n) : ℤ)

Tactic:
rify
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ LE.le (α := ℝ)
    (∏ x : α,
      (HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A x x_1)⁺ : ℝ))
          (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A x x_1)⁻ : ℝ))) +
        1))
    (∏ x : α, ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1))

Tactic:
Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)

Premises used: Finset.prod_le_prod
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
refine_1 :
  ∀ (i : α),
    Membership.mem (γ := Finset α) univ i →
      0 ≤
        HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
            (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
          1
refine_2 :
  ∀ (i : α),
    Membership.mem (γ := Finset α) univ i →
      HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
            (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
          1 ≤
        (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1
⊢ LE.le (α := ℝ)
    (∏ x : α,
      (HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A x x_1)⁺ : ℝ))
          (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A x x_1)⁻ : ℝ))) +
        1))
    (∏ x : α, ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1))

Tactic:
refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)

Premises used: Finset.prod_le_prod
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ N i ≤ HAdd.hAdd (α := ℤ) (P i) 1

Tactic:
have h := N_le_P_add_one A 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 β
hn : m < n
hm : 0 < m
i : α
h_1 : Membership.mem (γ := Finset α) univ i
h : N i ≤ HAdd.hAdd (α := ℤ) (P i) 1
⊢ ∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x)⁻ : ℝ)) ≤
    HAdd.hAdd (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁺ : ℝ)) 1

Tactic:
rify at h
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h_1 : Membership.mem (γ := Finset α) univ i
h :
  ∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x)⁻ : ℝ)) ≤
    HAdd.hAdd (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁺ : ℝ)) 1
linarith :
  HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
          (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
        1 <
      0 →
    HMul.hMul (α := ℝ) 1 (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ)) -
              HMul.hMul (α := ℝ) 1 (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
            HMul.hMul (α := ℝ) 1 1 -
          HMul.hMul (α := ℝ) 1 0 +
        (HMul.hMul (α := ℝ) 1 (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x)⁻ : ℝ))) -
          (HMul.hMul (α := ℝ) 1 (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁺ : ℝ)) + HMul.hMul (α := ℝ) 1 1)) =
      0
⊢ 0 ≤
    HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1

Tactic:
linarith only [h]
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
refine_2 :
  HAdd.hAdd (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
      (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁻ : ℝ)) ≤
    (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ)
⊢ HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1 ≤
    (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1

Tactic:
simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]

Premises used: add_le_add_iff_right, Finset.sum_neg_distrib, sub_neg_eq_add, 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 β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
simp : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = (↑n : ℝ) * (max 1 ‖A‖ * (↑B : ℝ))
⊢ (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = (↑n : ℝ) * (max 1 ‖A‖ * (↑B : ℝ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)

Tactic:
have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
refine_2 :
  LE.le (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑((A i x)⁺ + (A i x)⁻) : ℝ)) (∑ x : β, (↑B : ℝ) * max 1 ‖A‖)
⊢ HAdd.hAdd (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
      (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁻ : ℝ)) ≤
    (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ)

Tactic:
simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]

Premises used: Norm.norm, Finset.sum_add_distrib, Int.cast_add, Max.max, mul_comm, mul_add, 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 β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
refine_2 : ∀ (j : β), Membership.mem (γ := Finset β) univ j → (↑((A i j)⁺ + (A i j)⁻) : ℝ) ≤ max 1 ‖A‖
⊢ LE.le (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑((A i x)⁺ + (A i x)⁻) : ℝ)) (∑ x : β, (↑B : ℝ) * max 1 ‖A‖)

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 β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
j : β
h_1 : Membership.mem (γ := Finset β) univ j
refine_2 : |(↑(A i j) : ℝ)| ≤ max 1 ‖A‖
⊢ (↑((A i j)⁺ + (A i j)⁻) : ℝ) ≤ max 1 ‖A‖

Tactic:
rw [posPart_add_negPart (A i j), Int.cast_abs]

Premises used: Int.cast_abs, posPart_add_negPart
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
j : β
h_1 : Membership.mem (γ := Finset β) univ j
⊢ |(↑(A i j) : ℝ)| ≤ max 1 ‖A‖

Tactic:
le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)

Premises used: le_max_right, Matrix.norm_entry_le_entrywise_sup_norm, le_trans
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
j : β
h_1 : Membership.mem (γ := Finset β) univ j
⊢ |(↑(A i j) : ℝ)| ≤ max 1 ‖A‖

Tactic:
exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)

Premises used: le_max_right, Matrix.norm_entry_le_entrywise_sup_norm, le_trans
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ∏ x : α, ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) = ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m

Tactic:
simp
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
rw : ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + (↑n : ℝ) * max 1 ‖A‖) ^ m
⊢ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m

Tactic:
rw [← mul_pow, mul_add, mul_one]

Premises used: mul_add, mul_one, mul_pow
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
hab : 1 ≤ (↑n : ℝ) * max 1 ‖A‖
⊢ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + (↑n : ℝ) * max 1 ‖A‖) ^ m

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 β
hn : m < n
hm : 0 < m
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
H : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ 1 ≤ (↑n : ℝ) * max 1 ‖A‖

Tactic:
one_le_mul_of_one_le_of_one_le H <| le_max_left ..

Premises used: le_max_left, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
H : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ 1 ≤ (↑n : ℝ) * max 1 ‖A‖

Tactic:
exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..

Premises used: le_max_left, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
e_a : ((↑n : ℝ) * max 1 ‖A‖) ^ m = (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)
⊢ ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
e_a : HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≠ 0
⊢ ((↑n : ℝ) * max 1 ‖A‖) ^ m = (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)

Tactic:
rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
          ← Real.rpow_natCast, div_mul_cancel₀]

Premises used: div_mul_cancel₀, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≠ 0

Tactic:
sub_ne_zero_of_ne (mod_cast hn.ne')

Premises used: congrArg, cast, LT.lt.ne', sub_ne_zero_of_ne, Nat.cast_inj._simp_1, Eq.symm, Not
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≠ 0

Tactic:
exact sub_ne_zero_of_ne (mod_cast hn.ne')

Premises used: sub_ne_zero_of_ne
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
hbc : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)
hbc₁ : ((↑n : ℝ) * max 1 ‖A‖) ^ e < HAdd.hAdd (α := ℝ) (↑B : ℝ) 1
⊢ (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m <
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m

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 β
hn : m < n
hm : 0 < m
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)

Tactic:
sub_pos.mpr (mod_cast hn)

Premises used: Iff.mpr, sub_pos, Nat.cast_lt._simp_1, cast, Eq.symm
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)

Tactic:
exact sub_pos.mpr (mod_cast hn)

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ((↑n : ℝ) * max 1 ‖A‖) ^ e < HAdd.hAdd (α := ℝ) (↑B : ℝ) 1

Tactic:
Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)

Premises used: Norm.norm, HMul.hMul, HSub.hSub, Fintype.card, HDiv.hDiv, Nat.cast, HPow.hPow, Max.max, OfNat.ofNat, Nat.lt_floor_add_one
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ((↑n : ℝ) * max 1 ‖A‖) ^ e < HAdd.hAdd (α := ℝ) (↑B : ℝ) 1

Tactic:
exact Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
rw :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) *
      HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑m : ℝ) =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
rw₁ :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) = HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
rw₂ :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) =
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ)
rw₃ rw₄ :
  HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ) =
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n

Tactic:
rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]

Premises used: sub_add_cancel, Real.rpow_natCast