-- 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
rcases₁ :
  ∀ (x : β → ℤ) (hxT : Membership.mem (γ := Finset (β → ℤ)) T x) (y : β → ℤ)
    (hyT : Membership.mem (γ := Finset (β → ℤ)) T y) (hneq : x ≠ y) (hfeq : A *ᵥ x = A *ᵥ y),
    ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₂ :
  ∀ (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), ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₃ rcases₄ :
  ∀ (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),
    ‖replicateCol Unit (x - y) i j‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
rcases₅ :
  ∀ (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
rcases₆ :
  ∀ (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
rcases₇ :
  ∀ (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),
    LE.le (α := ℝ) (↑|x i - y i| : ℝ) (↑B : ℝ)
rcases₈ :
  ∀ (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| ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
rcases₉ :
  ∀ (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),
    -(↑⌊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)) : ℝ)⌋₊ : ℤ)
rcases₁₀ :
  ∀ (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),
    -(↑⌊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)) : ℝ)⌋₊ : ℤ)
left :
  ∀ (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),
    -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i
right right₁ :
  ∀ (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),
    x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e

Tactic:
classical
  -- Pigeonhole
  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⟩
  -- Proofs that x - y ≠ 0 and x - y is a solution
  refine ⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩
  -- Inequality
  have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity
  rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]
  intro i j
  simp only [replicateCol_apply, Pi.sub_apply]
  rw [Int.norm_eq_abs, ← Int.cast_abs]
  refine le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)
  norm_cast
  rw [abs_le]
  rw [Finset.mem_Icc] at hxT hyT
  constructor
  · simp only [neg_le_sub_iff_le_add]
    apply le_trans (hyT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_left]
    exact hxT.1 i
  · simp only [tsub_le_iff_right]
    apply le_trans (hxT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_right]
    exact hyT.1 i

Premises used: le_add_iff_nonneg_right, Int.cast_abs, abs_le, Finset.mem_Icc, Int.norm_eq_abs, tsub_le_iff_right, Matrix.replicateCol_apply, neg_le_sub_iff_le_add, Matrix.norm_replicateCol, le_add_iff_nonneg_left, Pi.sub_apply