awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
neg : ∀ (m : ℕ) (ge : m ≥ n) (dvd : setGcd s ∣ m), Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) m
⊢ ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m

Tactic:
refine ⟨insert x t, n, by simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩, fun m ge dvd ↦ ?_⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
m : ℕ
ge : m ≥ n
dvd : setGcd s ∣ m
neg :
  ∀ (c : ℕ) (ge : n + c ≥ n) (dvd : setGcd s ∣ n + c),
    Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + c)
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) m

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le ge

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
neg : Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (c / x * x + c % x))
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + c)

Tactic:
rw [← c.div_add_mod' x]

Premises used: Nat.div_add_mod'
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
neg :
  let q := c / x;
  Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (q * x + c % x))
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (c / x * x + c % x))

Tactic:
set q := c / x
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
neg :
  let r := c % x;
  Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (q * x + r))
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (q * x + c % x))

Tactic:
set r := c % x
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
neg : Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (q * x + (r + n))
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (q * x + r))

Tactic:
rw [add_comm, add_assoc]

Premises used: add_assoc, add_comm
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (q * x + (r + n))

Tactic:
add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
    (Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)

Premises used: Ideal.subset_span, Finset.mem_insert_self, Submodule.span_mono, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
neg : Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (q * x + (r + n))

Tactic:
refine add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
    (Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)

Premises used: Ideal.subset_span, Finset.mem_insert_self, Submodule.span_mono, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
⊢ setGcd s ∣ r

Tactic:
(dvd_mod_iff (setGcd_dvd_of_mem hxs)).mpr <|
    (Nat.dvd_add_right <| dvd_mul_of_dvd_right (Finset.dvd_sum fun i _ ↦
      dvd_mul_of_dvd_right (setGcd_dvd_of_mem (hts i.2)) _) _).mp dvd

Premises used: Iff.mpr, Nat.dvd_add_right, dvd_mul_of_dvd_right, Nat.dvd_mod_iff, Finset.dvd_sum, Nat.setGcd_dvd_of_mem, Iff.mp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
neg : ∀ (rx : ℕ) (hrx : r = setGcd s * rx), Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)

Tactic:
obtain ⟨rx, hrx⟩ : setGcd s ∣ r := (dvd_mod_iff (setGcd_dvd_of_mem hxs)).mpr <|
    (Nat.dvd_add_right <| dvd_mul_of_dvd_right (Finset.dvd_sum fun i _ ↦
      dvd_mul_of_dvd_right (setGcd_dvd_of_mem (hts i.2)) _) _).mp dvd

Premises used: Iff.mpr, Nat.dvd_add_right, dvd_mul_of_dvd_right, Nat.dvd_mod_iff, Nat.setGcd, Finset.dvd_sum, Nat.setGcd_dvd_of_mem, Iff.mp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
⊢ Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ))
    (∑ c : ↥t, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * (↑c : ℕ))

Tactic:
(sum_mem fun i _ ↦ mul_mem_left _ _ (subset_span i.2) :
      -- an explicit ℕ-linear combination of elements of `t` that is equal to `r + n`
       ∑ i : t, (if 0 ≤ a i then rx else x / setGcd s - rx) * (a i).natAbs * i ∈ span t)

Premises used: Ideal.subset_span, HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.setGcd, LE.le, SetLike.coe, Int.natAbs, Ideal.span, Ideal.mul_mem_left, OfNat.ofNat, sum_mem, Subtype.property, ite
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
h : r + n = ∑ c : ↥t, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * (↑c : ℕ)
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)

Tactic:
convert!
    (sum_mem fun i _ ↦ mul_mem_left _ _ (subset_span i.2) :
      -- an explicit ℕ-linear combination of elements of `t` that is equal to `r + n`
       ∑ i : t, (if 0 ≤ a i then rx else x / setGcd s - rx) * (a i).natAbs * i ∈ span t)

Premises used: Ideal.subset_span, HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.setGcd, LE.le, SetLike.coe, Int.natAbs, Ideal.span, Ideal.mul_mem_left, OfNat.ofNat, sum_mem, Subtype.property, ite
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
h :
  Eq (α := ℤ)
    (∑ x_1 : ↥t,
      ((↑rx : ℤ) * a x_1 + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a x_1).toNat : ℤ)) * (↑(↑x_1 : ℕ) : ℤ))
    (∑ x_1 : ↥t,
      HMul.hMul (α := ℤ) (↑(if 0 ≤ a x_1 then rx else x / setGcd s - rx) : ℤ) (↑(a x_1).natAbs : ℤ) * (↑(↑x_1 : ℕ) : ℤ))
⊢ r + n = ∑ c : ↥t, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * (↑c : ℕ)

Tactic:
simp_rw [← Int.natCast_inj, hrx, n, Finset.mul_sum, mul_comm _ rx, cast_add, cast_sum, cast_mul,
    ← eq, Finset.mul_sum, smul_eq_mul, ← mul_assoc, ← Finset.sum_add_distrib, ← add_mul]

Premises used: add_mul, Finset.mul_sum, Finset.sum_add_distrib, mul_assoc, Nat.cast_add, Nat.cast_sum, Nat.cast_mul, mul_comm, smul_eq_mul, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
h :
  ∀ (i : ↥t),
    Membership.mem (γ := Finset ↥t) Finset.univ i →
      (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
        HMul.hMul (α := ℤ) (↑(if 0 ≤ a i then rx else x / setGcd s - rx) : ℤ) (↑(a i).natAbs : ℤ)
⊢ Eq (α := ℤ)
    (∑ x_1 : ↥t,
      ((↑rx : ℤ) * a x_1 + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a x_1).toNat : ℤ)) * (↑(↑x_1 : ℕ) : ℤ))
    (∑ x_1 : ↥t,
      HMul.hMul (α := ℤ) (↑(if 0 ≤ a x_1 then rx else x / setGcd s - rx) : ℤ) (↑(a x_1).natAbs : ℤ) * (↑(↑x_1 : ℕ) : ℤ))

Tactic:
congr! 2 with i
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
pos :
  ∀ (hai : 0 ≤ a i),
    (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
      HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
neg :
  ∀ (hai : ¬0 ≤ a i),
    (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
      HMul.hMul (α := ℤ) (↑(x / setGcd s - rx) : ℤ) (↑(a i).natAbs : ℤ)
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑(if 0 ≤ a i then rx else x / setGcd s - rx) : ℤ) (↑(a i).natAbs : ℤ)

Tactic:
split_ifs with hai
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : 0 ≤ a i
⊢ -a i ≤ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : 0 ≤ a i
pos :
  (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑0 : ℤ) = HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
pos₁ : (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) 0 = HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
pos₂ : (↑rx : ℤ) * a i + 0 = HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
pos₃ : (↑rx : ℤ) * a i = HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
pos₄ : (↑rx : ℤ) * a i = (↑rx : ℤ) * |a i|
pos₅ pos₆ : (↑rx : ℤ) * a i = (↑rx : ℤ) * a i
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)

Tactic:
rw [Int.toNat_eq_zero.mpr (by lia), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr hai]

Premises used: Iff.mpr, MulZeroClass.mul_zero, Nat.cast_zero, Int.toNat_eq_zero, add_zero, abs_eq_self, Int.natCast_natAbs
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : ¬0 ≤ a i
⊢ a i ≤ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : ¬0 ≤ a i
⊢ 0 ≤ -a i

Tactic:
lia
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : ¬0 ≤ a i
neg : rx ≤ x / setGcd s
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑(x / setGcd s - rx) : ℤ) (↑(a i).natAbs : ℤ)

Tactic:
rw [cast_sub, Int.natCast_natAbs, abs_eq_neg_self.mpr (by lia), sub_mul,
      ← Int.eq_natCast_toNat.mpr (by lia), mul_neg (rx : ℤ), sub_neg_eq_add, add_comm]

Premises used: Iff.mpr, Nat.cast_sub, Nat.cast, add_comm, sub_mul, abs_eq_neg_self, Int.eq_natCast_toNat, sub_neg_eq_add, mul_neg, Int.natCast_natAbs
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : ¬0 ≤ a i
neg : r ≤ x
⊢ rx ≤ x / setGcd s

Tactic:
rw [← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0), ← hrx,
      Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)]

Premises used: Nat.mul_le_mul_left_iff, Nat.setGcd_dvd_of_mem, pos_of_ne_zero, Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : ¬0 ≤ a i
⊢ r ≤ x

Tactic:
(c.mod_lt (pos_of_ne_zero hx)).le

Premises used: LT.lt.le, Nat.mod_lt, pos_of_ne_zero
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
t : Finset ℕ
hts : (↑t : Set ℕ) ⊆ s
a : ↥t → ℤ
eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)
x : ℕ
hxs : x ∈ s
hx : x ≠ 0
n : ℕ := x / setGcd s * ∑ i : ↥t, (-a i).toNat * (↑i : ℕ)
c : ℕ
ge : n + c ≥ n
dvd : setGcd s ∣ n + c
q : ℕ := c / x
r : ℕ := c % x
rx : ℕ
hrx : r = setGcd s * rx
i : ↥t
h : Membership.mem (γ := Finset ↥t) Finset.univ i
hai : ¬0 ≤ a i
⊢ r ≤ x

Tactic:
exact (c.mod_lt (pos_of_ne_zero hx)).le

Premises used: LT.lt.le, Nat.mod_lt, pos_of_ne_zero
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
⊢ ∃ (n : ℕ), ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m

Tactic:
have ⟨_t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
  ⟨n, fun m ge dvd ↦ (Submodule.span_nat_eq_addSubmonoidClosure s).le
    (Submodule.span_mono hts (hn m ge dvd))⟩

Premises used: Nat.exists_mem_span_nat_finset_of_ge, _private.0.Nat.exists_mem_closure_of_ge.match_1, Exists, Eq.le, Submodule.span_nat_eq_addSubmonoidClosure, Submodule.span_mono, Exists.intro
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
⊢ Set.Finite (α := ℕ) {n : ℕ | setGcd s ∣ n ∧ n ∉ Ideal.span s}

Tactic:
have ⟨n, hn⟩ := exists_mem_closure_of_ge s
  (Finset.range n).finite_toSet.subset fun m h ↦ Finset.mem_range.mpr <|
    lt_of_not_ge fun ge ↦ h.2 <| (Submodule.span_nat_eq_addSubmonoidClosure s).ge (hn m ge h.1)

Premises used: Iff.mpr, Eq.ge, Dvd.dvd, Nat.exists_mem_closure_of_ge, lt_of_not_ge, setOf, Set.Finite, Membership.mem, Nat.setGcd, Set.Finite.subset, Finset.mem_range, Finset.range, And, And.right, And.left, Submodule.span_nat_eq_addSubmonoidClosure, _private.0.Nat.finite_setOf_setGcd_dvd_and_mem_span.match_1, Ideal.span, Finset.finite_toSet, Not
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n_1 : ℕ
s_1 t : Set ℕ
n : ℕ
s : Submodule ℕ ℕ
have :
  ∀ (t : Finset ℕ) (n : ℕ) (hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ))
    (hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m), s.FG
⊢ s.FG

Tactic:
have ⟨t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
⊢ s.FG

Tactic:
⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩

Premises used: Iff.mpr, Membership.mem, LE.le.antisymm, Submodule.FG, Finset.range, Exists.intro, Union.union, Finset.filter, Submodule.span_le
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
refine_1 : (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ) ⊆ (↑s : Set ℕ)
refine_2 :
  ∀ (m : ℕ) (hm : m ∈ s),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
⊢ s.FG

Tactic:
refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
⊢ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ) ⊆ (↑s : Set ℕ)

Tactic:
simpa using ⟨hts, fun _ ↦ And.right⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m_1 n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
m : ℕ
hm : m ∈ s
refine_2 :
  ∀ (le : n ≤ m), Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
refine_2₁ :
  ∀ (gt : m < n), Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m

Tactic:
obtain le | gt := le_or_gt n m

Premises used: le_or_gt
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m_1 n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
m : ℕ
hm : m ∈ s
le : n ≤ m
⊢ (↑t : Set ℕ) ⊆ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m_1 n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
m : ℕ
hm : m ∈ s
le : n ≤ m
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m

Tactic:
exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))

Premises used: Nat.setGcd_dvd_of_mem, Submodule.span_mono
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m_1 n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
m : ℕ
hm : m ∈ s
gt : m < n
⊢ m ∈ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)

Tactic:
simpa using .inr ⟨gt, hm⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m_1 n_1 : ℕ
s_1 t_1 : Set ℕ
n_2 : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : (↑t : Set ℕ) ⊆ (↑s : Set ℕ)
hn : ∀ m ≥ n, setGcd (↑s : Set ℕ) ∣ m → Membership.mem (γ := Ideal ℕ) (Ideal.span (↑t : Set ℕ)) m
m : ℕ
hm : m ∈ s
gt : m < n
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m

Tactic:
exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)

Premises used: Submodule.subset_span