awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
h : P (m_1 + 1)
⊢ findGreatest P m ≤ m_1 + 1

Tactic:
exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)

Premises used: Nat.le_succ, Nat.findGreatest_le, le_trans
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
h : ¬P (m_1 + 1)
⊢ findGreatest P m ≤ findGreatest P m_1

Tactic:
ih
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
h : ¬P (m_1 + 1)
⊢ findGreatest P m ≤ findGreatest P m_1

Tactic:
exact ih
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n : ℕ
hmn : m ≤ n
refl : findGreatest P m ≤ findGreatest P m
step :
  ∀ {m_1 : ℕ} (hmk : m.le m_1) (ih : findGreatest P m ≤ findGreatest P m_1), findGreatest P m ≤ findGreatest P m_1.succ
⊢ findGreatest P m ≤ findGreatest P n

Tactic:
induction hmn with
  | refl => simp
  | step hmk ih =>
    rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih

Premises used: Nat.le_succ, Nat.findGreatest_succ, refl, Nat.findGreatest_le, le_trans
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
⊢ findGreatest P 0 ≤ findGreatest P 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
pos : ∀ (h : P (n + 1)), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
neg : ∀ (h : ¬P (n + 1)), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
by_cases h : P (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
pos : n + 1 ≤ findGreatest Q (n + 1)
pos₁ pos₂ : n + 1 ≤ n + 1
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]

Premises used: Nat.findGreatest_eq
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
neg : findGreatest P n ≤ findGreatest Q (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
rw [findGreatest_of_not h]

Premises used: Nat.findGreatest_of_not
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P n ≤ findGreatest Q (n + 1)

Tactic:
le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

Premises used: Nat.le_succ, Nat.findGreatest_mono_right, le_trans
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P n ≤ findGreatest Q (n + 1)

Tactic:
exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

Premises used: Nat.le_succ, Nat.findGreatest_mono_right, le_trans
-- Module: Mathlib.Data.Nat.Find
Goal:
P Q : ℕ → Prop
inst : DecidablePred P
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
zero : findGreatest P 0 ≤ findGreatest P 0
succ : ∀ (n : ℕ) (hn : findGreatest P n ≤ findGreatest Q n), findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
⊢ findGreatest P n ≤ findGreatest Q n

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

Premises used: HAdd.hAdd, Nat.zero, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P Q : ℕ → Prop
inst : DecidablePred P
n : ℕ
inst_1 : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
hmn : m ≤ n
⊢ findGreatest P m ≤ findGreatest Q n

Tactic:
le_trans (Nat.findGreatest_mono_right _ hmn) (findGreatest_mono_left hPQ _)

Premises used: Nat.findGreatest_mono_left, Nat.findGreatest_mono_right, le_trans
-- Module: Mathlib.Data.Nat.Find
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hk : findGreatest P n < k
hkb : k ≤ n
⊢ ¬P k

Tactic:
(findGreatest_eq_iff.1 rfl).2.2 hk hkb

Premises used: And.right, Iff.mp, Nat.findGreatest_eq_iff, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
h : findGreatest P n = m
h0 : m ≠ 0
⊢ P m

Tactic:
(findGreatest_eq_iff.1 h).2.1 h0

Premises used: And.right, And.left, Iff.mp, Nat.findGreatest_eq_iff
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
hd : ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d
⊢ d = a.gcd b

Tactic:
(dvd_antisymm (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)) (dvd_gcd hda hdb)).symm

Premises used: Nat.gcd_dvd_left, dvd_antisymm, Nat.dvd_gcd, Nat.gcd_dvd_right, Eq.symm
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
inl : (HPow.hPow (α := ℕ) 0 c - 1) % (HPow.hPow (α := ℕ) 0 b - 1) = HPow.hPow (α := ℕ) 0 (c % b) - 1
inr : ∀ (ha0 : a > 0), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases eq_zero_or_pos a with rfl | ha0

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
inl :
  HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1
⊢ (HPow.hPow (α := ℕ) 0 c - 1) % (HPow.hPow (α := ℕ) 0 b - 1) = HPow.hPow (α := ℕ) 0 (c % b) - 1

Tactic:
simp [zero_pow_eq]

Premises used: zero_pow_eq
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
pos : c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg : c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₁ : c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
neg₁ : c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
pos₂ : ¬c = 0 → b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1
neg₂ : ¬c = 0 → b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1
pos₃ : ¬c = 0 → ¬b = 0 → c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1
neg₃ : ¬c = 0 → ¬b = 0 → ¬c % b = 0 → HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
⊢ HSub.hSub (α := ℕ) (if c = 0 then 1 else 0) 1 % HSub.hSub (α := ℕ) (if b = 0 then 1 else 0) 1 =
    HSub.hSub (α := ℕ) (if c % b = 0 then 1 else 0) 1

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : c = 0
h_1 : b = 0
h_2 : c % b = 0
⊢ HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : c = 0
h_1 : b = 0
h_2 : ¬c % b = 0
⊢ HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : c = 0
h_1 : ¬b = 0
h_2 : c % b = 0
⊢ HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : c = 0
h_1 : ¬b = 0
h_2 : ¬c % b = 0
⊢ HSub.hSub (α := ℕ) 1 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : ¬c = 0
h_1 : b = 0
h_2 : c % b = 0
⊢ HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : ¬c = 0
h_1 : b = 0
h_2 : ¬c % b = 0
⊢ HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 1 1 = HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : ¬c = 0
h_1 : ¬b = 0
h_2 : c % b = 0
⊢ HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
h : ¬c = 0
h_1 : ¬b = 0
h_2 : ¬c % b = 0
⊢ HSub.hSub (α := ℕ) 0 1 % HSub.hSub (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
inr : ∀ (ha0 : succ 0 > 0), (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1
inr₁ : ∀ (ha1 : succ 0 < a), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1

Premises used: Nat.eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c : ℕ
ha0 : succ 0 > 0
⊢ (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
inr : (a ^ c - 1) % (HPow.hPow (β := ℕ) a 0 - 1) = a ^ (c % 0) - 1
inr₁ : ∀ (hb0 : b > 0), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases eq_zero_or_pos b with rfl | hb0

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (HPow.hPow (β := ℕ) a 0 - 1) = a ^ (c % 0) - 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
inr : ∀ (h : c < b), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
inr₁ : ∀ (h : b ≤ c), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases lt_or_ge c b with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
inr : a ^ c - 1 < a ^ b - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rw [mod_eq_of_lt, mod_eq_of_lt h]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
inr : a ^ c < a ^ b
inr₁ inr₂ inr₃ inr₄ : c < b
⊢ a ^ c - 1 < a ^ b - 1

Tactic:
rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]

Premises used: Nat.sub_lt_sub_iff_right, Nat.pow_lt_pow_iff_right, Nat.one_le_pow
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
rw : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
rw₁ : (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₂ : (a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₃ : (a ^ (c - b) * (a ^ b - 1) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₄ :
  (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
      (a ^ b - 1) =
    a ^ ((c - b) % b) - 1
rw₅ :
  (a ^ (c - b) % (a ^ b - 1) * 0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₆ : (0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₇ : (0 + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₈ : (a ^ (c - b) - 1) % (a ^ b - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₉ : (a ^ (c - b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
rw₁₀ rw₁₁ : a ^ ((c - b) % b) - 1 = a ^ ((c - b) % b) - 1
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]

Premises used: Nat.mod_self, Nat.mod_mod, Nat.mul_mod, Nat.add_mod_right, zero_add, MulZeroClass.mul_zero, Nat.sub_add_cancel, Nat.add_mod, Nat.zero_mod
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
inr : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
suffices a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1) by
      rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
inr : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + a ^ (c - b) - 1
inr₁ : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 1
inr₂ : a ^ (c - b) * a ^ b - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 1
inr₃ inr₄ : a ^ (c - b) * a ^ b - 1 = a ^ (c - b) * a ^ b - 1
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)

Tactic:
rw [← Nat.add_sub_assoc (one_le_pow (c - b) a ha0), ← mul_add_one, pow_add,
      Nat.sub_add_cancel (one_le_pow b a ha0)]

Premises used: Nat.add_sub_assoc, HSub.hSub, pow_add, Nat.sub_add_cancel, Nat.one_le_pow, Nat.mul_add_one
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
inl : (HPow.hPow (β := ℕ) a 0 - 1).gcd (a ^ c - 1) = a ^ gcd 0 c - 1
inr : ∀ (hb : b > 0), (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
rcases eq_zero_or_pos b with rfl | hb

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a c : ℕ
⊢ (HPow.hPow (β := ℕ) a 0 - 1).gcd (a ^ c - 1) = a ^ gcd 0 c - 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
hb : b > 0
⊢ c % b < b

Tactic:
replace hb : c % b < b := mod_lt c hb
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
hb : c % b < b
inr : ((a ^ c - 1) % (a ^ b - 1)).gcd (a ^ b - 1) = a ^ b.gcd c - 1
inr₁ : (a ^ (c % b) - 1).gcd (a ^ b - 1) = a ^ b.gcd c - 1
inr₂ : a ^ (c % b).gcd b - 1 = a ^ b.gcd c - 1
inr₃ inr₄ : a ^ b.gcd c - 1 = a ^ b.gcd c - 1
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
rw [gcd_rec, pow_sub_one_mod_pow_sub_one, pow_sub_one_gcd_pow_sub_one, ← gcd_rec]

Premises used: Nat.pow_sub_one_mod_pow_sub_one, Nat.gcd_rec
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b : ℕ
h : a ∣ b
c : ℕ
⊢ a ∣ b.lcm c

Tactic:
h.trans (dvd_lcm_left b c)

Premises used: Nat.dvd_lcm_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
h : a.lcm b ∣ c
⊢ a ∣ c

Tactic:
(dvd_lcm_left a b).trans h

Premises used: Nat.dvd_lcm_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b : ℕ
h : a ∣ b
c : ℕ
⊢ a ∣ c.lcm b

Tactic:
h.trans (dvd_lcm_right c b)

Premises used: Nat.dvd_lcm_right, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
h : a.lcm b ∣ c
⊢ b ∣ c

Tactic:
(dvd_lcm_right a b).trans h

Premises used: Nat.dvd_lcm_right, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
h : m.Coprime n
rw : 1 * m.lcm n = m * n
rw₁ : m.gcd n * m.lcm n = m * n
rw₂ rw₃ : m * n = m * n
⊢ m.lcm n = m * n

Tactic:
rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]

Premises used: Nat.lcm, Nat.gcd_mul_lcm, Nat.Coprime.gcd_eq_one, one_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
⊢ Symmetric Coprime

Tactic:
fun _ _ => Coprime.symm

Premises used: Nat.Coprime.symm, Symmetric
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
H : k.Coprime n
⊢ k ∣ m * n ↔ k ∣ m

Tactic:
⟨H.dvd_of_dvd_mul_right, fun h => dvd_mul_of_dvd_left h n⟩

Premises used: dvd_mul_of_dvd_left, Iff.intro, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
H : k.Coprime m
⊢ k ∣ m * n ↔ k ∣ n

Tactic:
⟨H.dvd_of_dvd_mul_left, fun h => dvd_mul_of_dvd_right h m⟩

Premises used: dvd_mul_of_dvd_right, Iff.intro, Nat.Coprime.dvd_of_dvd_mul_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
rw : m.gcd (n + m) = 1 ↔ m.Coprime n
rw₁ : m.gcd (n + m) = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ m.Coprime (n + m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_self_right]

Premises used: Nat.Coprime, Nat.gcd_add_self_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
rw : m.Coprime (n + m) ↔ m.Coprime n
rw₁ rw₂ : m.Coprime n ↔ m.Coprime n
⊢ m.Coprime (m + n) ↔ m.Coprime n

Tactic:
rw [add_comm, coprime_add_self_right]

Premises used: add_comm, Nat.coprime_add_self_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
rw : (m + n).gcd n = 1 ↔ m.Coprime n
rw₁ : (m + n).gcd n = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ (m + n).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_self_left]

Premises used: Nat.Coprime, Nat.gcd_add_self_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
rw : (m + n).gcd m = 1 ↔ n.Coprime m
rw₁ : (m + n).gcd m = 1 ↔ n.gcd m = 1
rw₂ rw₃ : n.gcd m = 1 ↔ n.gcd m = 1
⊢ (m + n).Coprime m ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_self_add_left]

Premises used: Nat.Coprime, Nat.gcd_self_add_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : m.gcd (n + k * m) = 1 ↔ m.Coprime n
rw₁ : m.gcd (n + k * m) = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ m.Coprime (n + k * m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_mul_right_right]

Premises used: Nat.Coprime, Nat.gcd_add_mul_right_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : m.gcd (n + m * k) = 1 ↔ m.Coprime n
rw₁ : m.gcd (n + m * k) = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ m.Coprime (n + m * k) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_mul_left_right]

Premises used: Nat.Coprime, Nat.gcd_add_mul_left_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : m.gcd (k * m + n) = 1 ↔ m.Coprime n
rw₁ : m.gcd (k * m + n) = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ m.Coprime (k * m + n) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_right_add_right]

Premises used: Nat.Coprime, Nat.gcd_mul_right_add_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : m.gcd (m * k + n) = 1 ↔ m.Coprime n
rw₁ : m.gcd (m * k + n) = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ m.Coprime (m * k + n) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_left_add_right]

Premises used: Nat.Coprime, Nat.gcd_mul_left_add_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : (m + k * n).gcd n = 1 ↔ m.Coprime n
rw₁ : (m + k * n).gcd n = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ (m + k * n).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_mul_right_left]

Premises used: Nat.Coprime, Nat.gcd_add_mul_right_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : (m + n * k).gcd n = 1 ↔ m.Coprime n
rw₁ : (m + n * k).gcd n = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ (m + n * k).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_mul_left_left]

Premises used: Nat.Coprime, Nat.gcd_add_mul_left_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : (k * n + m).gcd n = 1 ↔ m.Coprime n
rw₁ : (k * n + m).gcd n = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ (k * n + m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_right_add_left]

Premises used: Nat.Coprime, Nat.gcd_mul_right_add_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n k : ℕ
rw : (n * k + m).gcd n = 1 ↔ m.Coprime n
rw₁ : (n * k + m).gcd n = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ (n * k + m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_left_add_left]

Premises used: Nat.Coprime, Nat.gcd_mul_left_add_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
h : c ∣ b
obtain : ∀ (n : ℕ), (a + c * n).Coprime c ↔ a.Coprime c
⊢ (a + b).Coprime c ↔ a.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
h : c ∣ a
obtain : ∀ (n : ℕ), (c * n + b).Coprime c ↔ b.Coprime c
⊢ (a + b).Coprime c ↔ b.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
h : a ∣ c
obtain : ∀ (n : ℕ), a.Coprime (b + a * n) ↔ a.Coprime b
⊢ a.Coprime (b + c) ↔ a.Coprime b

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
h : a ∣ b
obtain : ∀ (n : ℕ), a.Coprime (a * n + c) ↔ a.Coprime c
⊢ a.Coprime (b + c) ↔ a.Coprime c

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a₁ a₂ b : ℕ
ha : a₁ ∣ a₂
h : a₂.Coprime b
⊢ a₁.Coprime b

Tactic:
h.coprime_dvd_left ha

Premises used: Nat.Coprime.coprime_dvd_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b₁ b₂ : ℕ
hb : b₁ ∣ b₂
h : a.Coprime b₂
⊢ a.Coprime b₁

Tactic:
h.coprime_dvd_right hb

Premises used: Nat.Coprime.coprime_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a₁ a₂ b₁ b₂ : ℕ
ha : a₁ ∣ a₂
hb : b₁ ∣ b₂
h : a₂.Coprime b₂
⊢ a₁.Coprime b₁

Tactic:
(h.of_dvd_left ha).of_dvd_right hb

Premises used: Nat.Coprime.of_dvd_left, Nat.Coprime.of_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
h : m ≤ n
rw : (n - m).gcd m = 1 ↔ n.Coprime m
rw₁ : (n - m).gcd m = 1 ↔ n.gcd m = 1
rw₂ rw₃ : n.gcd m = 1 ↔ n.gcd m = 1
⊢ (n - m).Coprime m ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_sub_self_left h]

Premises used: Nat.Coprime, Nat.gcd_sub_self_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
h : m ≤ n
rw : m.gcd (n - m) = 1 ↔ m.Coprime n
rw₁ : m.gcd (n - m) = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ m.Coprime (n - m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_sub_self_right h]

Premises used: Nat.Coprime, Nat.gcd_sub_self_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
h : m ≤ n
rw : (n - m).gcd n = 1 ↔ m.Coprime n
rw₁ : (n - m).gcd n = 1 ↔ m.gcd n = 1
rw₂ rw₃ : m.gcd n = 1 ↔ m.gcd n = 1
⊢ (n - m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_self_sub_left h]

Premises used: Nat.Coprime, Nat.gcd_self_sub_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
h : m ≤ n
rw : n.gcd (n - m) = 1 ↔ n.Coprime m
rw₁ : n.gcd (n - m) = 1 ↔ n.gcd m = 1
rw₂ rw₃ : n.gcd m = 1 ↔ n.gcd m = 1
⊢ n.Coprime (n - m) ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_self_sub_right h]

Premises used: Nat.Coprime, Nat.gcd_self_sub_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n : ℕ
hn : 0 < n
a b : ℕ
obtain : ∀ (n : ℕ) (hn : 0 < n.succ), (a ^ n.succ).Coprime b ↔ a.Coprime b
⊢ (a ^ n).Coprime b ↔ a.Coprime b

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b n : ℕ
hn : 0 < n.succ
rw : (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b
⊢ (a ^ n.succ).Coprime b ↔ a.Coprime b

Tactic:
rw [Nat.pow_succ, Nat.coprime_mul_iff_left]

Premises used: Nat.coprime_mul_iff_left, Nat.pow_succ
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b

Tactic:
⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩

Premises used: Nat.Coprime.pow_left, And.right, And.intro, Iff.intro
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b

Tactic:
exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n : ℕ
hn : 0 < n
a b : ℕ
rw : (b ^ n).Coprime a ↔ a.Coprime b
rw₁ : b.Coprime a ↔ a.Coprime b
rw₂ rw₃ : a.Coprime b ↔ a.Coprime b
⊢ a.Coprime (b ^ n) ↔ a.Coprime b

Tactic:
rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]

Premises used: Nat.coprime_comm, Nat.coprime_pow_left_iff
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
⊢ ¬Coprime 0 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n : ℕ
⊢ Coprime 1 n ↔ True

Tactic:
simp [Coprime]

Premises used: Nat.Coprime
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n : ℕ
⊢ n.Coprime 1 ↔ True

Tactic:
simp [Coprime]

Premises used: Nat.Coprime