awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have rw : ∀ (i : β) (j : Unit), ‖replicateCol Unit (x - y) i j‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ‖replicateCol Unit (x - y) i j‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have simp : ‖x i - y i‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: simp only [replicateCol_apply, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
have rw : (↑|x i - y i| : ℝ) ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: rw [Int.norm_eq_abs, ← Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
have refine : LE.le (α := ℝ) (↑|x i - y i| : ℝ) (↑B : ℝ)
Tactic: refine le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ LE.le (α := ℝ) (↑|x i - y i| : ℝ) (↑B : ℝ)
have norm_cast : |x i - y i| ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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| ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
have 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)) : ℝ)⌋₊ : ℤ)
Tactic: rw [abs_le]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ -(↑⌊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)) : ℝ)⌋₊ : ℤ)
have 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)) : ℝ)⌋₊ : ℤ)
Tactic: rw [Finset.mem_Icc] at hxT hyT
Cleared hypotheses: hxT, y, hyT, hneq, hfeq, n_mul_norm_A_pow_e_nonneg, i, j
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ -(↑⌊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)) : ℝ)⌋₊ : ℤ)
have left : -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ -(↑⌊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)) : ℝ)⌋₊ : ℤ)
have right : x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ -(↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) ≤ x i - y i
have left : y i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
Tactic: simp only [neg_le_sub_iff_le_add]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ y i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
have left : B' i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
Tactic: apply le_trans (hyT.2 i)
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ B' i ≤ x i + (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
have 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)) : ℝ)⌋₊ : ℤ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ (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)) : ℝ)⌋₊ : ℤ)
have left : 0 ≤ x i
Tactic: simp only [le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ x i - y i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ)
have right : x i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
Tactic: simp only [tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ x i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
have right : B' i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
Tactic: apply le_trans (hxT.2 i)
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ B' i ≤ (↑⌊HPow.hPow (β := ℝ) ((↑n : ℝ) * max 1 ‖A‖) (↑(Rat.divInt (↑m : ℤ) (subNatNat n m)) : ℝ)⌋₊ : ℤ) + y i
have 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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ (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
have right : 0 ≤ y i
Tactic: simp only [le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have 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
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