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 α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
x :
  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))
x₁ : ∏ x : α, ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) = ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m
x₂ : ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m
x₃ :
  ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m
x₄ :
  (((↑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
x₅ :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
⊢ ∏ 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

Tactic:
calc
  ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1)
    ≤ ∏ x : α, (n * max 1 ‖A‖ * B + 1) := by
      refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
      · have h := N_le_P_add_one A i
        rify at h
        linarith only [h]
      · simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]
        have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
        gcongr with j _
        rw [posPart_add_negPart (A i j), Int.cast_abs]
        exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)
  _ = (n * max 1 ‖A‖ * B + 1) ^ m := by simp
  _ ≤ (n * max 1 ‖A‖) ^ m * (B + 1) ^ m := by
        rw [← mul_pow, mul_add, mul_one]
        gcongr
        have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
        exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..
  _ = ((n * max 1 ‖A‖) ^ (m / ((n : ℝ) - m))) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
        congr 1
        rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
          ← Real.rpow_natCast, div_mul_cancel₀]
        exact sub_ne_zero_of_ne (mod_cast hn.ne')
  _ < (B + 1) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
        gcongr
        · exact sub_pos.mpr (mod_cast hn)
        · exact Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)
  _ = (B + 1) ^ n := by
        rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]

Premises used: HMul.hMul, Finset.univ, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Finset.sum, Neg.neg
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
rcases :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y),
    ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
rcases Finset.exists_ne_map_eq_of_card_lt_of_maps_to
    (card_S_lt_card_T A hn hm) (image_T_subset_S A)
    with ⟨x, hxT, y, hyT, hneq, hfeq⟩

Premises used: Finset.exists_ne_map_eq_of_card_lt_of_maps_to, _private.0.Int.Matrix.image_T_subset_S, _private.0.Int.Matrix.card_S_lt_card_T
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ A *ᵥ (x - y) = 0

Tactic:
simp only [mulVec_sub, sub_eq_zero, hfeq]

Premises used: sub_eq_zero, Matrix.mulVec_sub
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
refine : ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
refine ⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
positivity
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rw : ∀ (i : β) (j : Unit), ‖replicateCol Unit (x - y) i j‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]

Premises used: Matrix.norm_le_iff, Matrix.norm_replicateCol
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
simp : ‖x i - y i‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ‖replicateCol Unit (x - y) i j‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
simp only [replicateCol_apply, Pi.sub_apply]

Premises used: Matrix.replicateCol_apply, Pi.sub_apply
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
rw : (↑|x i - y i| : ℝ) ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ ‖x i - y i‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
rw [Int.norm_eq_abs, ← Int.cast_abs]

Premises used: Int.cast_abs, Int.norm_eq_abs
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ (↑|x i - y i| : ℝ) ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)

Premises used: Nat.floor_le, le_trans
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
refine : LE.le (α := ℝ) (↑|x i - y i| : ℝ) (↑B : ℝ)
⊢ (↑|x i - y i| : ℝ) ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
refine le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)

Premises used: Nat.floor_le, le_trans
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
norm_cast :
  |x i - y i| ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ LE.le (α := ℝ) (↑|x i - y i| : ℝ) (↑B : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
rw :
  -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i ∧
    x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ |x i - y i| ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
rw [abs_le]

Premises used: abs_le
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : Membership.mem (γ := Finset (β → ℤ)) T x
y : β → ℤ
hyT : Membership.mem (γ := Finset (β → ℤ)) T y
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
rw :
  ∀ (hxT : 0 ≤ x ∧ x ≤ B') (y : β → ℤ) (hyT : 0 ≤ y ∧ y ≤ B') (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y)
    (n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e) (i : β) (j : Unit),
    -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i ∧
      x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i ∧
    x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
rw [Finset.mem_Icc] at hxT hyT

Premises used: Finset.mem_Icc
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
left : -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i
right : x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i ∧
    x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
left : y i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i

Tactic:
simp only [neg_le_sub_iff_le_add]

Premises used: neg_le_sub_iff_le_add
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
left : B' i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ y i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
apply le_trans (hyT.2 i)

Premises used: And.right, le_trans
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
left :
  (fun (x : β) ↦ ((↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) : ℤ))
      i ≤
    x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ B' i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
left : 0 ≤ x i
⊢ (fun (x : β) ↦ ((↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) : ℤ))
      i ≤
    x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
simp only [le_add_iff_nonneg_left]

Premises used: le_add_iff_nonneg_left
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ 0 ≤ x i

Tactic:
hxT.1 i

Premises used: And.left
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ 0 ≤ x i

Tactic:
exact hxT.1 i

Premises used: And.left
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
right : x i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
⊢ x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)

Tactic:
simp only [tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
right : B' i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
⊢ x i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i

Tactic:
apply le_trans (hxT.2 i)

Premises used: And.right, le_trans
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
right :
  (fun (x : β) ↦ ((↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) : ℤ))
      i ≤
    (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
⊢ B' i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
right : 0 ≤ y i
⊢ (fun (x : β) ↦ ((↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) : ℤ))
      i ≤
    (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i

Tactic:
simp only [le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ 0 ≤ y i

Tactic:
hyT.1 i

Premises used: And.left
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ 0 ≤ y i

Tactic:
exact hyT.1 i

Premises used: And.left
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
have := exists_ne_zero_int_vec_norm_le A hn hm
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rwa : 1 ≤ ‖A‖
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * ‖A‖) ^ e

Tactic:
rwa [max_eq_right] at this

Premises used: max_eq_right
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ 1 ≤ ‖A‖

Tactic:
Int.Matrix.one_le_norm_A_of_ne_zero _ hA

Premises used: Int.Matrix.one_le_norm_A_of_ne_zero
-- Module: Mathlib.NumberTheory.SiegelsLemma
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
hA : A ≠ 0
this : ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
⊢ 1 ≤ ‖A‖

Tactic:
exact Int.Matrix.one_le_norm_A_of_ne_zero _ hA

Premises used: Int.Matrix.one_le_norm_A_of_ne_zero
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Nat.factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h : m ∈ factoredNumbers s
h' : k ∣ m
⊢ m ≠ 0

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h : m ∈ factoredNumbers s
h' : k ∣ m
h₁ : m ≠ 0
⊢ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ k ≠ 0

Tactic:
have hk := ne_zero_of_dvd_ne_zero h₁ h'
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
⊢ k ∈ factoredNumbers s

Tactic:
⟨hk, fun p hp ↦ h₂ p ?_⟩

Premises used: Set.Mem, setOf, Nat.factoredNumbers, And.intro
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
refine : ∀ (p : ℕ) (hp : p ∈ k.primeFactorsList), p ∈ m.primeFactorsList
⊢ k ∈ factoredNumbers s

Tactic:
refine ⟨hk, fun p hp ↦ h₂ p ?_⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : p ∈ k.primeFactorsList
⊢ k ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ m ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : p ∈ k.primeFactorsList
rw : ∀ (hp : Prime p ∧ p ∣ k), Prime p ∧ p ∣ m
⊢ p ∈ m.primeFactorsList

Tactic:
rw [mem_primeFactorsList <| by assumption] at hp ⊢

Premises used: Nat.mem_primeFactorsList
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ Prime p ∧ p ∣ m

Tactic:
⟨hp.1, hp.2.trans h'⟩

Premises used: And.right, And.left, And.intro, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ Prime p ∧ p ∣ m

Tactic:
exact ⟨hp.1, hp.2.trans h'⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
simp_rw : (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
simp_rw [mem_factoredNumbers, mem_primeFactorsList']

Premises used: Nat.mem_primeFactorsList', Nat.mem_factoredNumbers
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
⟨fun ⟨H₀, H₁⟩ ↦ ⟨H₀, fun p _ hp₂ hp₃ ↦ H₁ p ⟨hp₂, hp₃, H₀⟩⟩,
    fun ⟨H₀, H₁⟩ ↦
      ⟨H₀, fun p ⟨hp₁, hp₂, hp₃⟩ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero hp₃) hp₂) hp₁ hp₂⟩⟩

Premises used: _private.0.Nat.mem_factoredNumbers_iff_forall_le.match_3, Membership.mem, _private.0.Nat.mem_factoredNumbers_iff_forall_le.match_4, Ne, And, Nat.pos_of_ne_zero, And.intro, Iff.intro, _private.0.Nat.mem_factoredNumbers_iff_forall_le.match_2, OfNat.ofNat, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
exact ⟨fun ⟨H₀, H₁⟩ ↦ ⟨H₀, fun p _ hp₂ hp₃ ↦ H₁ p ⟨hp₂, hp₃, H₀⟩⟩,
    fun ⟨H₀, H₁⟩ ↦
      ⟨H₀, fun p ⟨hp₁, hp₂, hp₃⟩ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero hp₃) hp₂) hp₁ hp₂⟩⟩
-- Module: Mathlib.NumberTheory.SmoothNumbers
Goal:
s : Finset ℕ
m : ℕ
obtain : ∀ (p : ℕ) (hp₁ : 1 + s.sup id ≤ p) (hp₂ : Prime p), m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := exists_infinite_primes (1 + Finset.sup s id)

Premises used: id, HAdd.hAdd, Finset.sup, OfNat.ofNat, Nat.exists_infinite_primes