-- Mathlib/NumberTheory/SiegelsLemma.lean
theorem exists_ne_zero_int_vec_norm_le
    (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) : ∃ t : β → ℤ, t ≠ 0 ∧
    A *ᵥ t = 0 ∧ ‖t‖ ≤ (n * max 1 ‖A‖) ^ ((m : ℝ) / (n - m))

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ ‖col Unit (x - y) i j‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Tactic:
simp only [col_apply, Pi.sub_apply]

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ ‖x i - y i‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ |x i - y i| ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
rw [abs_le]

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i ∧
    x i - y i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ ‖x - y‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

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

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
⊢ ∀ (i : β) (j : Unit), ‖col Unit (x - y) i j‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Proof state:
case intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : 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 * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i

Tactic:
simp only [neg_le_sub_iff_le_add]

Result:
case intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : 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 * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ y i ≤ x i + ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i ∧
    x i - y i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
rw [Finset.mem_Icc] at hxT hyT

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : 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 * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i ∧
    x i - y i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Tactic:
refine ⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ ‖x - y‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ ↑|x i - y i| ≤ ↑B

Tactic:
norm_cast

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ |x i - y i| ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ A *ᵥ (x - y) = 0

Tactic:
simp only [mulVec_sub, sub_eq_zero, hfeq]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : 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 * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i ∧
    x i - y i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
constructor

Result:
case intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : 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 * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ -↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ ≤ x i - y i

case intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : 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 * (1 ⊔ ‖A‖)) ^ e
i : β
j : Unit
⊢ x i - y i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ 0 ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Tactic:
positivity

Result:
no goals