awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ Membership.mem (γ := Set ℕ) {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
have left : Membership.mem (γ := Set ℕ) {k : ℕ | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k} (m * n - m - n)
Tactic: push Not
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False
have left : (a + 1) * m + (b + 1) * n = m * n
Tactic: apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (hypothesis)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ (a + 1) * m + (b + 1) * n = m * n
have h₁ : a * m + b * n = m * n - (m + n)
Tactic: simp only [Nat.sub_sub, smul_eq_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a * m + b * n = m * n - (m + n)
⊢ (a + 1) * m + (b + 1) * n = m * n
have left : ∀
  (h :
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑m : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑n : ℤ) =
      HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ)),
  HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) =
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)
Tactic: zify [hmn] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h :
  HMul.hMul (α := ℤ) (↑a : ℤ) (↑m : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑n : ℤ) =
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) =
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)
have left : ∀
  (h :
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑m : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑n : ℤ) -
        (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ)) =
      0),
  HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) -
      HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) =
    0
Tactic: rw [← sub_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h :
  HMul.hMul (α := ℤ) (↑a : ℤ) (↑m : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑n : ℤ) -
      (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ)) =
    0
⊢ HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) -
      HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) =
    0
have left : HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) -
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) =
  HMul.hMul (α := ℤ) (↑a : ℤ) (↑m : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑n : ℤ) -
    (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ))
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k
⊢ k ≤ m * n - m - n
have right : ∀ (hk : m * n - m - n < k), ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k
Tactic: contrapose! hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
⊢ ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k
have right : ∀ (a b : ℕ) (h : a * m + b * n = k), ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k
Tactic: obtain ⟨a, b, h⟩ := exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le m n k
      (by simp [cop.gcd_eq_one]) (by grind [pred_mul, mul_pred, pred_eq_sub_one])
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
n : ℕ
h : n ∈ s
⊢ setGcd s ∣ n
have rw : Membership.mem (γ := Ideal ℤ) (Ideal.span (Nat.cast '' s)) (↑n : ℤ)
Tactic: rw [setGcd, ← Int.dvd_natCast, ← mem_iff_generator_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
n : ℕ
⊢ n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m
have simp_rw : n ∣ Int.natAbs (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
Tactic: simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
    Set.forall_mem_image, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
n : ℕ
simp_rw : n ∣ Int.natAbs (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
⊢ n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m
have simp_rw₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
Tactic: simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
    Set.forall_mem_image, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
n : ℕ
simp_rw : n ∣ Int.natAbs (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
simp_rw₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
⊢ n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m
have simp_rw₂ : (∀ (x : ℤ), Membership.mem (γ := Set ℤ) (Nat.cast '' s) x → (↑n : ℤ) ∣ x) ↔ ∀ m ∈ s, n ∣ m
Tactic: simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
    Set.forall_mem_image, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
n : ℕ
simp_rw : n ∣ Int.natAbs (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
simp_rw₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (generator (Ideal.span (Nat.cast '' s))) ↔ ∀ m ∈ s, n ∣ m
simp_rw₂ : (∀ (x : ℤ), Membership.mem (γ := Set ℤ) (Nat.cast '' s) x → (↑n : ℤ) ∣ x) ↔ ∀ m ∈ s, n ∣ m
⊢ n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m
have simp_rw₃ : (∀ ⦃x : ℕ⦄, x ∈ s → Dvd.dvd (α := ℤ) (↑n : ℤ) (↑x : ℤ)) ↔ ∀ m ∈ s, n ∣ m
Tactic: simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
    Set.forall_mem_image, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw₁ : Eq (α := ℤ) (generator (Ideal.span (Nat.cast '' s))) 0 ↔ s ⊆ {0}
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
simp_rw₁ : Eq (α := ℤ) (generator (Ideal.span (Nat.cast '' s))) 0 ↔ s ⊆ {0}
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw₂ : Eq (α := Submodule ℤ ℤ) (Ideal.span (Nat.cast '' s)) ⊥ ↔ s ⊆ {0}
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
simp_rw₁ : Eq (α := ℤ) (generator (Ideal.span (Nat.cast '' s))) 0 ↔ s ⊆ {0}
simp_rw₂ : Eq (α := Submodule ℤ ℤ) (Ideal.span (Nat.cast '' s)) ⊥ ↔ s ⊆ {0}
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw₃ : (∀ (x : ℤ), Membership.mem (γ := Set ℤ) (Nat.cast '' s) x → x = 0) ↔ s ⊆ {0}
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
simp_rw₁ : Eq (α := ℤ) (generator (Ideal.span (Nat.cast '' s))) 0 ↔ s ⊆ {0}
simp_rw₂ : Eq (α := Submodule ℤ ℤ) (Ideal.span (Nat.cast '' s)) ⊥ ↔ s ⊆ {0}
simp_rw₃ : (∀ (x : ℤ), Membership.mem (γ := Set ℤ) (Nat.cast '' s) x → x = 0) ↔ s ⊆ {0}
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw₄ : (∀ ⦃x : ℕ⦄, x ∈ s → Eq (α := ℤ) (↑x : ℤ) 0) ↔ s ⊆ {0}
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
simp_rw₁ : Eq (α := ℤ) (generator (Ideal.span (Nat.cast '' s))) 0 ↔ s ⊆ {0}
simp_rw₂ : Eq (α := Submodule ℤ ℤ) (Ideal.span (Nat.cast '' s)) ⊥ ↔ s ⊆ {0}
simp_rw₃ : (∀ (x : ℤ), Membership.mem (γ := Set ℤ) (Nat.cast '' s) x → x = 0) ↔ s ⊆ {0}
simp_rw₄ : (∀ ⦃x : ℕ⦄, x ∈ s → Eq (α := ℤ) (↑x : ℤ) 0) ↔ s ⊆ {0}
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw₅ : (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ s ⊆ {0}
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
simp_rw : Int.natAbs (generator (Ideal.span (Nat.cast '' s))) = 0 ↔ s ⊆ {0}
simp_rw₁ : Eq (α := ℤ) (generator (Ideal.span (Nat.cast '' s))) 0 ↔ s ⊆ {0}
simp_rw₂ : Eq (α := Submodule ℤ ℤ) (Ideal.span (Nat.cast '' s)) ⊥ ↔ s ⊆ {0}
simp_rw₃ : (∀ (x : ℤ), Membership.mem (γ := Set ℤ) (Nat.cast '' s) x → x = 0) ↔ s ⊆ {0}
simp_rw₄ : (∀ ⦃x : ℕ⦄, x ∈ s → Eq (α := ℤ) (↑x : ℤ) 0) ↔ s ⊆ {0}
simp_rw₅ : (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ s ⊆ {0}
⊢ setGcd s = 0 ↔ s ⊆ {0}
have simp_rw₆ : (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ ∀ x ∈ s, Membership.mem (γ := Set ℕ) {0} x
Tactic: simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
hs : setGcd s ≠ 0
⊢ ∃ n ∈ s, n ≠ 0
have contrapose! : ∀ (hs : ∀ (n : ℕ) (_ : n ∈ s), n = 0), setGcd s = 0
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑(setGcd s) : ℤ)}) (Ideal.span (Nat.cast '' s))
have rw : Eq (α := Ideal ℤ) (Ideal.span {(↑(Int.natAbs (generator (Ideal.span (Nat.cast '' s)))) : ℤ)})
  (Ideal.span (Nat.cast '' s))
Tactic: rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
rw :
  Eq (α := Ideal ℤ) (Ideal.span {(↑(Int.natAbs (generator (Ideal.span (Nat.cast '' s)))) : ℤ)})
    (Ideal.span (Nat.cast '' s))
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑(setGcd s) : ℤ)}) (Ideal.span (Nat.cast '' s))
have rw₁ : Eq (α := Ideal ℤ) (Ideal.span {generator (Ideal.span (Nat.cast '' s))}) (Ideal.span (Nat.cast '' s))
Tactic: rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
rw :
  Eq (α := Ideal ℤ) (Ideal.span {(↑(Int.natAbs (generator (Ideal.span (Nat.cast '' s)))) : ℤ)})
    (Ideal.span (Nat.cast '' s))
rw₁ : Eq (α := Ideal ℤ) (Ideal.span {generator (Ideal.span (Nat.cast '' s))}) (Ideal.span (Nat.cast '' s))
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑(setGcd s) : ℤ)}) (Ideal.span (Nat.cast '' s))
have rw₂ : Eq (α := Ideal ℤ) (ℤ ∙ generator (Ideal.span (Nat.cast '' s))) (Ideal.span (Nat.cast '' s))
Tactic: rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
rw :
  Eq (α := Ideal ℤ) (Ideal.span {(↑(Int.natAbs (generator (Ideal.span (Nat.cast '' s)))) : ℤ)})
    (Ideal.span (Nat.cast '' s))
rw₁ : Eq (α := Ideal ℤ) (Ideal.span {generator (Ideal.span (Nat.cast '' s))}) (Ideal.span (Nat.cast '' s))
rw₂ : Eq (α := Ideal ℤ) (ℤ ∙ generator (Ideal.span (Nat.cast '' s))) (Ideal.span (Nat.cast '' s))
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑(setGcd s) : ℤ)}) (Ideal.span (Nat.cast '' s))
have rw₃ : Eq (α := Ideal ℤ) (Ideal.span (Nat.cast '' s)) (Ideal.span (Nat.cast '' s))
Tactic: rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
⊢ ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
have pos : ∀ (h0 : setGcd s = 0),
  ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
Tactic: by_cases h0 : setGcd s = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
pos :
  ∀ (h0 : setGcd s = 0),
    ∃ (t : Finset ℕ) (n : ℕ),
      (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
⊢ ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
have neg : ∀ (h0 : ¬setGcd s = 0),
  ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
Tactic: by_cases h0 : setGcd s = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h0 : setGcd s = 0
x : ℕ
h : x ≥ 0
dvd : setGcd s ∣ x
⊢ Membership.mem (γ := Ideal ℕ) (span (↑∅ : Set ℕ)) x
have refl : GE.ge (α := ℕ) 0 0 → ∀ (dvd : setGcd s ∣ 0), Membership.mem (γ := Ideal ℕ) (span (↑∅ : Set ℕ)) 0
Tactic: cases zero_dvd_iff.mp (h0 ▸ dvd)
Cleared hypotheses: x, h, dvd
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
⊢ ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
have neg : ∀ (t : Finset ℕ) (hts : (↑t : Set ℕ) ⊆ s) (a : ↥t → ℤ)
  (eq : Eq (α := ℤ) (∑ i : ↥t, HSMul.hSMul (β := ℤ) (a i) (↑(↑i : ℕ) : ℤ)) (↑(setGcd s) : ℤ)),
  ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
Tactic: have ⟨t, hts, a, eq⟩ := (Submodule.mem_span_image_iff_exists_fun _).mp
    (span_singleton_setGcd s ▸ mem_span_singleton_self _)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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) : ℤ)
⊢ ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
have neg : ∀ (x : ℕ) (hxs : x ∈ s) (hx : x ≠ 0),
  ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
Tactic: have ⟨x, hxs, hx⟩ := exists_ne_zero_of_setGcd_ne_zero h0
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 : ℕ)
⊢ ∃ (t : Finset ℕ) (n : ℕ),
    (↑t : Set ℕ) ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := Ideal ℕ) (span (↑t : Set ℕ)) m
have neg : ∀ (m : ℕ) (ge : m ≥ n) (dvd : setGcd s ∣ m), Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) m
Tactic: refine ⟨insert x t, n, by simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩, fun m ge dvd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) m
have neg : ∀ (c : ℕ) (ge : n + c ≥ n) (dvd : setGcd s ∣ n + c),
  Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + c)
Tactic: obtain ⟨c, rfl⟩ := exists_add_of_le ge
Cleared hypotheses: m, ge, dvd
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + c)
have neg : Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (n + (c / x * x + c % x))
Tactic: rw [← c.div_add_mod' x]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 ℕ)) (n + (q * x + r))
have neg : Membership.mem (γ := Ideal ℕ) (span (↑(insert x t) : Set ℕ)) (q * x + (r + n))
Tactic: rw [add_comm, add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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))
have neg : Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)
Tactic: refine add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
    (Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)
have neg : ∀ (rx : ℕ) (hrx : r = setGcd s * rx), 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
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑t : Set ℕ)) (r + n)
have h : r + n = ∑ c : ↥t, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * (↑c : ℕ)
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)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ r + n = ∑ c : ↥t, (if 0 ≤ a c then rx else x / setGcd s - rx) * (a c).natAbs * (↑c : ℕ)
have 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 : ℕ) : ℤ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ 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 : ℕ) : ℤ))
have 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 : ℤ)
Tactic: congr! 2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ (↑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 : ℤ)
have pos : ∀ (hai : 0 ≤ a i),
  (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
Tactic: split_ifs with hai
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 : ℤ)
⊢ (↑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 : ℤ)
have 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 : ℤ)
Tactic: split_ifs with hai