-- 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
⊢ ∏ x : α, (↑n * (1 ⊔ ‖A‖) * ↑B + 1) = (↑n * (1 ⊔ ‖A‖) * ↑B + 1) ^ m

Tactic:
simp only [prod_const, card_univ]

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_1 : β, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * (1 ⊔ ‖A‖) * ↑B + 1

Tactic:
simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]

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
⊢ ∑ x_1 : β, ↑B * ↑(A i x_1)⁺ + ∑ x : β, ↑B * ↑(A i x)⁻ ≤ ↑n * (1 ⊔ ‖A‖) * ↑B

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‖)) ^ m * (↑B + 1) ^ m = ((↑n * (1 ⊔ ‖A‖)) ^ e) ^ (↑n - ↑m) * (↑B + 1) ^ m

Tactic:
congr 1

Result:
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)

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

Tactic:
exact sub_pos.mpr (mod_cast hn)

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
h1 : ↑n * (1 ⊔ ‖A‖) * ↑B = ∑ x : β, (1 ⊔ ‖A‖) * ↑B
⊢ ∑ x : β, ↑B * ↑((A i x)⁺ + (A i x)⁻) ≤ ∑ x : β, ↑B * (1 ⊔ ‖A‖)

Tactic:
gcongr with j _

Result:
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)⁺ + (A i j)⁻) ≤ 1 ⊔ ‖A‖

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‖)) ^ e) ^ (↑n - ↑m) * (↑B + 1) ^ m < (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ m

Tactic:
gcongr

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

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

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:
rw [card_T_eq A, card_S_eq]

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

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 : α
x✝ : i ∈ univ
⊢ ↑n * (1 ⊔ ‖A‖) * ↑B = ↑n * ((1 ⊔ ‖A‖) * ↑B)

Tactic:
ring

Result:
no goals

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)⁺ + (A i j)⁻) ≤ 1 ⊔ ‖A‖

Tactic:
rw [posPart_add_negPart (A i j), Int.cast_abs]

Result:
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‖

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 : α
x✝ : i ∈ univ
⊢ ↑n * (1 ⊔ ‖A‖) * ↑B = ∑ x : β, (1 ⊔ ‖A‖) * ↑B

Tactic:
simp only [sum_const, card_univ, nsmul_eq_mul]

Result:
α : 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
⊢ ↑n * (1 ⊔ ‖A‖) * ↑B = ↑n * ((1 ⊔ ‖A‖) * ↑B)

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‖) * ↑B + ↑n * (1 ⊔ ‖A‖)) ^ m

Tactic:
gcongr

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
⊢ 1 ≤ ↑n * (1 ⊔ ‖A‖)