-- 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
⊢ ‖x i - y i‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

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

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), ‖col Unit (x - y) i j‖ ≤ (↑n * (1 ⊔ ‖A‖)) ^ e

Tactic:
intro i j

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
α : 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

Tactic:
refine le_trans ?_ (Nat.floor_le 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
⊢ ↑|x i - y i| ≤ ↑B

Proof state:
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
⊢ 0 ≤ y i

Tactic:
exact hyT.1 i

Result:
no goals

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
⊢ y i ≤ x i + ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
apply le_trans (hyT.2 i)

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
⊢ B' i ≤ x 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
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * (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⟩

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
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑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
⊢ (fun x => ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊) i ≤
    x i + ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
simp only [le_add_iff_nonneg_left]

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
⊢ 0 ≤ x i

Proof state:
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
⊢ B' i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ + y i

Tactic:
norm_cast

Result:
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
⊢ (fun x => ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊) i ≤
    ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ + y i

Proof state:
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 ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ + y i

Tactic:
apply le_trans (hxT.2 i)

Result:
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
⊢ B' i ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ + y i

Proof state:
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))⌋₊

Tactic:
simp only [tsub_le_iff_right]

Result:
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 ≤ ↑⌊(↑n * (1 ⊔ ‖A‖)) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊ + y i