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 α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m
have rw : ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + (↑n : ℝ) * max 1 ‖A‖) ^ m
Tactic: rw [← mul_pow, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + (↑n : ℝ) * max 1 ‖A‖) ^ m
have hab : 1 ≤ (↑n : ℝ) * max 1 ‖A‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
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
⊢ 1 ≤ (↑n : ℝ) * max 1 ‖A‖
have H : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m
have e_a : ((↑n : ℝ) * max 1 ‖A‖) ^ m = (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ ((↑n : ℝ) * max 1 ‖A‖) ^ m = (((↑n : ℝ) * max 1 ‖A‖) ^ e) ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)
have e_a : HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≠ 0
Tactic: rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
          ← Real.rpow_natCast, div_mul_cancel₀]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ (((↑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
have hbc : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
hbc : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)
⊢ (((↑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
have hbc₁ : ((↑n : ℝ) * max 1 ‖A‖) ^ e < HAdd.hAdd (α := ℝ) (↑B : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
⊢ HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
have rw : HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) *
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑m : ℝ) =
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
Tactic: rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
rw :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) *
      HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑m : ℝ) =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
⊢ HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
have rw₁ : HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) = HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
Tactic: rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
rw :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) *
      HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑m : ℝ) =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
rw₁ :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) = HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
⊢ HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
have rw₂ : HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) =
  HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ)
Tactic: rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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
rw :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) *
      HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑m : ℝ) =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
rw₁ :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) = HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
rw₂ :
  HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) + (↑m : ℝ)) =
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
    HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ n
have rw₃ : HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ) =
  HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑B : ℝ) 1) (↑n : ℝ)
Tactic: rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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 : α,
      (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
have 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))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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 : α,
      (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
have x₁ : ∏ x : α, ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) = ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m
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]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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 : α,
      (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
have x₂ : ((↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1) ^ m ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ m * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m
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]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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 : α,
      (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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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 : α,
      (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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
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 : α,
      (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
have x₅ : HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑B : ℝ) 1 ^ m =
  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]
-- 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: 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⟩
-- 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
⊢ ∃ (t : β → ℤ), t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have refine : ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: refine ⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
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
⊢ ‖x - y‖ ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
have n_mul_norm_A_pow_e_nonneg : 0 ≤ ((↑n : ℝ) * max 1 ‖A‖) ^ e
Tactic: have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity