awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.GCD
Goal:
k n r : ℕ
hkn : n.Coprime k
hk_1 : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
right : n % k * (m * r % k % k) % k = r % k
right₁ : n % k * (m * r % k) % k = r % k
right₂ : n * (m * r) % k = r % k
right₃ : n * m * r % k = r % k
right₄ : n * m % k * (r % k) % k = r % k
right₅ : 1 * (r % k) % k = r % k
right₆ : r % k % k = r % k
right₇ right₈ : r % k = r % k
⊢ n * (m * r % k) % k = r % k

Tactic:
rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]

Premises used: Nat.mod_mod, mul_assoc, Nat.mul_mod, one_mul
-- Module: Mathlib.Data.Int.GCD
Goal:
i j : ℤ
⊢ i.gcd j = i.natAbs.gcd j.natAbs

Tactic:
rfl

Premises used: Int.gcd, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℕ
rw :
  (↑(gcd (↑m : ℤ) -[n+1]) : ℤ) =
    (↑m : ℤ) * gcdA (↑m : ℤ) -[n+1] + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (natAbs (↑m : ℤ)).gcdB n.succ
⊢ (↑(gcd (↑m : ℤ) -[n+1]) : ℤ) =
    (↑m : ℤ) * gcdA (↑m : ℤ) -[n+1] + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * -(natAbs (↑m : ℤ)).gcdB n.succ

Tactic:
rw [Int.neg_mul_neg]

Premises used: Int.neg_mul_neg
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℕ
⊢ (↑(gcd (↑m : ℤ) -[n+1]) : ℤ) =
    (↑m : ℤ) * gcdA (↑m : ℤ) -[n+1] + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (natAbs (↑m : ℤ)).gcdB n.succ

Tactic:
apply Nat.gcd_eq_gcd_ab

Premises used: Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℕ
rw :
  (↑(-[m+1].gcd (↑n : ℤ)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * m.succ.gcdA (natAbs (↑n : ℤ)) + (↑n : ℤ) * -[m+1].gcdB (↑n : ℤ)
⊢ (↑(-[m+1].gcd (↑n : ℤ)) : ℤ) =
    -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * -m.succ.gcdA (natAbs (↑n : ℤ)) + (↑n : ℤ) * -[m+1].gcdB (↑n : ℤ)

Tactic:
rw [Int.neg_mul_neg]

Premises used: Int.neg_mul_neg
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℕ
⊢ (↑(-[m+1].gcd (↑n : ℤ)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * m.succ.gcdA (natAbs (↑n : ℤ)) + (↑n : ℤ) * -[m+1].gcdB (↑n : ℤ)

Tactic:
apply Nat.gcd_eq_gcd_ab

Premises used: Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℕ
rw :
  (↑(-[m+1].gcd -[n+1]) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * m.succ.gcdA -[n+1].natAbs +
      HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * -[m+1].natAbs.gcdB n.succ
⊢ (↑(-[m+1].gcd -[n+1]) : ℤ) =
    -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * -m.succ.gcdA -[n+1].natAbs +
      -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * - -[m+1].natAbs.gcdB n.succ

Tactic:
rw [Int.neg_mul_neg, Int.neg_mul_neg]

Premises used: Int.neg_mul_neg
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℕ
⊢ (↑(-[m+1].gcd -[n+1]) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * m.succ.gcdA -[n+1].natAbs +
      HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * -[m+1].natAbs.gcdB n.succ

Tactic:
apply Nat.gcd_eq_gcd_ab

Premises used: Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
i j : ℤ
⊢ i.lcm j = i.natAbs.lcm j.natAbs

Tactic:
rfl

Premises used: Int.lcm, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
a : ℤ
m n : ℕ
h : a.gcd (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) = 1
⊢ a.gcd (↑m : ℤ) = 1

Tactic:
Nat.dvd_one.mp <| h ▸ gcd_dvd_gcd_mul_right_right a m n

Premises used: Nat.dvd_one, Eq.rec, Nat.cast, Iff.mp, Int.gcd_dvd_gcd_mul_right_right
-- Module: Mathlib.Data.Int.GCD
Goal:
a : ℤ
m n : ℕ
h : a.gcd (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) = 1
⊢ a.gcd (↑n : ℤ) = 1

Tactic:
Nat.dvd_one.mp <| h ▸ gcd_dvd_gcd_mul_left_right a n m

Premises used: Nat.dvd_one, Eq.rec, Nat.cast, Iff.mp, Int.gcd_dvd_gcd_mul_left_right
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℤ
hc : x.gcd y ≠ 0
contrapose! : ∀ (hc : x = 0 ∧ y = 0), x.gcd y = 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
contrapose! hc
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℤ
hc : x = 0 ∧ y = 0
rw : gcd 0 y = 0
rw₁ : gcd 0 0 = 0
rw₂ : natAbs 0 = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ x.gcd y = 0

Tactic:
rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]

Premises used: Int.natAbs_zero, And.right, And.left, Int.gcd_zero_right
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℤ
H : 0 < m.gcd n
⊢ ∃ (m' : ℤ), ∃ (n' : ℤ), m'.gcd n' = 1 ∧ m = m' * (↑(m.gcd n) : ℤ) ∧ n = n' * (↑(m.gcd n) : ℤ)

Tactic:
⟨_, _, gcd_div_gcd_div_gcd H, (Int.ediv_mul_cancel (gcd_dvd_left ..)).symm,
    (Int.ediv_mul_cancel (gcd_dvd_right ..)).symm⟩

Premises used: Int.ediv_mul_cancel, Int.gcd_dvd_left, And.intro, Exists.intro, Int.gcd_dvd_right, Eq.symm, Int.gcd_div_gcd_div_gcd
-- Module: Mathlib.Data.Int.GCD
Goal:
m n : ℤ
H : 0 < m.gcd n
⊢ ∃ (g : ℕ), ∃ (m' : ℤ), ∃ (n' : ℤ), 0 < g ∧ m'.gcd n' = 1 ∧ m = m' * (↑g : ℤ) ∧ n = n' * (↑g : ℤ)

Tactic:
let ⟨m', n', h⟩ := exists_gcd_one H
  ⟨_, m', n', H, h⟩

Premises used: Int.gcd, HMul.hMul, Int.exists_gcd_one, Exists, Nat.cast, And, And.intro, LT.lt, Exists.intro, _private.0.Int.exists_gcd_one'.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
mp : a.gcd b ∣ n → ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y
mpr : (∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y) → a.gcd b ∣ n
⊢ a.gcd b ∣ n ↔ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y

Tactic:
constructor
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
mp : ∃ (x : ℤ), ∃ (y : ℤ), a * (a.gcdA b * (↑(n / a.gcd b) : ℤ)) + b * (a.gcdB b * (↑(n / a.gcd b) : ℤ)) = a * x + b * y
⊢ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y

Tactic:
rw [← Nat.mul_div_cancel' h, Int.natCast_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]

Premises used: mul_assoc, Int.natCast_mul, Int.add_mul, Int.gcd_eq_gcd_ab, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ (x : ℤ), ∃ (y : ℤ), a * (a.gcdA b * (↑(n / a.gcd b) : ℤ)) + b * (a.gcdB b * (↑(n / a.gcd b) : ℤ)) = a * x + b * y

Tactic:
⟨_, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ (x : ℤ), ∃ (y : ℤ), a * (a.gcdA b * (↑(n / a.gcd b) : ℤ)) + b * (a.gcdB b * (↑(n / a.gcd b) : ℤ)) = a * x + b * y

Tactic:
exact ⟨_, _, rfl⟩
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
x y : ℤ
h : (↑n : ℤ) = a * x + b * y
mpr : (↑(a.gcd b) : ℤ) ∣ a * x + b * y
⊢ a.gcd b ∣ n

Tactic:
rw [← Int.natCast_dvd_natCast, h]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
x y : ℤ
h : (↑n : ℤ) = a * x + b * y
⊢ (↑(a.gcd b) : ℤ) ∣ a * x + b * y

Tactic:
Int.dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left ..))
      (dvd_mul_of_dvd_left (gcd_dvd_right ..))

Premises used: Int.dvd_mul_of_dvd_left, Int.dvd_add, Int.gcd_dvd_left, Int.gcd_dvd_right
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
n : ℕ
x y : ℤ
h : (↑n : ℤ) = a * x + b * y
⊢ (↑(a.gcd b) : ℤ) ∣ a * x + b * y

Tactic:
exact Int.dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left ..))
      (dvd_mul_of_dvd_left (gcd_dvd_right ..))

Premises used: Int.dvd_mul_of_dvd_left, Int.dvd_add, Int.gcd_dvd_left, Int.gcd_dvd_right
-- Module: Mathlib.Data.Int.GCD
Goal:
a b d : ℤ
hd_pos : 0 ≤ d
hda : d ∣ a
hdb : d ∣ b
hd : ∀ (e : ℤ), e ∣ a → e ∣ b → e ∣ d
⊢ d = (↑(a.gcd b) : ℤ)

Tactic:
dvd_antisymm hd_pos (natCast_nonneg (gcd a b)) (dvd_coe_gcd hda hdb)
    (hd _ (gcd_dvd_left ..) (gcd_dvd_right ..))

Premises used: Int.gcd, Int.dvd_coe_gcd, Int.gcd_dvd_left, Int.gcd_dvd_right, Int.dvd_antisymm, Int.natCast_nonneg
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
⊢ (↑(a.gcd c) : ℤ) = a * a.gcdA c + c * a.gcdB c

Tactic:
have := gcd_eq_gcd_ab a c
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : (↑(a.gcd c) : ℤ) = a * a.gcdA c + c * a.gcdB c
⊢ 1 = a * a.gcdA c + c * a.gcdB c

Tactic:
simp only [hab, Int.ofNat_zero, Int.natCast_succ, zero_add] at this

Premises used: zero_add, Int.ofNat_zero, Int.natCast_succ
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ b * a * a.gcdA c + b * c * a.gcdB c = b

Tactic:
simp [mul_assoc, ← Int.mul_add, ← this]

Premises used: mul_assoc, Int.mul_add
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ b * a * a.gcdA c + b * c * a.gcdB c = b

Tactic:
have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← Int.mul_add, ← this]
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this_1 : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
rw : a ∣ b * a * a.gcdA c + b * c * a.gcdB c
⊢ a ∣ b

Tactic:
rw [← this]
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this_1 : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c

Tactic:
Int.dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b)) (dvd_mul_of_dvd_left habc)

Premises used: Int.dvd_mul_of_dvd_left, Int.dvd_add, dvd_mul_left
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this_1 : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c

Tactic:
exact Int.dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b)) (dvd_mul_of_dvd_left habc)

Premises used: Int.dvd_mul_of_dvd_left, Int.dvd_add, dvd_mul_left
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd b = 1
⊢ a ∣ c * b

Tactic:
rw [mul_comm] at habc

Premises used: mul_comm
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd b = 1
habc₁ : a ∣ c * b
⊢ a.gcd b = 1

Tactic:
rw [mul_comm] at habc

Premises used: mul_comm
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
dvd_of_dvd_mul_left_of_gcd_one habc hab

Premises used: Int.dvd_of_dvd_mul_left_of_gcd_one
-- Module: Mathlib.Data.Int.GCD
Goal:
a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
exact dvd_of_dvd_mul_left_of_gcd_one habc hab

Premises used: Int.dvd_of_dvd_mul_left_of_gcd_one
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
ha : a ≠ 0
simp_rw : IsLeast {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
⊢ IsLeast {n : ℕ | 0 < n ∧ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y} (a.gcd b)

Tactic:
simp_rw [← gcd_dvd_iff]

Premises used: Int.gcd_dvd_iff
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
ha : a ≠ 0
left : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
right : Membership.mem (γ := Set ℕ) (lowerBounds {n : ℕ | 0 < n ∧ a.gcd b ∣ n}) (a.gcd b)
⊢ IsLeast {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)

Tactic:
constructor
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
ha : a ≠ 0
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)

Tactic:
simpa [and_true, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha

Premises used: and_true, Set.mem_setOf_eq, dvd_refl, Int.gcd_pos_of_ne_zero_left
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
ha : a ≠ 0
right : ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → a.gcd b ∣ a_1 → a.gcd b ≤ a_1
⊢ Membership.mem (γ := Set ℕ) (lowerBounds {n : ℕ | 0 < n ∧ a.gcd b ∣ n}) (a.gcd b)

Tactic:
simp only [lowerBounds, and_imp, Set.mem_setOf_eq]

Premises used: lowerBounds, and_imp, Set.mem_setOf_eq
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → a.gcd b ∣ a_1 → a.gcd b ≤ a_1

Tactic:
fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

Premises used: Nat.le_of_dvd
-- Module: Mathlib.Data.Int.GCD
Goal:
a b : ℤ
ha : a ≠ 0
⊢ ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → a.gcd b ∣ a_1 → a.gcd b ≤ a_1

Tactic:
exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

Premises used: Nat.le_of_dvd
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
left : a ^ m = 1
right : a ^ n = 1
⊢ a ^ m = 1 ∧ a ^ n = 1

Tactic:
constructor
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
left : a ^ (m.gcd n * (m / m.gcd n)) = 1
left₁ : (a ^ m.gcd n) ^ (m / m.gcd n) = 1
left₂ : HPow.hPow (α := M) 1 (m / m.gcd n) = 1
left₃ left₄ : Eq.{u_1 + 1} (α := M) 1 1
⊢ a ^ m = 1

Tactic:
rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]

Premises used: one_pow, Nat.gcd_dvd_left, pow_mul, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
right : a ^ (m.gcd n * (n / m.gcd n)) = 1
right₁ : (a ^ m.gcd n) ^ (n / m.gcd n) = 1
right₂ : HPow.hPow (α := M) 1 (n / m.gcd n) = 1
right₃ right₄ : Eq.{u_1 + 1} (α := M) 1 1
⊢ a ^ n = 1

Tactic:
rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]

Premises used: one_pow, pow_mul, Nat.gcd_dvd_right, Nat.mul_div_cancel'
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hm : a ^ m = 1
hn : a ^ n = 1
zero : ∀ (hm : HPow.hPow (β := ℕ) a 0 = 1), a ^ Nat.gcd 0 n = 1
succ : ∀ (m : ℕ) (hm : a ^ (m + 1) = 1), a ^ (m + 1).gcd n = 1
⊢ a ^ m.gcd n = 1

Tactic:
obtain _ | m := m
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
hm : HPow.hPow (β := ℕ) a 0 = 1
⊢ a ^ Nat.gcd 0 n = 1

Tactic:
simpa
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
m : ℕ
hm : a ^ (m + 1) = 1
succ : ∀ (y : Mˣ) (hn : (↑y : M) ^ n = 1) (hm : (↑y : M) ^ (m + 1) = 1), (↑y : M) ^ (m + 1).gcd n = 1
⊢ a ^ (m + 1).gcd n = 1

Tactic:
obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero

Premises used: Nat.succ_ne_zero, rfl, IsUnit.of_pow_eq_one
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
n m : ℕ
y : Mˣ
hn : (↑y : M) ^ n = 1
hm : (↑y : M) ^ (m + 1) = 1
succ :
  ∀ (hn : HPow.hPow (β := ℤ) y (↑n : ℤ) = 1) (hm : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) = 1),
    HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
⊢ (↑y : M) ^ (m + 1).gcd n = 1

Tactic:
rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *

Premises used: zpow_natCast, Units.ext_iff, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
n m : ℕ
y : Mˣ
hn : HPow.hPow (β := ℤ) y (↑n : ℤ) = 1
hm : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) = 1
succ : y ^ ((↑(m + 1) : ℤ) * (m + 1).gcdA n + (↑n : ℤ) * (m + 1).gcdB n) = 1
succ₁ : y ^ ((↑(m + 1) : ℤ) * (m + 1).gcdA n) * y ^ ((↑n : ℤ) * (m + 1).gcdB n) = 1
succ₂ : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) ^ (m + 1).gcdA n * y ^ ((↑n : ℤ) * (m + 1).gcdB n) = 1
succ₃ : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) ^ (m + 1).gcdA n * HPow.hPow (β := ℤ) y (↑n : ℤ) ^ (m + 1).gcdB n = 1
succ₄ : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) ^ (m + 1).gcdA n * HPow.hPow (α := Mˣ) 1 ((m + 1).gcdB n) = 1
succ₅ : HPow.hPow (α := Mˣ) 1 ((m + 1).gcdA n) * HPow.hPow (α := Mˣ) 1 ((m + 1).gcdB n) = 1
succ₆ : 1 * HPow.hPow (α := Mˣ) 1 ((m + 1).gcdB n) = 1
succ₇ : HMul.hMul (α := Mˣ) 1 1 = 1
succ₈ succ₉ : Eq.{u_1 + 1} (α := Mˣ) 1 1
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1

Tactic:
rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]

Premises used: zpow_add, zpow_mul, one_zpow, Nat.gcd_eq_gcd_ab, one_mul
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : m.Coprime n
⊢ a ^ m = 1 ∧ a ^ n = 1 ↔ a = 1

Tactic:
simp [← pow_gcd_eq_one, hmn]

Premises used: pow_gcd_eq_one
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
m n : ℤ
ofNat : ∀ (m : ℕ), a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1
negSucc : ∀ (m : ℕ), a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1
⊢ a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1

Tactic:
obtain m | m := m
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
n : ℤ
m : ℕ
ofNat : ∀ (n : ℕ), a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1
ofNat₁ : ∀ (n : ℕ), a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1
⊢ a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1

Tactic:
obtain n | n := n
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
n : ℤ
m : ℕ
negSucc : ∀ (n : ℕ), a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1
negSucc₁ : ∀ (n : ℕ), a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1
⊢ a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1

Tactic:
obtain n | n := n
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1

Tactic:
simp
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1

Tactic:
simp
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1

Tactic:
simp
-- Module: Mathlib.Data.Int.GCD
Goal:
M : Type u_1
inst : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1

Tactic:
simp
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
rw : c ^ (n * m) = (c ^ m) ^ n
rw₁ rw₂ : c ^ (n * m) = c ^ (n * m)
⊢ (c ^ n) ^ m = (c ^ m) ^ n

Tactic:
rw [← pow_mul, ← pow_mul']

Premises used: pow_mul, pow_mul'
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
refine : ∀ (h : a ^ m = b ^ n), ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ a ^ m = b ^ n ↔ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨c, rfl, rfl⟩; rw [← pow_mul, ← pow_mul']⟩
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
pos : m = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
neg : ¬m = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases m = 0
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : m = 0
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
simp_all
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
pos : n = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
neg : ¬n = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases n = 0
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : n = 0
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
simp_all
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
pos : ∀ (hb : b = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
neg : ∀ (hb : ¬b = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : b = 0
⊢ a = HPow.hPow (α := α) 0 n ∧ b = HPow.hPow (α := α) 0 m

Tactic:
simp_all
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : b = 0
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
exact ⟨0, by simp_all⟩
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
pos : ∀ (ha : a = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
neg : ∀ (ha : ¬a = 0), ∃ (c : α), a = c ^ n ∧ b = c ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ b ^ n = a ^ m

Tactic:
have := h.symm
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : a = 0
this : b ^ n = a ^ m
⊢ a = HPow.hPow (α := α) 0 n ∧ b = HPow.hPow (α := α) 0 m

Tactic:
simp_all
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
exact ⟨0, by have := h.symm; simp_all⟩
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩

Premises used: HMul.hMul, Nat.gcdB, HPow.hPow, And.intro, Exists.intro, Nat.gcdA
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
neg₁ : b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m

Tactic:
refine ⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
(pow_one _).symm.trans ?_

Premises used: pow_one, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : HPow.hPow (β := ℕ) a 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
refine (pow_one _).symm.trans ?_

Premises used: pow_one, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
rw : a ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n)
| HPow.hPow (β := ℕ) a 1

Tactic:
rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]

Premises used: zpow_natCast, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : a ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n
⊢ HPow.hPow (β := ℕ) a 1 = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]

Premises used: zpow_natCast, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : a ^ ((↑m : ℤ) * m.gcdA n) * a ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑n : ℤ) * m.gcdB n) * b ^ ((↑n : ℤ) * m.gcdA n)
⊢ a ^ ((↑m : ℤ) * m.gcdA n + (↑n : ℤ) * m.gcdB n) = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

Tactic:
simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]

Premises used: zpow_natCast, zpow_mul, Commute.mul_zpow, zpow_add₀, Nat.gcdB, mul_comm, Nat.gcdA, Commute.zpow_zpow₀
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
neg : (b ^ n) ^ m.gcdA n * (a ^ n) ^ m.gcdB n = (a ^ n) ^ m.gcdB n * (b ^ n) ^ m.gcdA n
⊢ a ^ ((↑m : ℤ) * m.gcdA n) * a ^ ((↑n : ℤ) * m.gcdB n) = a ^ ((↑n : ℤ) * m.gcdB n) * b ^ ((↑n : ℤ) * m.gcdA n)

Tactic:
simp only [zpow_mul, zpow_natCast, h]

Premises used: zpow_natCast, zpow_mul
-- Module: Mathlib.Data.Int.GCD
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h_1 : ¬m = 0
h_2 : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ Commute a b

Tactic:
aesop