awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
h₁₁ : (b.psp_from_prime p).FermatPsp b ∧ m ≤ b.psp_from_prime p
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n

Tactic:
use psp_from_prime b p

Premises used: _private.0.Nat.psp_from_prime
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
h₁₁ : (b.psp_from_prime p).FermatPsp b
h₁₂ : m ≤ b.psp_from_prime p
⊢ (b.psp_from_prime p).FermatPsp b ∧ m ≤ b.psp_from_prime p

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ (b.psp_from_prime p).FermatPsp b

Tactic:
psp_from_prime_psp b_ge_two hp₂ h₉ h₆

Premises used: _private.0.Nat.psp_from_prime_psp
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ (b.psp_from_prime p).FermatPsp b

Tactic:
exact psp_from_prime_psp b_ge_two hp₂ h₉ h₆

Premises used: _private.0.Nat.psp_from_prime_psp
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ m ≤ p

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (HPow.hPow (β := ℕ) b 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ HPow.hPow (β := ℕ) b 2
h₃ : 0 < HPow.hPow (β := ℕ) b 2 - 1
h₄ : 0 < b * (HPow.hPow (β := ℕ) b 2 - 1)
h₅ : b * (HPow.hPow (β := ℕ) b 2 - 1) < p
h₆ : ¬p ∣ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₇ : b ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₈ : 2 ≤ b * (HPow.hPow (β := ℕ) b 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ m ≤ b.psp_from_prime p

Tactic:
exact le_trans (show m ≤ p by lia) (le_of_lt h₁₀)

Premises used: le_of_lt, le_trans
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ b = 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ b = 1

Tactic:
have h₁ : b = 1 := by lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
neg : ∃ (n : ℕ), n.FermatPsp 1 ∧ m ≤ n
⊢ ∃ (n : ℕ), n.FermatPsp b ∧ m ≤ n

Tactic:
rw [h₁]
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
h₂ : (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)
⊢ ∃ (n : ℕ), n.FermatPsp 1 ∧ m ≤ n

Tactic:
use 2 * (m + 2)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ Ne (α := ℕ) 2 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ m + 2 ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ¬Prime (2 * (m + 2))

Tactic:
have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by lia) (by lia)
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ 1 < 2 * (m + 2)

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ m ≤ 2 * (m + 2)

Tactic:
lia
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
this : ¬Prime (2 * (m + 2))
⊢ (2 * (m + 2)).FermatPsp 1 ∧ m ≤ 2 * (m + 2)

Tactic:
exact ⟨fermatPsp_base_one (by lia) this, by lia⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b

Tactic:
Filter.frequently_atTop.2 fun n => ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
refine : ∀ (n : ℕ), ∃ b_1 ≥ n, b_1.FermatPsp b
⊢ ∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b

Tactic:
refine Filter.frequently_atTop.2 fun n => ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
n : ℕ
obtain : ∀ (p : ℕ) (hp : p.FermatPsp b ∧ n ≤ p), ∃ b_1 ≥ n, b_1.FermatPsp b
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b

Tactic:
obtain ⟨p, hp⟩ := exists_infinite_pseudoprimes h n

Premises used: Nat.exists_infinite_pseudoprimes
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : p.FermatPsp b ∧ n ≤ p
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b

Tactic:
⟨p, hp.2, hp.1⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
n p : ℕ
hp : p.FermatPsp b ∧ n ≤ p
⊢ ∃ b_1 ≥ n, b_1.FermatPsp b

Tactic:
exact ⟨p, hp.2, hp.1⟩
-- Module: Mathlib.NumberTheory.FermatPsp
Goal:
b : ℕ
h : 1 ≤ b
⊢ Set.Infinite (α := ℕ) {n : ℕ | n.FermatPsp b}

Tactic:
Nat.frequently_atTop_iff_infinite.mp (frequently_atTop_fermatPsp h)

Premises used: Nat.frequently_atTop_fermatPsp, Nat.frequently_atTop_iff_infinite, Iff.mp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
n : ℕ
s : Set ℕ
simp_rw :
  IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₁ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | k ∉ AddSubmonoid.closure s}) n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₂ :
  Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} n ∧
      Membership.mem (γ := Set ℕ)
        {x : ℕ | ∀ ⦃a : ℕ⦄, Membership.mem (γ := Set ℕ) {k : ℕ | k ∉ AddSubmonoid.closure s} a → a ≤ x} n ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₃ :
  (n ∉ AddSubmonoid.closure s ∧ ∀ ⦃a : ℕ⦄, a ∉ AddSubmonoid.closure s → a ≤ n) ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
simp_rw₄ :
  (n ∉ AddSubmonoid.closure s ∧ ∀ ⦃a : ℕ⦄, ¬a ≤ n → Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) a) ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k
⊢ FrobeniusNumber n s ↔
    n ∉ AddSubmonoid.closure s ∧ ∀ k > n, Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) k

Tactic:
simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]

Premises used: not_le, FrobeniusNumber, not_imp_comm, upperBounds, Set.mem_setOf, IsGreatest
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
simp_rw : IsGreatest {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
⊢ FrobeniusNumber (m * n - m - n) {m, n}

Tactic:
simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]

Premises used: FrobeniusNumber, AddSubmonoid.mem_closure_pair
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
⊢ m + n ≤ m * n

Tactic:
have hmn : m + n ≤ m * n := add_le_mul hm hn
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
left : Membership.mem (γ := Set ℕ) {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)
right :
  Membership.mem (γ := Set ℕ) (upperBounds {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k}) (m * n - m - n)
⊢ IsGreatest {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
left : Membership.mem (γ := Set ℕ) {k : ℕ | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k} (m * n - m - n)
⊢ Membership.mem (γ := Set ℕ) {k : ℕ | ¬∃ (m_1 : ℕ) (n_1 : ℕ), m_1 • m + n_1 • n = k} (m * n - m - n)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
left : (a + 1) * m + (b + 1) * n = m * n
⊢ False

Tactic:
apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)

Premises used: Nat.add_one_ne_zero, Nat.Coprime.mul_add_mul_ne_mul
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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 * m + b * n = m * n - (m + n)

Tactic:
simp only [Nat.sub_sub, smul_eq_mul] at h

Premises used: Nat.sub_sub, smul_eq_mul
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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)
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 : ℤ)
⊢ (a + 1) * m + (b + 1) * n = m * n

Tactic:
zify [hmn] at h ⊢
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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 : ℤ)
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
⊢ HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) =
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)

Tactic:
rw [← sub_eq_zero] at h ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
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 : ℤ))
⊢ HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 * (↑m : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 * (↑n : ℤ) -
      HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) =
    0

Tactic:
rw [← h]
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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 : ℤ) =
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑m : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑n : ℤ) -
      (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
right : ∀ (hk : m * n - m - n < k), ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k
⊢ k ≤ m * n - m - n

Tactic:
contrapose! hk
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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.gcd n ∣ k

Tactic:
simp [cop.gcd_eq_one]

Premises used: Nat.Coprime.gcd_eq_one
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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.pred * n.pred ≤ k

Tactic:
grind [pred_mul, mul_pred, pred_eq_sub_one]

Premises used: Nat.mul_pred, Nat.pred_eq_sub_one, Nat.pred_mul
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
right : ∀ (a b : ℕ) (h : a * m + b * n = k), ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * 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])

Premises used: Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
a b : ℕ
h : a * m + b * n = k
⊢ ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k

Tactic:
⟨a, b, succ_inj.mp (congrArg succ h)⟩

Premises used: Nat.succ_inj, congrArg, Exists.intro, Iff.mp, Nat.succ
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
a b : ℕ
h : a * m + b * n = k
⊢ ∃ (m_1 : ℕ) (n_1 : ℕ), m_1 * m + n_1 * n = k

Tactic:
exact ⟨a, b, succ_inj.mp (congrArg succ h)⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
n : ℕ
h : n ∈ s
rw : Membership.mem (γ := Ideal ℤ) (Ideal.span (Nat.cast '' s)) (↑n : ℤ)
⊢ setGcd s ∣ n

Tactic:
rw [setGcd, ← Int.dvd_natCast, ← mem_iff_generator_dvd]

Premises used: Int.dvd_natCast, Nat.setGcd, Submodule.IsPrincipal.mem_iff_generator_dvd
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
n : ℕ
h : n ∈ s
⊢ Membership.mem (γ := Ideal ℤ) (Ideal.span (Nat.cast '' s)) (↑n : ℤ)

Tactic:
Ideal.subset_span ⟨n, h, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
n : ℕ
h : n ∈ s
⊢ Membership.mem (γ := Ideal ℤ) (Ideal.span (Nat.cast '' s)) (↑n : ℤ)

Tactic:
exact Ideal.subset_span ⟨n, h, rfl⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
n : ℕ
h : Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) n
⊢ setGcd s ∣ n

Tactic:
AddSubmonoid.closure_induction (fun _ ↦ setGcd_dvd_of_mem) (dvd_zero _) (fun _ _ _ _ ↦ dvd_add) h

Premises used: AddSubmonoid.closure_induction
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
simp_rw₃ : (∀ ⦃x : ℕ⦄, x ∈ s → Dvd.dvd (α := ℤ) (↑n : ℤ) (↑x : ℤ)) ↔ ∀ m ∈ s, n ∣ m
⊢ n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m

Tactic:
simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
    Set.forall_mem_image, Int.natCast_dvd_natCast]

Premises used: Nat.setGcd, Submodule.IsPrincipal.dvd_generator_span_iff, Int.natCast_dvd, Set.forall_mem_image, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s t : Set ℕ
h : s ⊆ t
⊢ setGcd t ∣ setGcd s

Tactic:
dvd_setGcd_iff.mpr fun _m hm ↦ setGcd_dvd_of_mem (h hm)

Premises used: Iff.mpr, Nat.setGcd_dvd_of_mem, Nat.dvd_setGcd_iff
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
n : ℕ
h : ¬setGcd s ∣ n
⊢ DvdNotUnit (setGcd (insert n s)) (setGcd s)

Tactic:
dvdNotUnit_of_dvd_of_not_dvd (setGcd_mono <| Set.subset_insert ..)
    fun dvd ↦ h <| dvd_setGcd_iff.mp dvd _ (Set.mem_insert ..)

Premises used: dvdNotUnit_of_dvd_of_not_dvd, Nat.dvd_setGcd_iff, Iff.mp, Set.mem_insert, Nat.setGcd_mono, Set.subset_insert
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
m : ℕ
h : setGcd s ∣ m
⊢ setGcd s ∣ m

Tactic:
h
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
n : ℕ
h : setGcd s ∣ n
m : ℕ
hm : m ∈ s
⊢ setGcd s ∣ m

Tactic:
setGcd_dvd_of_mem hm

Premises used: Nat.setGcd_dvd_of_mem
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
m : ℕ
h : setGcd s ∣ m
⊢ setGcd s ∣ m

Tactic:
exacts [h, setGcd_dvd_of_mem hm]
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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}
simp_rw₆ : (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ ∀ x ∈ s, Membership.mem (γ := Set ℕ) {0} x
⊢ setGcd 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]

Premises used: Set.subset_def, Nat.setGcd, Int.natCast_eq_zero, Int.natAbs_eq_zero, Set.mem_singleton_iff, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot, Set.forall_mem_image
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
hs : setGcd s ≠ 0
contrapose! : ∀ (hs : ∀ (n : ℕ) (_ : n ∈ s), n = 0), setGcd s = 0
⊢ ∃ n ∈ s, n ≠ 0

Tactic:
contrapose! hs
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
hs : ∀ (n : ℕ) (_ : n ∈ s), n = 0
⊢ setGcd s = 0

Tactic:
setGcd_eq_zero_iff.mpr hs

Premises used: Iff.mpr, Nat.setGcd_eq_zero_iff
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
hs : ∀ (n : ℕ) (_ : n ∈ s), n = 0
⊢ setGcd s = 0

Tactic:
exact setGcd_eq_zero_iff.mpr hs

Premises used: Iff.mpr, Nat.setGcd_eq_zero_iff
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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))
rw₃ rw₄ : Eq (α := Ideal ℤ) (Ideal.span (Nat.cast '' s)) (Ideal.span (Nat.cast '' s))
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑(setGcd s) : ℤ)}) (Ideal.span (Nat.cast '' s))

Tactic:
rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
    Ideal.span, span_singleton_generator]

Premises used: Iff.mpr, Ideal.span_singleton_eq_span_singleton, Nat.setGcd, Submodule.IsPrincipal.span_singleton_generator, Ideal.span, Int.associated_natAbs
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
⊢ s ⊆ (↑(Ideal.span {setGcd s}) : Set ℕ)

Tactic:
fun _x hx ↦ Ideal.mem_span_singleton.mpr (setGcd_dvd_of_mem hx)

Premises used: Iff.mpr, Set.Mem, setOf, Set.Subset, Nat.setGcd_dvd_of_mem, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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
neg :
  ∀ (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

Tactic:
by_cases h0 : setGcd s = 0

Premises used: Nat.setGcd
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : setGcd s = 0
⊢ (↑∅ : Set ℕ) ⊆ s

Tactic:
simp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : setGcd s = 0
x : ℕ
h : x ≥ 0
dvd : setGcd s ∣ x
refl : GE.ge (α := ℕ) 0 0 → ∀ (dvd : setGcd s ∣ 0), Membership.mem (γ := Ideal ℕ) (span (↑∅ : Set ℕ)) 0
⊢ Membership.mem (γ := Ideal ℕ) (span (↑∅ : Set ℕ)) x

Tactic:
cases zero_dvd_iff.mp (h0 ▸ dvd)

Premises used: zero_dvd_iff, Iff.mp
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : setGcd s = 0
h : GE.ge (α := ℕ) 0 0
dvd : setGcd s ∣ 0
⊢ Membership.mem (γ := Ideal ℕ) (span (↑∅ : Set ℕ)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : setGcd s = 0
h : GE.ge (α := ℕ) 0 0
dvd : setGcd s ∣ 0
⊢ Membership.mem (γ := Ideal ℕ) (span (↑∅ : Set ℕ)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.NumberTheory.FrobeniusNumber
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

Tactic:
refine ⟨∅, 0, by simp, fun _ _ dvd ↦ by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _⟩
-- Module: Mathlib.NumberTheory.FrobeniusNumber
Goal:
s : Set ℕ
h0 : ¬setGcd s = 0
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
⊢ ∃ (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 _)
-- 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) : ℤ)
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
⊢ ∃ (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
-- 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 : ℕ)
⊢ (↑(insert x t) : Set ℕ) ⊆ s

Tactic:
simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩

Premises used: Set.insert_subset_iff