awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₈ : (a ^ (c - b) - 1) % (a ^ b - 1) % (a ^ b - 1) = a ^ ((c - b) % 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₉ : (a ^ (c - b) - 1) % (a ^ b - 1) = a ^ ((c - b) % 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have rw₁₀ : a ^ ((c - b) % b) - 1 = a ^ ((c - b) % 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
have inr : a ^ (c - b + b) - 1 = a ^ (c - b) * (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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
have inr : 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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 - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
have inr₁ : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
have inr₂ : a ^ (c - b) * a ^ b - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
have inr₃ : a ^ (c - b) * a ^ b - 1 = a ^ (c - b) * a ^ 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have inl : (HPow.hPow (β := ℕ) a 0 - 1).gcd (a ^ c - 1) = a ^ gcd 0 c - 1
Tactic: rcases eq_zero_or_pos b with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
inl : (HPow.hPow (β := ℕ) a 0 - 1).gcd (a ^ c - 1) = a ^ gcd 0 c - 1
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have inr : ∀ (hb : b > 0), (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
Tactic: rcases eq_zero_or_pos b with rfl | hb
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (hypothesis)
Goal:
a b c : ℕ
hb : b > 0
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have hb₁ : c % b < b
Tactic: replace hb : c % b < b := mod_lt c hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
hb : c % b < b
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have inr : ((a ^ c - 1) % (a ^ b - 1)).gcd (a ^ b - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
hb : c % b < b
inr : ((a ^ c - 1) % (a ^ b - 1)).gcd (a ^ b - 1) = a ^ b.gcd c - 1
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have inr₁ : (a ^ (c % b) - 1).gcd (a ^ b - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have inr₂ : a ^ (c % b).gcd b - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1
have inr₃ : a ^ b.gcd 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]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m.Coprime n
⊢ m.lcm n = m * n
have rw : 1 * m.lcm n = m * n
Tactic: rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m.Coprime n
rw : 1 * m.lcm n = m * n
⊢ m.lcm n = m * n
have rw₁ : m.gcd n * m.lcm n = m * n
Tactic: rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m.Coprime n
rw : 1 * m.lcm n = m * n
rw₁ : m.gcd n * m.lcm n = m * n
⊢ m.lcm n = m * n
have rw₂ : m * n = m * n
Tactic: rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
⊢ m.Coprime (n + m) ↔ m.Coprime n
have rw : m.gcd (n + m) = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_add_self_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : m.gcd (n + m) = 1 ↔ m.Coprime n
⊢ m.Coprime (n + m) ↔ m.Coprime n
have rw₁ : m.gcd (n + m) = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_self_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : m.gcd (n + m) = 1 ↔ m.Coprime n
rw₁ : m.gcd (n + m) = 1 ↔ m.gcd n = 1
⊢ m.Coprime (n + m) ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_self_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
⊢ m.Coprime (m + n) ↔ m.Coprime n
have rw : m.Coprime (n + m) ↔ m.Coprime n
Tactic: rw [add_comm, coprime_add_self_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : m.Coprime (n + m) ↔ m.Coprime n
⊢ m.Coprime (m + n) ↔ m.Coprime n
have rw₁ : m.Coprime n ↔ m.Coprime n
Tactic: rw [add_comm, coprime_add_self_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
⊢ (m + n).Coprime n ↔ m.Coprime n
have rw : (m + n).gcd n = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_add_self_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : (m + n).gcd n = 1 ↔ m.Coprime n
⊢ (m + n).Coprime n ↔ m.Coprime n
have rw₁ : (m + n).gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_self_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : (m + n).gcd n = 1 ↔ m.Coprime n
rw₁ : (m + n).gcd n = 1 ↔ m.gcd n = 1
⊢ (m + n).Coprime n ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_self_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
⊢ (m + n).Coprime m ↔ n.Coprime m
have rw : (m + n).gcd m = 1 ↔ n.Coprime m
Tactic: rw [Coprime, Coprime, gcd_self_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : (m + n).gcd m = 1 ↔ n.Coprime m
⊢ (m + n).Coprime m ↔ n.Coprime m
have rw₁ : (m + n).gcd m = 1 ↔ n.gcd m = 1
Tactic: rw [Coprime, Coprime, gcd_self_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
rw : (m + n).gcd m = 1 ↔ n.Coprime m
rw₁ : (m + n).gcd m = 1 ↔ n.gcd m = 1
⊢ (m + n).Coprime m ↔ n.Coprime m
have rw₂ : n.gcd m = 1 ↔ n.gcd m = 1
Tactic: rw [Coprime, Coprime, gcd_self_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ m.Coprime (n + k * m) ↔ m.Coprime n
have rw : m.gcd (n + k * m) = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_add_mul_right_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : m.gcd (n + k * m) = 1 ↔ m.Coprime n
⊢ m.Coprime (n + k * m) ↔ m.Coprime n
have rw₁ : m.gcd (n + k * m) = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_right_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ m.Coprime (n + k * m) ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_right_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ m.Coprime (n + m * k) ↔ m.Coprime n
have rw : m.gcd (n + m * k) = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_add_mul_left_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : m.gcd (n + m * k) = 1 ↔ m.Coprime n
⊢ m.Coprime (n + m * k) ↔ m.Coprime n
have rw₁ : m.gcd (n + m * k) = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_left_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ m.Coprime (n + m * k) ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_left_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ m.Coprime (k * m + n) ↔ m.Coprime n
have rw : m.gcd (k * m + n) = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_mul_right_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : m.gcd (k * m + n) = 1 ↔ m.Coprime n
⊢ m.Coprime (k * m + n) ↔ m.Coprime n
have rw₁ : m.gcd (k * m + n) = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_right_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ m.Coprime (k * m + n) ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_right_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ m.Coprime (m * k + n) ↔ m.Coprime n
have rw : m.gcd (m * k + n) = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_mul_left_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : m.gcd (m * k + n) = 1 ↔ m.Coprime n
⊢ m.Coprime (m * k + n) ↔ m.Coprime n
have rw₁ : m.gcd (m * k + n) = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_left_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ m.Coprime (m * k + n) ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_left_add_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ (m + k * n).Coprime n ↔ m.Coprime n
have rw : (m + k * n).gcd n = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_add_mul_right_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : (m + k * n).gcd n = 1 ↔ m.Coprime n
⊢ (m + k * n).Coprime n ↔ m.Coprime n
have rw₁ : (m + k * n).gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_right_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (m + k * n).Coprime n ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_right_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ (m + n * k).Coprime n ↔ m.Coprime n
have rw : (m + n * k).gcd n = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_add_mul_left_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : (m + n * k).gcd n = 1 ↔ m.Coprime n
⊢ (m + n * k).Coprime n ↔ m.Coprime n
have rw₁ : (m + n * k).gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_left_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (m + n * k).Coprime n ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_add_mul_left_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ (k * n + m).Coprime n ↔ m.Coprime n
have rw : (k * n + m).gcd n = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_mul_right_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : (k * n + m).gcd n = 1 ↔ m.Coprime n
⊢ (k * n + m).Coprime n ↔ m.Coprime n
have rw₁ : (k * n + m).gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_right_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (k * n + m).Coprime n ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_right_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
⊢ (n * k + m).Coprime n ↔ m.Coprime n
have rw : (n * k + m).gcd n = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_mul_left_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n k : ℕ
rw : (n * k + m).gcd n = 1 ↔ m.Coprime n
⊢ (n * k + m).Coprime n ↔ m.Coprime n
have rw₁ : (n * k + m).gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_left_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (n * k + m).Coprime n ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_mul_left_add_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
h : c ∣ b
⊢ (a + b).Coprime c ↔ a.Coprime c
have obtain : ∀ (n : ℕ), (a + c * n).Coprime c ↔ a.Coprime c
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
h : c ∣ a
⊢ (a + b).Coprime c ↔ b.Coprime c
have obtain : ∀ (n : ℕ), (c * n + b).Coprime c ↔ b.Coprime c
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
h : a ∣ c
⊢ a.Coprime (b + c) ↔ a.Coprime b
have obtain : ∀ (n : ℕ), a.Coprime (b + a * n) ↔ a.Coprime b
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
h : a ∣ b
⊢ a.Coprime (b + c) ↔ a.Coprime c
have obtain : ∀ (n : ℕ), a.Coprime (a * n + c) ↔ a.Coprime c
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime m ↔ n.Coprime m
have rw : (n - m).gcd m = 1 ↔ n.Coprime m
Tactic: rw [Coprime, Coprime, gcd_sub_self_left h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
rw : (n - m).gcd m = 1 ↔ n.Coprime m
⊢ (n - m).Coprime m ↔ n.Coprime m
have rw₁ : (n - m).gcd m = 1 ↔ n.gcd m = 1
Tactic: rw [Coprime, Coprime, gcd_sub_self_left h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (n - m).Coprime m ↔ n.Coprime m
have rw₂ : n.gcd m = 1 ↔ n.gcd m = 1
Tactic: rw [Coprime, Coprime, gcd_sub_self_left h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ m.Coprime (n - m) ↔ m.Coprime n
have rw : m.gcd (n - m) = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_sub_self_right h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
rw : m.gcd (n - m) = 1 ↔ m.Coprime n
⊢ m.Coprime (n - m) ↔ m.Coprime n
have rw₁ : m.gcd (n - m) = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_sub_self_right h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ m.Coprime (n - m) ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_sub_self_right h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime n ↔ m.Coprime n
have rw : (n - m).gcd n = 1 ↔ m.Coprime n
Tactic: rw [Coprime, Coprime, gcd_self_sub_left h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
rw : (n - m).gcd n = 1 ↔ m.Coprime n
⊢ (n - m).Coprime n ↔ m.Coprime n
have rw₁ : (n - m).gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_self_sub_left h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ (n - m).Coprime n ↔ m.Coprime n
have rw₂ : m.gcd n = 1 ↔ m.gcd n = 1
Tactic: rw [Coprime, Coprime, gcd_self_sub_left h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ n.Coprime (n - m) ↔ n.Coprime m
have rw : n.gcd (n - m) = 1 ↔ n.Coprime m
Tactic: rw [Coprime, Coprime, gcd_self_sub_right h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
h : m ≤ n
rw : n.gcd (n - m) = 1 ↔ n.Coprime m
⊢ n.Coprime (n - m) ↔ n.Coprime m
have rw₁ : n.gcd (n - m) = 1 ↔ n.gcd m = 1
Tactic: rw [Coprime, Coprime, gcd_self_sub_right h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
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
⊢ n.Coprime (n - m) ↔ n.Coprime m
have rw₂ : n.gcd m = 1 ↔ n.gcd m = 1
Tactic: rw [Coprime, Coprime, gcd_self_sub_right h]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n : ℕ
hn : 0 < n
a b : ℕ
⊢ (a ^ n).Coprime b ↔ a.Coprime b
have obtain : ∀ (n : ℕ) (hn : 0 < n.succ), (a ^ n.succ).Coprime b ↔ a.Coprime b
Tactic: obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n.succ).Coprime b ↔ a.Coprime b
have rw : (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b
Tactic: rw [Nat.pow_succ, Nat.coprime_mul_iff_left]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n : ℕ
hn : 0 < n
a b : ℕ
⊢ a.Coprime (b ^ n) ↔ a.Coprime b
have rw : (b ^ n).Coprime a ↔ a.Coprime b
Tactic: rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n : ℕ
hn : 0 < n
a b : ℕ
rw : (b ^ n).Coprime a ↔ a.Coprime b
⊢ a.Coprime (b ^ n) ↔ a.Coprime b
have rw₁ : b.Coprime a ↔ a.Coprime b
Tactic: rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n : ℕ
hn : 0 < n
a b : ℕ
rw : (b ^ n).Coprime a ↔ a.Coprime b
rw₁ : b.Coprime a ↔ a.Coprime b
⊢ a.Coprime (b ^ n) ↔ a.Coprime b
have rw₂ : a.Coprime b ↔ a.Coprime b
Tactic: rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b c : ℕ
hac : a.Coprime c
b_dvd_c : b ∣ c
⊢ (a * b).gcd c = b
have rcases : ∀ (d : ℕ) (hac : a.Coprime (d * b)) (b_dvd_c : b ∣ d * b), (a * b).gcd (d * b) = b
Tactic: rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
Cleared hypotheses: c, hac, b_dvd_c
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ (a * b).gcd (d * b) = b
have rw : a.gcd d * b = b
Tactic: rw [gcd_mul_right]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d * b = b
have h : a.gcd d = 1
Tactic: convert! one_mul b
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
⊢ m.Coprime n ↔ IsRelPrime m n
have simp_rw : m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1
Tactic: simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]