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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
⊢ (LE.le.{u_1} (α := α → ℤ) N fun (i : α) ↦ ∑ j : β, A i j * v j) ∧
    LE.le.{u_1} (α := α → ℤ) (fun (i : α) ↦ ∑ j : β, A i j * v j) P
have refine_1 : ∀ (i : α), LE.le (α := (fun (i : α) ↦ ℤ) i) (N i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i)
Tactic: refine ⟨fun i ↦ ?_, fun i ↦ ?_⟩
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
refine_1 : ∀ (i : α), LE.le (α := (fun (i : α) ↦ ℤ) i) (N i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i)
⊢ (LE.le.{u_1} (α := α → ℤ) N fun (i : α) ↦ ∑ j : β, A i j * v j) ∧
    LE.le.{u_1} (α := α → ℤ) (fun (i : α) ↦ ∑ j : β, A i j * v j) P
have refine_2 : ∀ (i : α), LE.le (α := (fun (i : α) ↦ ℤ) i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i) (P i)
Tactic: refine ⟨fun i ↦ ?_, fun i ↦ ?_⟩
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
⊢ LE.le (α := (fun (i : α) ↦ ℤ) i) (N i) ((fun (i : α) ↦ (∑ j : β, A i j * v j : ℤ)) i)
have refine_1 : LE.le (α := ℤ) (∑ x : β, -((↑B : ℤ) * (A i x)⁻)) (∑ j : β, A i j * v j)
Tactic: simp only [mul_neg]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
⊢ LE.le (α := ℤ) (∑ x : β, -((↑B : ℤ) * (A i x)⁻)) (∑ j : β, A i j * v j)
have refine_1 : ∀ (j : β), Membership.mem (γ := Finset β) univ j → -((↑B : ℤ) * (A i j)⁻) ≤ A i j * v j
Tactic: gcongr ∑ _ : β, ?_ with j _
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ A i j * v j
have refine_1 : -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
Tactic: rw [← mul_comm (v j)]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
have refine_1 : ∀ (hsign : 0 ≤ A i j), -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
Tactic: rcases le_total 0 (A i j) with hsign | hsign
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
refine_1 : ∀ (hsign : 0 ≤ A i j), -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
have refine_1₁ : ∀ (hsign : A i j ≤ 0), -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
Tactic: rcases le_total 0 (A i j) with hsign | hsign
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
⊢ LE.le (α := ℤ) (∑ j : β, A i j * v j) (∑ j : β, (↑B : ℤ) * (A i j)⁺)
have refine_2 : ∀ (j : β), Membership.mem (γ := Finset β) univ j → A i j * v j ≤ (↑B : ℤ) * (A i j)⁺
Tactic: gcongr ∑ _ : β, ?_ with j _
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
⊢ A i j * v j ≤ (↑B : ℤ) * (A i j)⁺
have refine_2 : v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
Tactic: rw [← mul_comm (v j)]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
have refine_2 : ∀ (hsign : 0 ≤ A i j), v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
Tactic: rcases le_total 0 (A i j) with hsign | hsign
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
refine_2 : ∀ (hsign : 0 ≤ A i j), v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
have refine_2₁ : ∀ (hsign : A i j ≤ 0), v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
Tactic: rcases le_total 0 (A i j) with hsign | hsign
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
have refine_1 : -HMul.hMul (α := ℤ) (↑B : ℤ) 0 ≤ v j * A i j
Tactic: rw [negPart_eq_zero.2 hsign]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ -((↑B : ℤ) * (A i j)⁻) ≤ v j * A i j
have refine_1 : -((↑B : ℤ) * -A i j) ≤ v j * A i j
Tactic: rw [negPart_eq_neg.2 hsign]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ -((↑B : ℤ) * -A i j) ≤ v j * A i j
have refine_1 : (↑B : ℤ) * A i j ≤ v j * A i j
Tactic: simp only [mul_neg, neg_neg]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
have refine_2 : v j * A i j ≤ (↑B : ℤ) * A i j
Tactic: rw [posPart_eq_self.2 hsign]
-- 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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ (↑B : ℤ) * A i j
have refine_2 : v j ≤ (↑B : ℤ)
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 β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun (i : α) ↦ ∑ j : β, A i j * v j
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
hsign : A i j ≤ 0
⊢ v j * A i j ≤ (↑B : ℤ) * (A i j)⁺
have refine_2 : v j * A i j ≤ HMul.hMul (α := ℤ) (↑B : ℤ) 0
Tactic: rw [posPart_eq_zero.2 hsign]
-- 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 β
⊢ card.{u_2} (α := β → ℤ) T = (B + 1) ^ n
have rw : ∏ i : β, card (α := ℤ) (Icc (0 i) (↑B : ℤ)) = (B + 1) ^ n
Tactic: rw [Pi.card_Icc 0 B']
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
⊢ LE.le (α := ℤ) (N i) 0
have h : ∀ (i_1 : β), Membership.mem (γ := Finset β) univ i_1 → (↑B : ℤ) * -(A i i_1)⁻ ≤ 0
Tactic: apply Finset.sum_nonpos
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
j : β
h : Membership.mem (γ := Finset β) univ j
⊢ (↑B : ℤ) * -(A i j)⁻ ≤ 0
have h : 0 ≤ (↑B : ℤ) * (A i j)⁻
Tactic: simp only [mul_neg, Left.neg_nonpos_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
⊢ 0 ≤ HAdd.hAdd (α := ℤ) (P i) 1
have apply : ∀ (i_1 : β), Membership.mem (γ := Finset β) univ i_1 → 0 ≤ (↑B : ℤ) * (A i i_1)⁺
Tactic: apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
⊢ N i ≤ HAdd.hAdd (α := ℤ) (P i) 1
have calc : LE.le (α := ℤ) (N i) 0
Tactic: calc N i
  _ ≤ 0 := by
    apply Finset.sum_nonpos
    intro j _
    simp only [mul_neg, Left.neg_nonpos_iff]
    positivity
  _ ≤ P i + 1 := by
    apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))
    intro j _
    positivity
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
i : α
calc : LE.le (α := ℤ) (N i) 0
⊢ N i ≤ HAdd.hAdd (α := ℤ) (P i) 1
have calc₁ : 0 ≤ HAdd.hAdd (α := ℤ) (P i) 1
Tactic: calc N i
  _ ≤ 0 := by
    apply Finset.sum_nonpos
    intro j _
    simp only [mul_neg, Left.neg_nonpos_iff]
    positivity
  _ ≤ P i + 1 := by
    apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))
    intro j _
    positivity
-- 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 α
⊢ Eq (α := ℤ) (↑(card.{u_1} (α := α → ℤ) S) : ℤ) (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1))
have rw : Eq (α := ℤ) (∏ i : α, (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
  (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1))
Tactic: rw [Pi.card_Icc N P, Nat.cast_prod]
-- 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 α
⊢ Eq (α := ℤ) (∏ i : α, (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
    (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1))
have e_f : Eq.{u_1 + 1} (α := α → ℤ)
  (fun (i : α) ↦ (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
  fun (i : α) ↦ HSub.hSub (α := ℤ) (P i) (N i) + 1
Tactic: congr
-- 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 α
⊢ Eq.{u_1 + 1} (α := α → ℤ)
    (fun (i : α) ↦ (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ))
    fun (i : α) ↦ HSub.hSub (α := ℤ) (P i) (N i) + 1
have e_f : ∀ (i : α),
  (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ) =
    HSub.hSub (α := ℤ) (P i) (N i) + 1
Tactic: ext i
-- 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 α
i : α
⊢ (↑(card (α := ℤ) (Icc (∑ j : β, (↑B : ℤ) * -(A i j)⁻) (∑ j : β, (↑B : ℤ) * (A i j)⁺))) : ℤ) =
    HSub.hSub (α := ℤ) (P i) (N i) + 1
have e_f : HAdd.hAdd (α := ℤ) (P i) 1 - N i = HSub.hSub (α := ℤ) (P i) (N i) + 1
Tactic: rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
⊢ 1 ≤ ‖A‖
have by_contra! : ∀ (h : ‖A‖ < 1), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ False
have apply : A = 0
Tactic: apply hA
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ A = 0
have a : ∀ (i : α) (j : β), A i j = 0 i j
Tactic: ext 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 α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
⊢ A i j = 0
have a : ∀ (h : ∀ (i : α) (j : β), ‖A i j‖ < 1) (i : α) (j : β), A i j = 0
Tactic: rw [norm_lt_iff Real.zero_lt_one] at h
Cleared hypotheses: h, i, j
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ∀ (i : α) (j : β), ‖A i j‖ < 1
i : α
j : β
⊢ A i j = 0
have h₁ : ‖A i j‖ < 1
Tactic: specialize h i j
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : ‖A i j‖ < 1
⊢ A i j = 0
have h₁ : LT.lt (α := ℝ) |(↑(A i j) : ℝ)| 1
Tactic: rw [Int.norm_eq_abs] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SiegelsLemma (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : LT.lt (α := ℝ) |(↑(A i j) : ℝ)| 1
⊢ A i j = 0
have h₁ : |A i j| < 1
Tactic: norm_cast at h
Cleared hypotheses: h
-- 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
⊢ card.{u_1} (α := α → ℤ) S < card.{u_2} (α := β → ℤ) T
have zify : LT.lt (α := ℤ) (↑(card.{u_1} (α := α → ℤ) S) : ℤ) (↑(card.{u_2} (α := β → ℤ) T) : ℤ)
Tactic: zify
-- 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
⊢ LT.lt (α := ℤ) (↑(card.{u_1} (α := α → ℤ) S) : ℤ) (↑(card.{u_2} (α := β → ℤ) T) : ℤ)
have rw : LT.lt (α := ℤ) (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1)) (↑((B + 1) ^ n) : ℤ)
Tactic: rw [card_T_eq A, card_S_eq]
-- 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
⊢ LT.lt (α := ℤ) (∏ i : α, (HSub.hSub (α := ℤ) (P i) (N i) + 1)) (↑((B + 1) ^ n) : ℤ)
have rify : ∏ 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
Tactic: rify
-- 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
⊢ 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))
have refine_1 : ∀ (i : α),
  Membership.mem (γ := Finset α) univ i →
    0 ≤
      HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
          (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
        1
Tactic: refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
-- 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
refine_1 :
  ∀ (i : α),
    Membership.mem (γ := Finset α) univ i →
      0 ≤
        HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
            (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
          1
⊢ 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))
have refine_2 : ∀ (i : α),
  Membership.mem (γ := Finset α) univ i →
    HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
          (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
        1 ≤
      (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1
Tactic: refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
-- 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
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ 0 ≤
    HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1
have h : N i ≤ HAdd.hAdd (α := ℤ) (P i) 1
Tactic: have h := N_le_P_add_one A i
-- 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
i : α
h_1 : Membership.mem (γ := Finset α) univ i
h : N i ≤ HAdd.hAdd (α := ℤ) (P i) 1
⊢ 0 ≤
    HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1
have h₁ : ∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x)⁻ : ℝ)) ≤
  HAdd.hAdd (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁺ : ℝ)) 1
Tactic: rify at h
Cleared hypotheses: h
-- 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
i : α
h_1 : Membership.mem (γ := Finset α) univ i
h :
  ∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x)⁻ : ℝ)) ≤
    HAdd.hAdd (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁺ : ℝ)) 1
⊢ 0 ≤
    HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1
have linarith : HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1 <
    0 →
  HMul.hMul (α := ℝ) 1 (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ)) -
            HMul.hMul (α := ℝ) 1 (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
          HMul.hMul (α := ℝ) 1 1 -
        HMul.hMul (α := ℝ) 1 0 +
      (HMul.hMul (α := ℝ) 1 (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x)⁻ : ℝ))) -
        (HMul.hMul (α := ℝ) 1 (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁺ : ℝ)) + HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith only [h]
-- 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
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ HSub.hSub (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
        (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (-(↑(A i x_1)⁻ : ℝ))) +
      1 ≤
    (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) + 1
have refine_2 : HAdd.hAdd (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
    (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁻ : ℝ)) ≤
  (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ)
Tactic: simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_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 α β ℤ
inst_2 : DecidableEq α
inst_3 : DecidableEq β
hn : m < n
hm : 0 < m
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
have simp : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = (↑n : ℝ) * (max 1 ‖A‖ * (↑B : ℝ))
Tactic: simp
-- 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
i : α
h : Membership.mem (γ := Finset α) univ i
⊢ HAdd.hAdd (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
      (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁻ : ℝ)) ≤
    (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ)
have h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
Tactic: have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
-- 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
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∑ x_1 : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x_1)⁺ : ℝ))
      (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑(A i x)⁻ : ℝ)) ≤
    (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ)
have refine_2 : LE.le (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑((A i x)⁺ + (A i x)⁻) : ℝ)) (∑ x : β, (↑B : ℝ) * max 1 ‖A‖)
Tactic: simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
-- 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
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
⊢ LE.le (α := ℝ) (∑ x : β, HMul.hMul (α := ℝ) (↑B : ℝ) (↑((A i x)⁺ + (A i x)⁻) : ℝ)) (∑ x : β, (↑B : ℝ) * max 1 ‖A‖)
have refine_2 : ∀ (j : β), Membership.mem (γ := Finset β) univ j → (↑((A i j)⁺ + (A i j)⁻) : ℝ) ≤ max 1 ‖A‖
Tactic: gcongr with j _
-- 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
i : α
h : Membership.mem (γ := Finset α) univ i
h1 : (↑n : ℝ) * max 1 ‖A‖ * (↑B : ℝ) = ∑ x : β, max 1 ‖A‖ * (↑B : ℝ)
j : β
h_1 : Membership.mem (γ := Finset β) univ j
⊢ (↑((A i j)⁺ + (A i j)⁻) : ℝ) ≤ max 1 ‖A‖
have refine_2 : |(↑(A i j) : ℝ)| ≤ max 1 ‖A‖
Tactic: rw [posPart_add_negPart (A i j), Int.cast_abs]