awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
have obtain : ∀ (i : ℕ) (hn : ¬i + 1 = 0),
  fib (HAdd.hAdd (α := ℤ) (-(↑(i + 1) : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑(i + 1) : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑(i + 1) : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑(i + 1) : ℤ)))
Tactic: obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
i : ℕ
hn : ¬i + 1 = 0
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑(i + 1) : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑(i + 1) : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑(i + 1) : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑(i + 1) : ℤ)))
have simp_rw : ((if Even (α := ℤ) (↑i : ℤ) then -fib (↑i : ℤ) else fib (↑i : ℤ)) *
      if Even (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1) then -fib (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1)
      else fib (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1)) +
    -HPow.hPow (β := ℕ) (if Even (α := ℤ) (↑(i + 1) : ℤ) then -fib (↑(i + 1) : ℤ) else fib (↑(i + 1) : ℤ)) 2 =
  fib (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑(i + 1) : ℤ) 1) -
    HPow.hPow (β := ℕ) (fib (↑(i + 1) : ℤ)) 2
Tactic: simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
have if : ∀ (hn : n = 0),
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
Tactic: if hn : n = 0 then simp [hn] else
    obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
    grind
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℕ
if :
  ∀ (hn : n = 0),
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
        HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
      HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
have if₁ : ∀ (hn : ¬n = 0),
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
Tactic: if hn : n = 0 then simp [hn] else
    obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
    grind
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
x a : ℤ
⊢ HPow.hPow (β := ℕ) (fib (x + a)) 2 - fib x * fib (x + 2 * a) =
    HPow.hPow (β := ℕ) (fib x * fib (a + 1) + fib (x - 1) * fib a) 2 -
      fib x *
        (fib x * (HPow.hPow (β := ℕ) (fib (a + 1)) 2 + HPow.hPow (β := ℕ) (fib a) 2) +
          fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))
have rw : HPow.hPow (β := ℕ) (fib (a + x)) 2 - fib x * fib (x + 2 * a) =
  HPow.hPow (β := ℕ) (fib x * fib (a + 1) + fib (x - 1) * fib a) 2 -
    fib x *
      (fib x * (HPow.hPow (β := ℕ) (fib (a + 1)) 2 + HPow.hPow (β := ℕ) (fib a) 2) +
        fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))
Tactic: rw [add_comm x]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
x a : ℤ
⊢ HPow.hPow (β := ℕ) (fib (a + x)) 2 - fib x * fib (x + 2 * a) =
    HPow.hPow (β := ℕ) (fib x * fib (a + 1) + fib (x - 1) * fib a) 2 -
      fib x *
        (fib x * (HPow.hPow (β := ℕ) (fib (a + 1)) 2 + HPow.hPow (β := ℕ) (fib a) 2) +
          fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))
have simp : HPow.hPow (β := ℕ) (fib (a - 1) * fib x + fib a * (fib (x - 1) + fib x)) 2 -
    fib x *
      (fib (x - 1) * (fib (a - 1) * fib a + fib a * (fib (a - 1) + fib a)) +
        fib x * (fib (a - 1) * fib (a - 1) + fib a * fib a + (fib (a - 1) * fib a + fib a * (fib (a - 1) + fib a)))) =
  HPow.hPow (β := ℕ) (fib x * (fib (a - 1) + fib a) + fib (x - 1) * fib a) 2 -
    fib x *
      (fib x * (HPow.hPow (β := ℕ) (fib (a - 1) + fib a) 2 + HPow.hPow (β := ℕ) (fib a) 2) +
        fib (x - 1) * (fib a * (fib (a - 1) + fib a) + fib (a - 1) * fib a))
Tactic: simp only [two_mul, fib_add, fib_one, mul_one, reduceAdd, fib_two, ← add_sub, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ r.xgcdAux s t r' s' t' =
    (r' % r).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r : ℤ) * s) (t' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r : ℤ) * t) r
      s t
have obtain : ∀ (r : ℕ) (h : 0 < r.succ),
  r.succ.xgcdAux s t r' s' t' =
    (r' % r.succ).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r.succ : ℤ) * s)
      (t' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r.succ : ℤ) * t) r.succ s t
Tactic: obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ r.succ.xgcdAux s t r' s' t' =
    (r' % r.succ).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r.succ : ℤ) * s)
      (t' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r.succ : ℤ) * t) r.succ s t
have rw : (match (motive := (n : ℕ) → (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → ℕ × ℤ × ℤ) r.succ,
    fun (m : ℕ) (x : m < r.succ) ↦
    Nat.strongRec' (p := fun (x : ℕ) ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
      (fun (n : ℕ) (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) (s t : ℤ) (r' : ℕ) (s' t' : ℤ) ↦
        match (motive := (n : ℕ) → (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → ℕ × ℤ × ℤ) n, ih with
        | 0, ih => (r', s', t')
        | k.succ, ih =>
          have q := r' / k.succ;
          ih (r' % k.succ) sorry (s' - (↑q : ℤ) * s) (t' - (↑q : ℤ) * t) k.succ s t)
      m with
  | 0, ih => (r', s', t')
  | k.succ, ih =>
    have q := r' / k.succ;
    ih (r' % k.succ) sorry (s' - (↑q : ℤ) * s) (t' - (↑q : ℤ) * t) k.succ s t) =
  (r' % r.succ).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r.succ : ℤ) * s)
    (t' - HDiv.hDiv (α := ℤ) (↑r' : ℤ) (↑r.succ : ℤ) * t) r.succ s t
Tactic: rw [xgcdAux, Nat.strongRec'_spec]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
s : ℕ
h : s ≠ 0
⊢ s.gcdA 0 = 1
have obtain : ∀ (s : ℕ) (h : s.succ ≠ 0), s.succ.gcdA 0 = 1
Tactic: obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
s : ℕ
h : s ≠ 0
⊢ s.gcdB 0 = 0
have obtain : ∀ (s : ℕ) (h : s.succ ≠ 0), s.succ.gcdB 0 = 0
Tactic: obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x_1 y_1 x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (x.xgcdAux s t y s' t').1 = x.gcd y
have simp : (y % x).gcd x = x.gcd y
Tactic: simp only [h, xgcdAux_rec, IH]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x_1 y_1 x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (y % x).gcd x = x.gcd y
have rw : x.gcd y = x.gcd y
Tactic: rw [← gcd_rec]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)
have rw : x.xgcdAux 1 0 y 0 1 = (x.gcd y, (x.xgcdAux 1 0 y 0 1).2)
Tactic: rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y : ℕ
rw : x.xgcdAux 1 0 y 0 1 = (x.gcd y, (x.xgcdAux 1 0 y 0 1).2)
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)
have rw₁ : x.xgcdAux 1 0 y 0 1 = ((x.xgcdAux 1 0 y 0 1).1, (x.xgcdAux 1 0 y 0 1).2)
Tactic: rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y 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' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (a.xgcdAux s t b s' t')
have H1 : x.P y
  ((b % a).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t) a s
    t)
Tactic: rw [xgcdAux_rec h]
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y 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' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y
    ((b % a).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t) a s
      t)
have H1 : x.P y (b % a, s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s, t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
Tactic: refine IH ?_ p
-- Lean 4 proof step from Mathlib.Data.Int.GCD (goal)
Goal:
x y 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' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (b % a, s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s, t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
have H1 : HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
  (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
    (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
Tactic: dsimp [P] at *
-- 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'
⊢ HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
    (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
      (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
have H1 : (↑b : ℤ) - (↑a : ℤ) * HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
  (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
    (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
Tactic: rw [Int.emod_def]
-- 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'
⊢ (↑b : ℤ) - (↑a : ℤ) * HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
    (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
      (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
have H1 : ∀ (k : ℤ), (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
Tactic: generalize (b / a : ℤ) = k
-- 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 : ℤ
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1 : (↑b : ℤ) - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
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)
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₁ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
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)
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₂ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
  (↑x : ℤ) * s' - (↑x : ℤ) * (k * s) + (↑y : ℤ) * (t' - k * t)
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)
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₃ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
  (↑x : ℤ) * s' + (↑y : ℤ) * (t' - k * t) - (↑x : ℤ) * (k * s)
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)
⊢ (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
have H1₄ : (↑x : ℤ) * s' + (↑y : ℤ) * t' - ((↑x : ℤ) * s + (↑y : ℤ) * t) * k =
  (↑x : ℤ) * s' + ((↑y : ℤ) * t' - (↑y : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
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)
⊢ (↑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 : ℤ) * (k * t)) - (↑x : ℤ) * (k * s)
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)
⊢ (↑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 : ℤ) * (k * s)
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)
⊢ (↑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]