awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hai : 0 ≤ a i
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
have pos : (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑0 : ℤ) = 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]
-- 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
hai : 0 ≤ a i
pos :
  (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑0 : ℤ) = HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
have pos₁ : (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) 0 = 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]
-- 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
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 : ℤ)
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
have pos₂ : (↑rx : ℤ) * a i + 0 = 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]
-- 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
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 : ℤ)
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
have pos₃ : (↑rx : ℤ) * a i = 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]
-- 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
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 : ℤ)
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
have pos₄ : (↑rx : ℤ) * a i = (↑rx : ℤ) * |a i|
Tactic: rw [Int.toNat_eq_zero.mpr (by lia), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr 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
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|
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑rx : ℤ) (↑(a i).natAbs : ℤ)
have pos₅ : (↑rx : ℤ) * a i = (↑rx : ℤ) * a i
Tactic: rw [Int.toNat_eq_zero.mpr (by lia), cast_zero, mul_zero, add_zero,
      Int.natCast_natAbs, abs_eq_self.mpr 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
hai : ¬0 ≤ a i
⊢ (↑rx : ℤ) * a i + HMul.hMul (α := ℤ) (↑(x / setGcd s) : ℤ) (↑(-a i).toNat : ℤ) =
    HMul.hMul (α := ℤ) (↑(x / setGcd s - rx) : ℤ) (↑(a i).natAbs : ℤ)
have neg : rx ≤ x / setGcd s
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]
-- 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
hai : ¬0 ≤ a i
⊢ rx ≤ x / setGcd s
have neg : r ≤ x
Tactic: rw [← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0), ← hrx,
      Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
m n_1 : ℕ
s_1 t : Set ℕ
n : ℕ
s : Submodule ℕ ℕ
⊢ s.FG
have 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
Tactic: have ⟨t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
have refine_1 : (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ) ⊆ (↑s : Set ℕ)
Tactic: refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 ℕ)
⊢ s.FG
have refine_2 : ∀ (m : ℕ) (hm : m ∈ s),
  Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
Tactic: refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
have refine_2 : ∀ (le : n ≤ m), Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
Tactic: obtain le | gt := le_or_gt n m
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
⊢ Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
have refine_2₁ : ∀ (gt : m < n), Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
Tactic: obtain le | gt := le_or_gt n m
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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
have refine_1 : (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ) ⊆ (↑s : Set ℕ)
Tactic: classical
    refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
    · simpa using ⟨hts, fun _ ↦ And.right⟩
    obtain le | gt := le_or_gt n m
    · exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
    · exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 ℕ)
⊢ s.FG
have refine_2 : ∀ (m : ℕ) (hm : m ∈ s),
  Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
Tactic: classical
    refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
    · simpa using ⟨hts, fun _ ↦ And.right⟩
    obtain le | gt := le_or_gt n m
    · exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
    · exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 refine_2₁ :
  ∀ (m : ℕ) (hm : m ∈ s),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
⊢ s.FG
have refine_2₂ : ∀ (m : ℕ) (hm : m ∈ s) (le : n ≤ m),
  Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
Tactic: classical
    refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
    · simpa using ⟨hts, fun _ ↦ And.right⟩
    obtain le | gt := le_or_gt n m
    · exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
    · exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
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 refine_2₁ :
  ∀ (m : ℕ) (hm : m ∈ s),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
refine_2₂ :
  ∀ (m : ℕ) (hm : m ∈ s) (le : n ≤ m),
    Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
⊢ s.FG
have refine_2₃ : ∀ (m : ℕ) (hm : m ∈ s) (gt : m < n),
  Membership.mem (γ := Submodule ℕ ℕ) (Submodule.span ℕ (↑(t ∪ {m ∈ Finset.range n | m ∈ s}) : Set ℕ)) m
Tactic: classical
    refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
    · simpa using ⟨hts, fun _ ↦ And.right⟩
    obtain le | gt := le_or_gt n m
    · exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
    · exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : AddSubmonoid ℕ
⊢ s.FG
have rw : Submodule.FG (R := ℕ) (M := ℕ) ((AddSubmonoid.toNatSubmodule : (a : AddSubmonoid ℕ) → Submodule ℕ ℕ) s)
Tactic: rw [← s.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg]
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (hypothesis)
Goal:
s : Set ℕ
h : ∃ (n : ℕ), FrobeniusNumber n s
n : ℕ
hn : FrobeniusNumber n s
⊢ setGcd s = 1 ∧ 1 ∉ s
have hn₁ : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: rw [frobeniusNumber_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
⊢ ∃ (n : ℕ), FrobeniusNumber n s
have have : ∀ (n : ℕ) (hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m),
  ∃ (n : ℕ), FrobeniusNumber n s
Tactic: have ⟨n, hn⟩ := exists_mem_closure_of_ge s
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (hypothesis)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
⊢ ∃ (n : ℕ), FrobeniusNumber n s
have this : P 1
Tactic: have : P 1 := h.2 ∘ one_mem_closure_iff.mp
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
⊢ ∃ (n : ℕ), FrobeniusNumber n s
have refine : ∀ (k : ℕ) (gt : k > findGreatest P n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have inl : ∀ (le : k ≤ n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: obtain le | le := le_total k n
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
inl : ∀ (le : k ≤ n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
have inr : ∀ (le : n ≤ k), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: obtain le | le := le_total k n
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
⊢ ∃ (n : ℕ), FrobeniusNumber n s
have refine : ∀ (k : ℕ) (gt : k > findGreatest P n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: classical
    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
    obtain le | le := le_total k n
    · exact of_not_not (findGreatest_is_greatest gt le)
    · exact hn k le (h.1.dvd.trans <| one_dvd k)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
refine : ∀ (k : ℕ) (gt : k > findGreatest P n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ ∃ (n : ℕ), FrobeniusNumber n s
have inl : ∀ (k : ℕ) (gt : k > findGreatest P n) (le : k ≤ n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: classical
    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
    obtain le | le := le_total k n
    · exact of_not_not (findGreatest_is_greatest gt le)
    · exact hn k le (h.1.dvd.trans <| one_dvd k)
-- Lean 4 proof step from Mathlib.NumberTheory.FrobeniusNumber (goal)
Goal:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) m
P : (n : ℕ) → Prop := fun (n : ℕ) ↦ n ∉ AddSubmonoid.closure s
this : P 1
refine : ∀ (k : ℕ) (gt : k > findGreatest P n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
inl :
  ∀ (k : ℕ) (gt : k > findGreatest P n) (le : k ≤ n), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ ∃ (n : ℕ), FrobeniusNumber n s
have inr : ∀ (k : ℕ) (gt : k > findGreatest P n) (le : n ≤ k), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
Tactic: classical
    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
    obtain le | le := le_total k n
    · exact of_not_not (findGreatest_is_greatest gt le)
    · exact hn k le (h.1.dvd.trans <| one_dvd k)
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
have rw : HMul.hMul (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K) x =
  HMul.hMul (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K) x
Tactic: rw [Algebra.smul_def, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ HMul.hMul (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K) x =
    HMul.hMul (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K) x
have e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K)
  ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft) : K)
    ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) c : K)
have e_a : Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
  (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
Tactic: refine congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
have e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)
Tactic: refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_