-- Mathlib/NumberTheory/SiegelsLemma.lean
private lemma card_S_lt_card_T [DecidableEq α] [DecidableEq β]
    (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) :
    #S < #T

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * (1 ⊔ ‖A‖) * ↑B + 1) ^ m ≤ (↑n * (1 ⊔ ‖A‖)) ^ m * (↑B + 1) ^ m

Tactic:
rw [← mul_pow, mul_add, mul_one]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * (1 ⊔ ‖A‖) * ↑B + 1) ^ m ≤ (↑n * (1 ⊔ ‖A‖) * ↑B + ↑n * (1 ⊔ ‖A‖)) ^ m

Proof state:
case bc.hxy
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * (1 ⊔ ‖A‖)) ^ e < ↑B + 1

Tactic:
exact Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ∏ i : α, (P i - N i + 1) < ↑((B + 1) ^ n)

Tactic:
rify

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1) < (↑B + 1) ^ n

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ #S < #T

Tactic:
zify

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ↑(#S) < ↑(#T)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * (1 ⊔ ‖A‖) * ↑B = ∑ x : β, (1 ⊔ ‖A‖) * ↑B
⊢ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ + ∑ x : β, ↑B * ↑(A i x)⁻ ≤ ↑n * (1 ⊔ ‖A‖) * ↑B

Tactic:
simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * (1 ⊔ ‖A‖) * ↑B = ∑ x : β, (1 ⊔ ‖A‖) * ↑B
⊢ ∑ x : β, ↑B * ↑((A i x)⁺ + (A i x)⁻) ≤ ∑ x : β, ↑B * (1 ⊔ ‖A‖)

Proof state:
case hab.bc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
H : 1 ≤ ↑n
⊢ 1 ≤ ↑n * (1 ⊔ ‖A‖)

Tactic:
exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ + ∑ x : β, ↑B * ↑(A i x)⁻ ≤ ↑n * (1 ⊔ ‖A‖) * ↑B

Tactic:
have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
  simp only [sum_const, card_univ, nsmul_eq_mul]
  ring

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * (1 ⊔ ‖A‖) * ↑B = ∑ x : β, (1 ⊔ ‖A‖) * ↑B
⊢ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ + ∑ x : β, ↑B * ↑(A i x)⁻ ≤ ↑n * (1 ⊔ ‖A‖) * ↑B

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ 0 ≤ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1

Tactic:
have h := N_le_P_add_one A i

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h : N i ≤ P i + 1
⊢ 0 ≤ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1

Proof state:
case e_a.h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ↑n - ↑m ≠ 0

Tactic:
exact sub_ne_zero_of_ne (mod_cast hn.ne')

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h : ∑ x : β, ↑B * -↑(A i x)⁻ ≤ ∑ x : β, ↑B * ↑(A i x)⁺ + 1
⊢ 0 ≤ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1

Tactic:
linarith only [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1) ≤ ∏ x : α, (↑n * (1 ⊔ ‖A‖) * ↑B + 1)

Tactic:
refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ 0 ≤ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1

case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * (1 ⊔ ‖A‖) * ↑B + 1

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h : N i ≤ P i + 1
⊢ 0 ≤ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1

Tactic:
rify at h

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h : ∑ x : β, ↑B * -↑(A i x)⁻ ≤ ∑ x : β, ↑B * ↑(A i x)⁺ + 1
⊢ 0 ≤ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A i x_1)⁻ + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ m = (↑B + 1) ^ n

Tactic:
rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]

Result:
no goals

Proof state:
case hab.bc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ 1 ≤ ↑n * (1 ⊔ ‖A‖)

Tactic:
have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)

Result:
case hab.bc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
H : 1 ≤ ↑n
⊢ 1 ≤ ↑n * (1 ⊔ ‖A‖)

Proof state:
case refine_2.h.h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * (1 ⊔ ‖A‖) * ↑B = ∑ x : β, (1 ⊔ ‖A‖) * ↑B
j : β
a✝ : j ∈ univ
⊢ |↑(A i j)| ≤ 1 ⊔ ‖A‖

Tactic:
exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)

Result:
no goals

Proof state:
case e_a
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * (1 ⊔ ‖A‖)) ^ m = ((↑n * (1 ⊔ ‖A‖)) ^ e) ^ (↑n - ↑m)

Tactic:
rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
  ← Real.rpow_natCast, div_mul_cancel₀]

Result:
case e_a.h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ ↑n - ↑m ≠ 0