awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n r : ℕ
hkn : n.Coprime k
hk_1 : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = r % k
have right : n * (m * r % k) % k = r % k
Tactic: use (m * r) % k, mod_lt _ (by lia)
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n r : ℕ
hkn : n.Coprime k
hk_1 : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n * (m * r % k) % k = r % k
have right : n % k * (m * r % k % k) % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₁ : n % k * (m * r % k) % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₂ : n * (m * r) % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₃ : n * m * r % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₄ : n * m % k * (r % k) % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₅ : 1 * (r % k) % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₆ : r % k % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ n * (m * r % k) % k = r % k
have right₇ : r % k = r % k
Tactic: rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
m n : ℕ
⊢ (↑(gcd (↑m : ℤ) -[n+1]) : ℤ) =
    (↑m : ℤ) * gcdA (↑m : ℤ) -[n+1] + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * -(natAbs (↑m : ℤ)).gcdB n.succ
have rw : (↑(gcd (↑m : ℤ) -[n+1]) : ℤ) =
  (↑m : ℤ) * gcdA (↑m : ℤ) -[n+1] + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (natAbs (↑m : ℤ)).gcdB n.succ
Tactic: rw [Int.neg_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
m n : ℕ
⊢ (↑(-[m+1].gcd (↑n : ℤ)) : ℤ) =
    -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * -m.succ.gcdA (natAbs (↑n : ℤ)) + (↑n : ℤ) * -[m+1].gcdB (↑n : ℤ)
have rw : (↑(-[m+1].gcd (↑n : ℤ)) : ℤ) =
  HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * m.succ.gcdA (natAbs (↑n : ℤ)) + (↑n : ℤ) * -[m+1].gcdB (↑n : ℤ)
Tactic: rw [Int.neg_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
have 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
Tactic: rw [Int.neg_mul_neg, Int.neg_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℤ
hc : x.gcd y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0
have contrapose! : ∀ (hc : x = 0 ∧ y = 0), x.gcd y = 0
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ x.gcd y = 0
have rw : gcd 0 y = 0
Tactic: rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℤ
hc : x = 0 ∧ y = 0
rw : gcd 0 y = 0
⊢ x.gcd y = 0
have rw₁ : gcd 0 0 = 0
Tactic: rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℤ
hc : x = 0 ∧ y = 0
rw : gcd 0 y = 0
rw₁ : gcd 0 0 = 0
⊢ x.gcd y = 0
have rw₂ : natAbs 0 = 0
Tactic: rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℤ
hc : x = 0 ∧ y = 0
rw : gcd 0 y = 0
rw₁ : gcd 0 0 = 0
rw₂ : natAbs 0 = 0
⊢ x.gcd y = 0
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n ↔ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y
have mp : a.gcd b ∣ n → ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
n : ℕ
mp : a.gcd b ∣ n → ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y
⊢ a.gcd b ∣ n ↔ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y
have mpr : (∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y) → a.gcd b ∣ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y
have mp : ∃ (x : ℤ), ∃ (y : ℤ), a * (a.gcdA b * (↑(n / a.gcd b) : ℤ)) + b * (a.gcdB b * (↑(n / a.gcd b) : ℤ)) = 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]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
n : ℕ
x y : ℤ
h : (↑n : ℤ) = a * x + b * y
⊢ a.gcd b ∣ n
have mpr : (↑(a.gcd b) : ℤ) ∣ a * x + b * y
Tactic: rw [← Int.natCast_dvd_natCast, h]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
⊢ a ∣ b
have this : (↑(a.gcd c) : ℤ) = a * a.gcdA c + c * a.gcdB c
Tactic: have := gcd_eq_gcd_ab a c
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
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
⊢ a ∣ b
have this₁ : 1 = a * a.gcdA c + c * a.gcdB c
Tactic: simp only [hab, Int.ofNat_zero, Int.natCast_succ, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
have rw : a ∣ b * a * a.gcdA c + b * c * a.gcdB c
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd b = 1
⊢ a ∣ c
have habc₁ : a ∣ c * b
Tactic: rw [mul_comm] at habc
Cleared hypotheses: habc, hab
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n : ℕ | 0 < n ∧ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = a * x + b * y} (a.gcd b)
have simp_rw : IsLeast {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
Tactic: simp_rw [← gcd_dvd_iff]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
have left : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
ha : a ≠ 0
left : Membership.mem (γ := Set ℕ) {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
⊢ IsLeast {n : ℕ | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
have right : Membership.mem (γ := Set ℕ) (lowerBounds {n : ℕ | 0 < n ∧ a.gcd b ∣ n}) (a.gcd b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
a b : ℤ
ha : a ≠ 0
⊢ Membership.mem (γ := Set ℕ) (lowerBounds {n : ℕ | 0 < n ∧ a.gcd b ∣ n}) (a.gcd b)
have right : ∀ ⦃a_1 : ℕ⦄, 0 < a_1 → a.gcd b ∣ a_1 → a.gcd b ≤ a_1
Tactic: simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1 ∧ a ^ n = 1
have left : a ^ m = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
left : a ^ m = 1
⊢ a ^ m = 1 ∧ a ^ n = 1
have right : a ^ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1
have left : a ^ (m.gcd n * (m / m.gcd n)) = 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ m = 1
have left₁ : (a ^ m.gcd n) ^ (m / m.gcd n) = 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ m = 1
have left₂ : HPow.hPow (α := M) 1 (m / m.gcd n) = 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ m = 1
have left₃ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ n = 1
have right : a ^ (m.gcd n * (n / m.gcd n)) = 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ n = 1
have right₁ : (a ^ m.gcd n) ^ (n / m.gcd n) = 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ n = 1
have right₂ : HPow.hPow (α := M) 1 (n / m.gcd n) = 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ n = 1
have right₃ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
m n : ℕ
hm : a ^ m = 1
hn : a ^ n = 1
⊢ a ^ m.gcd n = 1
have zero : ∀ (hm : HPow.hPow (β := ℕ) a 0 = 1), a ^ Nat.gcd 0 n = 1
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ m.gcd n = 1
have succ : ∀ (m : ℕ) (hm : a ^ (m + 1) = 1), a ^ (m + 1).gcd n = 1
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
m : ℕ
hm : a ^ (m + 1) = 1
⊢ a ^ (m + 1).gcd n = 1
have succ : ∀ (y : Mˣ) (hn : (↑y : M) ^ n = 1) (hm : (↑y : M) ^ (m + 1) = 1), (↑y : M) ^ (m + 1).gcd n = 1
Tactic: obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero
Cleared hypotheses: a, hn, hm
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Monoid M
n m : ℕ
y : Mˣ
hn : (↑y : M) ^ n = 1
hm : (↑y : M) ^ (m + 1) = 1
⊢ (↑y : M) ^ (m + 1).gcd n = 1
have succ : ∀ (hn : HPow.hPow (β := ℤ) y (↑n : ℤ) = 1) (hm : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) = 1),
  HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
Tactic: rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ : y ^ ((↑(m + 1) : ℤ) * (m + 1).gcdA n + (↑n : ℤ) * (m + 1).gcdB n) = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₁ : y ^ ((↑(m + 1) : ℤ) * (m + 1).gcdA n) * y ^ ((↑n : ℤ) * (m + 1).gcdB n) = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₂ : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) ^ (m + 1).gcdA n * y ^ ((↑n : ℤ) * (m + 1).gcdB n) = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₃ : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) ^ (m + 1).gcdA n * HPow.hPow (β := ℤ) y (↑n : ℤ) ^ (m + 1).gcdB n = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₄ : HPow.hPow (β := ℤ) y (↑(m + 1) : ℤ) ^ (m + 1).gcdA n * HPow.hPow (α := Mˣ) 1 ((m + 1).gcdB n) = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₅ : HPow.hPow (α := Mˣ) 1 ((m + 1).gcdA n) * HPow.hPow (α := Mˣ) 1 ((m + 1).gcdB n) = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₆ : 1 * HPow.hPow (α := Mˣ) 1 ((m + 1).gcdB n) = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₇ : HMul.hMul (α := Mˣ) 1 1 = 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ HPow.hPow (β := ℤ) y (↑((m + 1).gcd n) : ℤ) = 1
have succ₈ : Eq.{u_1 + 1} (α := Mˣ) 1 1
Tactic: rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Group M
a : M
m n : ℤ
⊢ a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1
have ofNat : ∀ (m : ℕ), a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1
Tactic: obtain m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ m.gcd n = 1 ↔ a ^ m = 1 ∧ a ^ n = 1
have negSucc : ∀ (m : ℕ), a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1
Tactic: obtain m | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1
have ofNat : ∀ (n : ℕ), a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1
Tactic: obtain n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1
have ofNat₁ : ∀ (n : ℕ), a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1
Tactic: obtain n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
M : Type u_1
inst : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1
have negSucc : ∀ (n : ℕ), a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1
Tactic: obtain n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1
have negSucc₁ : ∀ (n : ℕ), a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1
Tactic: obtain n | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ (c ^ n) ^ m = (c ^ m) ^ n
have rw : c ^ (n * m) = (c ^ m) ^ n
Tactic: rw [← pow_mul, ← pow_mul']
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
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
⊢ (c ^ n) ^ m = (c ^ m) ^ n
have rw₁ : c ^ (n * m) = c ^ (n * m)
Tactic: rw [← pow_mul, ← pow_mul']
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
⊢ a ^ m = b ^ n ↔ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have refine : ∀ (h : 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']⟩
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ (c : α), a = c ^ n ∧ b = c ^ m
have pos : m = 0 → ∃ (c : α), a = c ^ n ∧ b = c ^ m
Tactic: by_cases m = 0