-- Mathlib/NumberTheory/SiegelsLemma.lean
private lemma image_T_subset_S [DecidableEq α] [DecidableEq β] (v) (hv : v ∈ T) : A *ᵥ v ∈ S

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P

Tactic:
have mulVec_def : A.mulVec v =
    fun i ↦ Finset.sum univ fun j : β ↦ A i j * v j := rfl

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P

Tactic:
rw [mulVec_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
⊢ (N ≤ fun i => ∑ j : β, A i j * v j) ∧ (fun i => ∑ j : β, A i j * v j) ≤ P

Proof state:
case refine_2.h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ A i j * v j ≤ ↑B * (A i j)⁺

Tactic:
rw [← mul_comm (v j)]

Result:
case refine_2.h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Proof state:
case refine_2.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
rw [posPart_eq_zero.2 hsign]

Result:
case refine_2.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * 0

Proof state:
case refine_1.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

Tactic:
rw [negPart_eq_zero.2 hsign]

Result:
case refine_1.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * 0) ≤ v j * A i j

Proof state:
case refine_2.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos (hv.1 j) hsign

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
⊢ N i ≤ (fun i => ∑ j : β, A i j * v j) i

case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
⊢ (fun i => ∑ j : β, A i j * v j) i ≤ P i

Tactic:
all_goals
  simp only [mul_neg]
  gcongr ∑ _ : α, ?_ with j _ rw [← mul_comm (v j)] rcases le_total 0 (A i j) with hsign | hsign

Result:
case refine_1.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

case refine_1.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

case refine_2.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

case refine_2.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : v ∈ T
⊢ A *ᵥ v ∈ S

Tactic:
rw [mem_Icc] at hv ⊢

Result:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
⊢ (fun i => ∑ j : β, A i j * v j) i ≤ P i

Tactic:
simp only [mul_neg]

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
⊢ ∑ j : β, A i j * v j ≤ ∑ j : β, ↑B * (A i j)⁺

Proof state:
case refine_2.h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
rcases le_total 0 (A i j) with hsign | hsign

Result:
case refine_2.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

case refine_2.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Proof state:
case refine_1.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * 0) ≤ v j * A i j

Tactic:
exact mul_nonneg (hv.1 j) hsign

Result:
no goals