awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t →
      (↑a : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t' →
        (↑((b % a).xgcdAux s t a s' t').1 : ℤ) =
          HMul.hMul (α := ℤ) (↑x : ℤ) ((b % a).xgcdAux s t a s' t').2.1 +
            HMul.hMul (α := ℤ) (↑y : ℤ) ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t
p' : (↑b : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t'
k : ℤ
H1 : (↑b : ℤ) - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₁ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₂ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' - (↑x : ℤ) * (k * s) + (↑y : ℤ) * (t' - k * t)
H1₃ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + (↑y : ℤ) * (t' - k * t) - (↑x : ℤ) * (k * s)
H1₄ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₅ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₆ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (k * s)
H1₇ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (s * k)
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₈ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
  (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * (s * k)
Tactic: rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t →
      (↑a : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t' →
        (↑((b % a).xgcdAux s t a s' t').1 : ℤ) =
          HMul.hMul (α := ℤ) (↑x : ℤ) ((b % a).xgcdAux s t a s' t').2.1 +
            HMul.hMul (α := ℤ) (↑y : ℤ) ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t
p' : (↑b : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t'
k : ℤ
H1 : (↑b : ℤ) - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₁ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₂ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' - (↑x : ℤ) * (k * s) + (↑y : ℤ) * (t' - k * t)
H1₃ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + (↑y : ℤ) * (t' - k * t) - (↑x : ℤ) * (k * s)
H1₄ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₅ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₆ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (k * s)
H1₇ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (s * k)
H1₈ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * (s * k)
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₉ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
  (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
Tactic: rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t →
      (↑a : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t' →
        (↑((b % a).xgcdAux s t a s' t').1 : ℤ) =
          HMul.hMul (α := ℤ) (↑x : ℤ) ((b % a).xgcdAux s t a s' t').2.1 +
            HMul.hMul (α := ℤ) (↑y : ℤ) ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t
p' : (↑b : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t'
k : ℤ
H1 : (↑b : ℤ) - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₁ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₂ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' - (↑x : ℤ) * (k * s) + (↑y : ℤ) * (t' - k * t)
H1₃ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + (↑y : ℤ) * (t' - k * t) - (↑x : ℤ) * (k * s)
H1₄ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₅ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₆ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (k * s)
H1₇ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (s * k)
H1₈ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * (s * k)
H1₉ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₁₀ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k) =
  (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
Tactic: rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t →
      (↑a : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t' →
        (↑((b % a).xgcdAux s t a s' t').1 : ℤ) =
          HMul.hMul (α := ℤ) (↑x : ℤ) ((b % a).xgcdAux s t a s' t').2.1 +
            HMul.hMul (α := ℤ) (↑y : ℤ) ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t
p' : (↑b : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t'
k : ℤ
H1 : (↑b : ℤ) - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₁ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₂ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' - (↑x : ℤ) * (k * s) + (↑y : ℤ) * (t' - k * t)
H1₃ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + (↑y : ℤ) * (t' - k * t) - (↑x : ℤ) * (k * s)
H1₄ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₅ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₆ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (k * s)
H1₇ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (s * k)
H1₈ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * (s * k)
H1₉ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
H1₁₀ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₁₁ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k) =
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - (↑y : ℤ) * t * k - (↑x : ℤ) * s * k
Tactic: rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t →
      (↑a : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t' →
        (↑((b % a).xgcdAux s t a s' t').1 : ℤ) =
          HMul.hMul (α := ℤ) (↑x : ℤ) ((b % a).xgcdAux s t a s' t').2.1 +
            HMul.hMul (α := ℤ) (↑y : ℤ) ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : (↑a : ℤ) = (↑x : ℤ) * s + (↑y : ℤ) * t
p' : (↑b : ℤ) = (↑x : ℤ) * s' + (↑y : ℤ) * t'
k : ℤ
H1 : (↑b : ℤ) - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₁ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
H1₂ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' - (↑x : ℤ) * (k * s) + (↑y : ℤ) * (t' - k * t)
H1₃ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + (↑y : ℤ) * (t' - k * t) - (↑x : ℤ) * (k * s)
H1₄ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₅ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
H1₆ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (k * s)
H1₇ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (t * k)) - (↑x : ℤ) * (s * k)
H1₈ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * (s * k)
H1₉ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s * k + (↑y : ℤ) * t * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
H1₁₀ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k) =
    (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * t * k) - (↑x : ℤ) * s * k
H1₁₁ :
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k) =
    (↑x : ℤ) * s' + (↑y : ℤ) * t' - (↑y : ℤ) * t * k - (↑x : ℤ) * s * k
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₁₂ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k) =
  (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑y : ℤ) * t * k + (↑x : ℤ) * s * k)
Tactic: rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y r r' : ℕ
⊢ ∀ {s t s' t' : ℤ}, x.P y (r, s, t) → x.P y (r', s', t') → x.P y (r.xgcdAux s t r' s' t')
have H0 : ∀ (n : ℕ) {s t s' t' : ℤ}, x.P y (0, s, t) → x.P y (n, s', t') → x.P y (xgcdAux 0 s t n s' t')
Tactic: induction r, r' using gcd.induction with
  | H0 => simp
  | H1 a b h IH =>
    intro s t s' t' p p'
    rw [xgcdAux_rec h]; refine IH ?_ p; dsimp [P] at *
    rw [Int.emod_def]; generalize (b / a : ℤ) = k
    rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
Cleared hypotheses: r, r'
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y r r' : ℕ
H0 : ∀ (n : ℕ) {s t s' t' : ℤ}, x.P y (0, s, t) → x.P y (n, s', t') → x.P y (xgcdAux 0 s t n s' t')
⊢ ∀ {s t s' t' : ℤ}, x.P y (r, s, t) → x.P y (r', s', t') → x.P y (r.xgcdAux s t r' s' t')
have H1 : ∀ (a b : ℕ) (h : 0 < a)
  (IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t'))
  {s t s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')
Tactic: induction r, r' using gcd.induction with
  | H0 => simp
  | H1 a b h IH =>
    intro s t s' t' p p'
    rw [xgcdAux_rec h]; refine IH ?_ p; dsimp [P] at *
    rw [Int.emod_def]; generalize (b / a : ℤ) = k
    rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
Cleared hypotheses: r, r'
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
x y : ℕ
⊢ (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y
have this : x.P y (x.xgcdAux 1 0 y 0 1)
Tactic: have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℕ
this : x.P y (x.xgcdAux 1 0 y 0 1)
⊢ (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y
have rwa : ∀ (this : x.P y (x.gcd y, x.xgcd y)), (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y
Tactic: rwa [xgcdAux_val, xgcd_val] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℕ
this : x.P y (x.xgcdAux 1 0 y 0 1)
rwa : ∀ (this : x.P y (x.gcd y, x.xgcd y)), (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y
⊢ (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y
have rwa₁ : ∀ (this : x.P y (x.gcd y, x.gcdA y, x.gcdB y)), (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y
Tactic: rwa [xgcdAux_val, xgcd_val] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
k n : ℕ
hk : n.gcd k < k
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = n.gcd k
have hk' : Ne (α := ℤ) (↑k : ℤ) 0
Tactic: have hk' := Int.ofNat_ne_zero.2 (Nat.zero_lt_of_lt hk).ne'
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = n.gcd k
have key : (HMod.hMod (α := ℤ) (↑(n.gcd k) : ℤ) (↑k : ℤ)).toNat = (((↑n : ℤ) * n.gcdA k + (↑k : ℤ) * n.gcdB k) % (↑k : ℤ)).toNat
Tactic: have key := congr(($(gcd_eq_gcd_ab n k) % k).toNat)
-- Lean 4 proof step from Mathlib.Data.Int.GCD (hypothesis)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key :
  (HMod.hMod (α := ℤ) (↑(n.gcd k) : ℤ) (↑k : ℤ)).toNat = (((↑n : ℤ) * n.gcdA k + (↑k : ℤ) * n.gcdB k) % (↑k : ℤ)).toNat
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = n.gcd k
have key₁ : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
Tactic: rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = n.gcd k
have refine_1 : (n.gcdA k % (↑k : ℤ)).toNat < k
Tactic: refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_1 : (n.gcdA k % (↑k : ℤ)).toNat < k
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = n.gcd k
have refine_2 : Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
Tactic: refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
⊢ (n.gcdA k % (↑k : ℤ)).toNat < k
have refine_1 : n.gcdA k % (↑k : ℤ) < (↑k : ℤ)
Tactic: rw [Int.toNat_lt (Int.emod_nonneg _ hk')]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2 : HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_2 :
  HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2₁ : HMul.hMul (α := ℤ) (↑n : ℤ) (↑(n.gcdA k % (↑k : ℤ)).toNat : ℤ) % (↑k : ℤ) =
  (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_2 :
  HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₁ :
  HMul.hMul (α := ℤ) (↑n : ℤ) (↑(n.gcdA k % (↑k : ℤ)).toNat : ℤ) % (↑k : ℤ) =
    (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2₂ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_2 :
  HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₁ :
  HMul.hMul (α := ℤ) (↑n : ℤ) (↑(n.gcdA k % (↑k : ℤ)).toNat : ℤ) % (↑k : ℤ) =
    (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₂ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2₃ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_2 :
  HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₁ :
  HMul.hMul (α := ℤ) (↑n : ℤ) (↑(n.gcdA k % (↑k : ℤ)).toNat : ℤ) % (↑k : ℤ) =
    (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₂ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₃ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2₄ : HMod.hMod (α := ℤ) (↑n : ℤ) (↑k : ℤ) * (n.gcdA k % (↑k : ℤ) % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_2 :
  HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₁ :
  HMul.hMul (α := ℤ) (↑n : ℤ) (↑(n.gcdA k % (↑k : ℤ)).toNat : ℤ) % (↑k : ℤ) =
    (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₂ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₃ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
refine_2₄ :
  HMod.hMod (α := ℤ) (↑n : ℤ) (↑k : ℤ) * (n.gcdA k % (↑k : ℤ) % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2₅ : HMod.hMod (α := ℤ) (↑n : ℤ) (↑k : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
key : n.gcd k = ((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat
refine_2 :
  HMod.hMod (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat) : ℤ) (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₁ :
  HMul.hMul (α := ℤ) (↑n : ℤ) (↑(n.gcdA k % (↑k : ℤ)).toNat : ℤ) % (↑k : ℤ) =
    (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₂ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
refine_2₃ : (↑n : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
refine_2₄ :
  HMod.hMod (α := ℤ) (↑n : ℤ) (↑k : ℤ) * (n.gcdA k % (↑k : ℤ) % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
refine_2₅ : HMod.hMod (α := ℤ) (↑n : ℤ) (↑k : ℤ) * (n.gcdA k % (↑k : ℤ)) % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
⊢ Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
have refine_2₆ : (↑n : ℤ) * n.gcdA k % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
Tactic: rw [Int.natCast_mod, Int.natCast_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = r % k
have inl : ∀ (hkn : n.Coprime 1) (hk : Ne (α := ℕ) 1 0), ∃ (m : ℕ), m < 1 ∧ n * m % 1 = r % 1
Tactic: obtain rfl | hk : k = 1 ∨ 1 < k := by lia
Cleared hypotheses: k, hkn, hk
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
inl : ∀ (hkn : n.Coprime 1) (hk : Ne (α := ℕ) 1 0), ∃ (m : ℕ), m < 1 ∧ n * m % 1 = r % 1
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = r % k
have inr : ∀ (hk : 1 < k), ∃ (m : ℕ), m < k ∧ n * m % k = r % k
Tactic: obtain rfl | hk : k = 1 ∨ 1 < k := 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 : ℕ), m < k ∧ n * m % k = r % k
have inr : ∀ (m : ℕ) (hm : n * m % k = 1), ∃ (m : ℕ), m < k ∧ n * m % k = r % k
Tactic: obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hkn hk