awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b c : ℕ
hac : a.Coprime c
b_dvd_c : b ∣ c
rcases : ∀ (d : ℕ) (hac : a.Coprime (d * b)) (b_dvd_c : b ∣ d * b), (a * b).gcd (d * b) = b
⊢ (a * b).gcd c = b

Tactic:
rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩

Premises used: exists_eq_mul_left_of_dvd, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
rw : a.gcd d * b = b
⊢ (a * b).gcd (d * b) = b

Tactic:
rw [gcd_mul_right]

Premises used: Nat.gcd_mul_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ 1 * b = b

Tactic:
one_mul b

Premises used: one_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
h : a.gcd d = 1
⊢ a.gcd d * b = b

Tactic:
convert! one_mul b

Premises used: one_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d = 1

Tactic:
Coprime.coprime_mul_right_right hac

Premises used: Nat.Coprime.coprime_mul_right_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d = 1

Tactic:
exact Coprime.coprime_mul_right_right hac

Premises used: Nat.Coprime.coprime_mul_right_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
h : m.Coprime n
hmn : m * n = 0
⊢ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

Tactic:
(Nat.mul_eq_zero.mp hmn).imp (fun hm => ⟨hm, n.coprime_zero_left.mp <| hm ▸ h⟩) fun hn =>
    let eq := hn ▸ h.symm
    ⟨m.coprime_zero_left.mp <| eq, hn⟩

Premises used: Eq.rec, And.intro, Nat.coprime_zero_left, Iff.mp, Or.imp, Nat.mul_eq_zero
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
simp_rw : m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1
⊢ m.Coprime n ↔ IsRelPrime m n

Tactic:
simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]

Premises used: Nat.dvd_gcd_iff, and_imp, IsRelPrime, Nat.coprime_iff_gcd_eq_one, isUnit_iff_dvd_one
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1

Tactic:
⟨fun h _ ↦ (h ▸ ·), (dvd_one.mp <| · dvd_rfl)⟩

Premises used: Nat.dvd_one, Eq.rec, Iff.intro, Iff.mp, dvd_rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1

Tactic:
exact ⟨fun h _ ↦ (h ▸ ·), (dvd_one.mp <| · dvd_rfl)⟩
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
a b k : ℕ
h_ab_coprime : a.Coprime b
hka : k ∣ a
hkb : k ∣ b
⊢ k = 1

Tactic:
dvd_one.mp (isUnit_iff_dvd_one.mp <| coprime_iff_isRelPrime.mp h_ab_coprime hka hkb)

Premises used: Nat.dvd_one, Iff.mp, isUnit_iff_dvd_one, Nat.coprime_iff_isRelPrime
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ n ∣ a

Tactic:
cop.symm.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))

Premises used: Iff.mpr, Eq.mpr, Nat.Coprime.symm, congr_arg, Nat.dvd_mul_left, Nat.dvd_add_iff_left, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
obtain : ∀ (x : ℕ) (ha : n * x ≠ 0) (h : n * x * m + b * n = m * n), False
⊢ False

Tactic:
obtain ⟨x, rfl⟩ : n ∣ a :=
    cop.symm.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))

Premises used: Iff.mpr, Eq.mpr, Nat.Coprime.symm, congr_arg, Nat.dvd_mul_left, Nat.dvd_add_iff_left, Nat.Coprime.dvd_of_dvd_mul_right, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n b : ℕ
cop : m.Coprime n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ m ∣ b

Tactic:
cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))

Premises used: Iff.mpr, Eq.mpr, HMul.hMul, congr_arg, Nat.dvd_mul_right, Nat.dvd_mul_left, Nat.dvd_add_iff_right, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n b : ℕ
cop : m.Coprime n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
obtain : ∀ (y : ℕ) (hb : m * y ≠ 0) (h : n * x * m + m * y * n = m * n), False
⊢ False

Tactic:
obtain ⟨y, rfl⟩ : m ∣ b :=
    cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))

Premises used: Iff.mpr, Eq.mpr, HMul.hMul, congr_arg, Nat.dvd_mul_right, Nat.dvd_mul_left, Nat.dvd_add_iff_right, Nat.Coprime.dvd_of_dvd_mul_right, rfl
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
rw : ∀ (ha : 1 ≤ x ∧ n ≠ 0) (y : ℕ) (hb : 1 ≤ y ∧ m ≠ 0) (h : n * x * m + m * y * n = m * n), False
⊢ False

Tactic:
rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb

Premises used: mul_comm, Nat.one_le_iff_ne_zero, mul_ne_zero_iff
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False

Tactic:
mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)

Premises used: eq_zero_of_mul_eq_self_left, And.right, And.left, Nat.add_le_add, mul_ne_zero, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
refine : (x + y) * (m * n) = m * n
⊢ False

Tactic:
refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)

Premises used: eq_zero_of_mul_eq_self_left, And.right, And.left, Nat.add_le_add, mul_ne_zero, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
rw₁ : (x + y) * m * n = n * x * m + m * y * n
rw₂ : (x * m + y * m) * n = n * x * m + m * y * n
rw₃ : x * m * n + y * m * n = n * x * m + m * y * n
rw₄ : n * (x * m) + y * m * n = n * x * m + m * y * n
rw₅ : n * x * m + y * m * n = n * x * m + m * y * n
rw₆ rw₇ : n * x * m + m * y * n = n * x * m + m * y * n
⊢ (x + y) * (m * n) = m * n

Tactic:
rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]

Premises used: mul_assoc, mul_comm, Nat.add_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
⊢ x.gcd n * x.gcd m = x ↔ x ∣ n * m

Tactic:
⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩

Premises used: Iff.mpr, dvd_antisymm, Nat.dvd_gcd_mul_gcd_iff_dvd_mul, Iff.intro
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
refine_1 : ∀ (h : x.gcd n * x.gcd m = x), x ∣ n * m
refine_2 : x ∣ n * m → x.gcd n * x.gcd m ∣ x
⊢ x.gcd n * x.gcd m = x ↔ x ∣ n * m

Tactic:
refine ⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x ∣ n * m

Tactic:
h ▸ Nat.mul_dvd_mul ?_ ?_

Premises used: Eq.rec, Nat.mul_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
refine_1 : x.gcd n ∣ n
refine_1₁ : x.gcd m ∣ m
⊢ x ∣ n * m

Tactic:
refine h ▸ Nat.mul_dvd_mul ?_ ?_
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd n ∣ n

Tactic:
x.gcd_dvd_right _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd n ∣ n

Tactic:
exact x.gcd_dvd_right _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd m ∣ m

Tactic:
x.gcd_dvd_right _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x.gcd m ∣ m

Tactic:
exact x.gcd_dvd_right _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x

Tactic:
(hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_

Premises used: Nat.Coprime.mul_dvd_of_dvd_of_dvd, Nat.Coprime.gcd_both
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
refine_2 : x.gcd n ∣ x
refine_2₁ : x.gcd m ∣ x
⊢ x.gcd n * x.gcd m ∣ x

Tactic:
refine (hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_

Premises used: Nat.Coprime.mul_dvd_of_dvd_of_dvd, Nat.Coprime.gcd_both
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
⊢ x.gcd n ∣ x

Tactic:
x.gcd_dvd_left _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
⊢ x.gcd n ∣ x

Tactic:
exact x.gcd_dvd_left _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
⊢ x.gcd m ∣ x

Tactic:
x.gcd_dvd_left _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
⊢ x.gcd m ∣ x

Tactic:
exact x.gcd_dvd_left _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
inl : ∀ (hn : n = 0), k / m * (m / n) = k / n
inr : ∀ (hn : n > 0), k / m * (m / n) = k / n
⊢ k / m * (m / n) = k / n

Tactic:
rcases n.eq_zero_or_pos with hn | hn

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n = 0
⊢ k / m * (m / n) = k / n

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k / m * (m / n) = k / n

Tactic:
(Nat.div_eq_of_eq_mul_left hn ?_).symm

Premises used: Nat.div_eq_of_eq_mul_left, Eq.symm
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
inr : k = k / m * (m / n) * n
⊢ k / m * (m / n) = k / n

Tactic:
refine (Nat.div_eq_of_eq_mul_left hn ?_).symm

Premises used: Nat.div_eq_of_eq_mul_left, Eq.symm
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
inr : k = k / m * (m / n * n)
inr₁ : k = k / m * m
inr₂ inr₃ : k = k
⊢ k = k / m * (m / n) * n

Tactic:
rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]

Premises used: Nat.div_mul_cancel, mul_assoc
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
⊢ k / m ∣ k / n

Tactic:
⟨_, (div_mul_div hkm hkn).symm⟩

Premises used: Exists.intro, Nat.div_mul_div, Eq.symm
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
rw : k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c
⊢ (k / m).lcm (k / n) = k / m.gcd n

Tactic:
rw [Nat.lcm_eq_iff]

Premises used: Nat.lcm_eq_iff
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c

Tactic:
⟨div_dvd_div_left hkm (Nat.gcd_dvd_left m n),
        div_dvd_div_left hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ ?_⟩

Premises used: Nat.gcd_dvd_left, Nat.div_dvd_div_left, And.intro, Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
refine : ∀ (c : ℕ) (hmc : k / m ∣ c) (hnc : k / n ∣ c), k / m.gcd n ∣ c
⊢ k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c

Tactic:
refine ⟨div_dvd_div_left hkm (Nat.gcd_dvd_left m n),
        div_dvd_div_left hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ ?_⟩
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
inl : ∀ (hm : m = 0), k / m.gcd n ∣ c
inr : ∀ (hm : m > 0), k / m.gcd n ∣ c
⊢ k / m.gcd n ∣ c

Tactic:
rcases m.eq_zero_or_pos with hm | hm

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m = 0
⊢ k / m.gcd n ∣ c

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
inr : ∀ (hn : n = 0), k / m.gcd n ∣ c
inr₁ : ∀ (hn : n > 0), k / m.gcd n ∣ c
⊢ k / m.gcd n ∣ c

Tactic:
rcases n.eq_zero_or_pos with hn | hn

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n = 0
⊢ k / m.gcd n ∣ c

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k ∣ m * c

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
hmc₁ : k ∣ m * c
⊢ k / n ∣ c

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
hmc₁ : k ∣ m * c
hnc₁ : k / n ∣ c
⊢ m > 0

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
hmc₁ : k ∣ m * c
hnc₁ : k / n ∣ c
hm₁ : m > 0
⊢ n > 0

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k ∣ n * c

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
hnc₁ : k ∣ n * c
⊢ m > 0

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
hnc₁ : k ∣ n * c
hm₁ : m > 0
⊢ n > 0

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc

Premises used: Nat.div_dvd_iff_dvd_mul
-- Module: Mathlib.Data.Nat.GCD.Basic
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k ∣ n * c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c

Tactic:
simpa [Nat.div_dvd_iff_dvd_mul (Nat.dvd_trans (Nat.gcd_dvd_left m n) hkm)
    (gcd_pos_of_pos_left n hm), Nat.gcd_mul_right m c n] using (Nat.dvd_gcd hmc hnc)

Premises used: Nat.gcd_dvd_left, Nat.gcd_mul_right, Nat.dvd_trans, Nat.div_dvd_iff_dvd_mul, Nat.gcd_pos_of_pos_left, Nat.dvd_gcd
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
l : List ℕ
k : ℕ
nil : Coprime (List.prod []) k ↔ ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n.Coprime k
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (tail.prod.Coprime k ↔ ∀ n ∈ tail, n.Coprime k) → ((head :: tail).prod.Coprime k ↔ ∀ n ∈ head :: tail, n.Coprime k)
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k

Tactic:
induction l
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
k : ℕ
⊢ Coprime (List.prod []) k ↔ ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n.Coprime k

Tactic:
simp [Nat.coprime_mul_iff_left, *]

Premises used: Nat.coprime_mul_iff_left
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
k head : ℕ
tail : List ℕ
tail_ih : tail.prod.Coprime k ↔ ∀ n ∈ tail, n.Coprime k
⊢ (head :: tail).prod.Coprime k ↔ ∀ n ∈ head :: tail, n.Coprime k

Tactic:
simp [Nat.coprime_mul_iff_left, *]

Premises used: Nat.coprime_mul_iff_left
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
k : ℕ
l : List ℕ
simp_rw : l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
⊢ k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n

Tactic:
simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]

Premises used: Nat.coprime_comm, Nat.coprime_list_prod_left_iff
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
m : Multiset ℕ
k : ℕ
h : ∀ (a : List ℕ), (Multiset.prod ⟦a⟧).Coprime k ↔ ∀ n ∈ ⟦a⟧, n.Coprime k
⊢ m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k

Tactic:
induction m using Quotient.inductionOn
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
k : ℕ
a : List ℕ
⊢ (Multiset.prod ⟦a⟧).Coprime k ↔ ∀ n ∈ ⟦a⟧, n.Coprime k

Tactic:
simpa using coprime_list_prod_left_iff

Premises used: Nat.coprime_list_prod_left_iff
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
k : ℕ
m : Multiset ℕ
h : ∀ (a : List ℕ), k.Coprime (Multiset.prod ⟦a⟧) ↔ ∀ n ∈ ⟦a⟧, k.Coprime n
⊢ k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n

Tactic:
induction m using Quotient.inductionOn
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
k : ℕ
a : List ℕ
⊢ k.Coprime (Multiset.prod ⟦a⟧) ↔ ∀ n ∈ ⟦a⟧, k.Coprime n

Tactic:
simpa using coprime_list_prod_right_iff

Premises used: Nat.coprime_list_prod_right_iff
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
ι : Type u_1
t : Finset ι
s : ι → ℕ
x : ℕ
⊢ Coprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, (s i).Coprime x

Tactic:
simpa using coprime_multiset_prod_left_iff (m := t.val.map s)

Premises used: Nat.coprime_multiset_prod_left_iff
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
ι : Type u_1
x : ℕ
t : Finset ι
s : ι → ℕ
⊢ x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)

Tactic:
simpa using coprime_multiset_prod_right_iff (m := t.val.map s)

Premises used: Nat.coprime_multiset_prod_right_iff
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
ι : Type u_1
inst : Fintype ι
s : ι → ℕ
x : ℕ
⊢ Coprime (∏ i : ι, s i) x ↔ ∀ (i : ι), (s i).Coprime x

Tactic:
simp [coprime_prod_left_iff]

Premises used: Nat.coprime_prod_left_iff
-- Module: Mathlib.Data.Nat.GCD.BigOperators
Goal:
ι : Type u_1
inst : Fintype ι
x : ℕ
s : ι → ℕ
⊢ x.Coprime (∏ i : ι, s i) ↔ ∀ (i : ι), x.Coprime (s i)

Tactic:
simp [coprime_prod_right_iff]

Premises used: Nat.coprime_prod_right_iff
-- Module: Mathlib.Data.Nat.GCD.Prime
Goal:
p a b : ℕ
hp : Prime p
h : p ∣ a.lcm b
⊢ p ∣ a ∨ p ∣ b

Tactic:
dvd_or_dvd hp (h.trans (lcm_dvd_mul a b))

Premises used: Nat.Prime.dvd_or_dvd, Nat.lcm_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.GCD.Prime
Goal:
p a b : ℕ
hp : Prime p
⊢ p ∣ a.lcm b ↔ p ∣ a ∨ p ∣ b

Tactic:
⟨hp.dvd_or_dvd_of_dvd_lcm, (Or.elim · (dvd_lcm_of_dvd_left · _) (dvd_lcm_of_dvd_right · _))⟩

Premises used: Nat.dvd_lcm_of_dvd_left, Iff.intro, Or.elim, Nat.dvd_lcm_of_dvd_right, Nat.Prime.dvd_or_dvd_of_dvd_lcm
-- Module: Mathlib.Data.Nat.GCD.Prime
Goal:
p a b : ℕ
hp : Prime p
ha : ¬p ∣ a
hb : ¬p ∣ b
⊢ ¬p ∣ a.lcm b

Tactic:
hp.dvd_lcm.not.mpr <| not_or.mpr ⟨ha, hb⟩

Premises used: Nat.Prime.dvd_lcm, Iff.mpr, Iff.not, not_or, And.intro
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m k : ℕ
⊢ hyperoperation 0 m k = k + 1

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n m : ℕ
⊢ hyperoperation (n + 3) m 0 = 1

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n m k : ℕ
⊢ hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m : ℕ
⊢ hyperoperation 1 m 0 = m + 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m n : ℕ
h : hyperoperation 1 m n = m + n
⊢ hyperoperation 1 m (n + 1) = m + (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m k : ℕ
zero : hyperoperation 1 m 0 = m + 0
succ : ∀ (n : ℕ), hyperoperation 1 m n = m + n → hyperoperation 1 m (n + 1) = m + (n + 1)
⊢ hyperoperation 1 m k = m + k

Tactic:
induction k with grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m : ℕ
⊢ hyperoperation 2 m 0 = m * 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m n : ℕ
h : hyperoperation 2 m n = m * n
⊢ hyperoperation 2 m (n + 1) = m * (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m k : ℕ
zero : hyperoperation 2 m 0 = m * 0
succ : ∀ (n : ℕ), hyperoperation 2 m n = m * n → hyperoperation 2 m (n + 1) = m * (n + 1)
⊢ hyperoperation 2 m k = m * k

Tactic:
induction k with grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m : ℕ
⊢ hyperoperation 3 m 0 = HPow.hPow (β := ℕ) m 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m n : ℕ
h : hyperoperation 3 m n = m ^ n
⊢ hyperoperation 3 m (n + 1) = m ^ (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m k : ℕ
zero : hyperoperation 3 m 0 = HPow.hPow (β := ℕ) m 0
succ : ∀ (n : ℕ), hyperoperation 3 m n = m ^ n → hyperoperation 3 m (n + 1) = m ^ (n + 1)
⊢ hyperoperation 3 m k = m ^ k

Tactic:
induction k with grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m : ℕ
⊢ hyperoperation (HAdd.hAdd (α := ℕ) 0 2) m 1 = m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
m n : ℕ
h : hyperoperation (n + 2) m 1 = m
⊢ hyperoperation (n + 1 + 2) m 1 = m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n m : ℕ
zero : hyperoperation (HAdd.hAdd (α := ℕ) 0 2) m 1 = m
succ : ∀ (n : ℕ), hyperoperation (n + 2) m 1 = m → hyperoperation (n + 1 + 2) m 1 = m
⊢ hyperoperation (n + 2) m 1 = m

Tactic:
induction n with grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
⊢ hyperoperation (HAdd.hAdd (α := ℕ) 0 1) 2 2 = 4

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n : ℕ
h : hyperoperation (n + 1) 2 2 = 4
⊢ hyperoperation (n + 1 + 1) 2 2 = 4

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n : ℕ
zero : hyperoperation (HAdd.hAdd (α := ℕ) 0 1) 2 2 = 4
succ : ∀ (n : ℕ), hyperoperation (n + 1) 2 2 = 4 → hyperoperation (n + 1 + 1) 2 2 = 4
⊢ hyperoperation (n + 1) 2 2 = 4

Tactic:
induction n with grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
k : ℕ
⊢ hyperoperation (HAdd.hAdd (α := ℕ) 0 3) 1 k = 1

Tactic:
grind [cases Nat]

Premises used: Nat
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n : ℕ
h : ∀ (k : ℕ), hyperoperation (n + 3) 1 k = 1
k : ℕ
⊢ hyperoperation (n + 1 + 3) 1 k = 1

Tactic:
grind [cases Nat]

Premises used: Nat
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n k : ℕ
zero : ∀ (k : ℕ), hyperoperation (HAdd.hAdd (α := ℕ) 0 3) 1 k = 1
succ : ∀ (n : ℕ), (∀ (k : ℕ), hyperoperation (n + 3) 1 k = 1) → ∀ (k : ℕ), hyperoperation (n + 1 + 3) 1 k = 1
⊢ hyperoperation (n + 3) 1 k = 1

Tactic:
induction n generalizing k with grind [cases Nat]

Premises used: Nat
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n : ℕ
⊢ hyperoperation (n + 4) 0 0 = if Even (α := ℕ) 0 then 1 else 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n n_1 : ℕ
h : hyperoperation (n + 4) 0 n_1 = if Even n_1 then 1 else 0
⊢ hyperoperation (n + 4) 0 (n_1 + 1) = if Even (n_1 + 1) then 1 else 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Hyperoperation
Goal:
n k : ℕ
zero : hyperoperation (n + 4) 0 0 = if Even (α := ℕ) 0 then 1 else 0
succ :
  ∀ (n_1 : ℕ),
    (hyperoperation (n + 4) 0 n_1 = if Even n_1 then 1 else 0) →
      hyperoperation (n + 4) 0 (n_1 + 1) = if Even (n_1 + 1) then 1 else 0
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0

Tactic:
induction k with grind
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
⊢ 0 < n.succ

Tactic:
succ_pos n

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Init
Goal:
⊢ LE.le (α := ℕ) 2 0 ↔ Ne (α := ℕ) 0 0 ∧ Ne (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Init
Goal:
⊢ LE.le (α := ℕ) 2 1 ↔ Ne (α := ℕ) 1 0 ∧ Ne (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
⊢ 2 ≤ n + 2 ↔ n + 2 ≠ 0 ∧ n + 2 ≠ 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
⊢ m.mul n = m * n

Tactic:
mul_eq

Premises used: Nat.mul_eq
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
rw : ¬Eq (α := ℕ) 0 1
rw₁ : LT.lt (α := ℕ) 1 2
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt]

Premises used: Nat.mod_eq_of_lt, Nat.mul_mod_right, Nat.add_mul_mod_self_left, Nat.add_comm
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
⊢ ¬Eq (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Init
Goal:
m n : ℕ
⊢ LT.lt (α := ℕ) 1 2

Tactic:
simp