awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
i : ℕ
hn : ¬i + 1 = 0
⊢ ((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:
grind
-- Module: Mathlib.Data.Int.Fib.Lemmas
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 : ℤ)))
if₁ :
  ∀ (hn : ¬n = 0),
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
        HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
      HPow.hPow (α := ℤ) (-1) (natAbs (-(↑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 : ℤ)))
if₃ 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 : ℤ)))

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

Premises used: sub_eq_add_neg, neg_add, Int.fib_neg, _private.0.Int.fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq, Int.natAbs_natCast, Int.natAbs_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
x a : ℤ
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))
⊢ 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))

Tactic:
rw [add_comm x]

Premises used: add_comm
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
x a : ℤ
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))
⊢ 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:
simp only [two_mul, fib_add, fib_one, mul_one, reduceAdd, fib_two, ← add_sub, sub_add_cancel]

Premises used: Int.reduceAdd, add_sub, two_mul, Int.fib_one, Int.fib_two, Int.fib_add, mul_one, sub_add_cancel
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
x a : ℤ
⊢ 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:
ring
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
x 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)) =
    HPow.hPow (α := ℤ) (-1) x.natAbs * HPow.hPow (β := ℕ) (fib a) 2

Tactic:
grind [fib_succ_mul_fib_pred_sub_fib_sq, fib_add_two]

Premises used: Int.fib_succ_mul_fib_pred_sub_fib_sq, Int.fib_add_two
-- Module: Mathlib.Data.Int.GCD
Goal:
s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
rfl

Premises used: Nat.xgcdAux, rfl, Nat.strongRec'
-- Module: Mathlib.Data.Int.GCD
Goal:
r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
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
⊢ 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

Tactic:
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
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) ⋯ (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) ⋯ (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
⊢ 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:
rw [xgcdAux, Nat.strongRec'_spec]

Premises used: Nat.xgcdAux, Nat.strongRec'_spec
-- Module: Mathlib.Data.Int.GCD
Goal:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ (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) ⋯ (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) ⋯ (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:
rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s : ℕ
⊢ gcdA 0 s = 0

Tactic:
rfl

Premises used: Nat.gcdA, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s : ℕ
⊢ gcdB 0 s = 1

Tactic:
rfl

Premises used: Nat.gcdB, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s : ℕ
h : s ≠ 0
obtain : ∀ (s : ℕ) (h : s.succ ≠ 0), s.succ.gcdA 0 = 1
⊢ s.gcdA 0 = 1

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s : ℕ
h : s.succ ≠ 0
⊢ s.succ.gcdA 0 = 1

Tactic:
rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s : ℕ
h : s ≠ 0
obtain : ∀ (s : ℕ) (h : s.succ ≠ 0), s.succ.gcdB 0 = 0
⊢ s.gcdB 0 = 0

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
s : ℕ
h : s.succ ≠ 0
⊢ s.succ.gcdB 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').1 = gcd 0 n

Tactic:
simp
-- Module: Mathlib.Data.Int.GCD
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' : ℤ
simp : (y % x).gcd x = x.gcd y
⊢ (x.xgcdAux s t y s' t').1 = x.gcd y

Tactic:
simp only [h, xgcdAux_rec, IH]

Premises used: Nat.xgcdAux_rec
-- Module: Mathlib.Data.Int.GCD
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' : ℤ
rw rw₁ : x.gcd y = x.gcd y
⊢ (y % x).gcd x = x.gcd y

Tactic:
rw [← gcd_rec]

Premises used: Nat.gcd_rec
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℕ
rw : x.xgcdAux 1 0 y 0 1 = (x.gcd y, (x.xgcdAux 1 0 y 0 1).2)
rw₁ rw₂ : x.xgcdAux 1 0 y 0 1 = ((x.xgcdAux 1 0 y 0 1).1, (x.xgcdAux 1 0 y 0 1).2)
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

Tactic:
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]

Premises used: Nat.xgcd, OfNat.ofNat, Nat.xgcdAux_fst
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℕ
⊢ x.xgcd y = ((x.xgcd y).1, (x.xgcd y).2)

Tactic:
constructor
-- Module: Mathlib.Data.Int.GCD
Goal:
x y 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:
simp
-- Module: Mathlib.Data.Int.GCD
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')
H1 :
  x.P y
    ((b % a).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t) a s
      t)
⊢ x.P y (a.xgcdAux s t b s' t')

Tactic:
rw [xgcdAux_rec h]

Premises used: Nat.xgcdAux_rec
-- Module: Mathlib.Data.Int.GCD
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)

Tactic:
IH ?_ p
-- Module: Mathlib.Data.Int.GCD
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')
H1 : x.P y (b % a, s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s, t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
⊢ x.P y
    ((b % a).xgcdAux (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t) a s
      t)

Tactic:
refine IH ?_ p
-- Module: Mathlib.Data.Int.GCD
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')
H1 :
  HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
    (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
      (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
⊢ x.P y (b % a, s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s, t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)

Tactic:
dsimp [P] at *

Premises used: _private.0.Nat.P
-- Module: Mathlib.Data.Int.GCD
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'
H1 :
  (↑b : ℤ) - (↑a : ℤ) * HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
    (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
      (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)
⊢ HMod.hMod (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
    (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
      (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)

Tactic:
rw [Int.emod_def]

Premises used: Int.emod_def
-- Module: Mathlib.Data.Int.GCD
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'
H1 : ∀ (k : ℤ), (↑b : ℤ) - (↑a : ℤ) * k = (↑x : ℤ) * (s' - k * s) + (↑y : ℤ) * (t' - k * t)
⊢ (↑b : ℤ) - (↑a : ℤ) * HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) =
    (↑x : ℤ) * (s' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * s) +
      (↑y : ℤ) * (t' - HDiv.hDiv (α := ℤ) (↑b : ℤ) (↑a : ℤ) * t)

Tactic:
generalize (b / a : ℤ) = k

Premises used: HDiv.hDiv, Nat.cast
-- Module: Mathlib.Data.Int.GCD
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
H1₁₂ 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)

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]

Premises used: add_sub_assoc, HMul.hMul, mul_assoc, Int.mul_sub, Nat.cast, add_comm, sub_sub, mul_comm, sub_add_eq_add_sub, Int.add_mul
-- Module: Mathlib.Data.Int.GCD
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')
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')
⊢ ∀ {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')

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]

Premises used: add_sub_assoc, mul_assoc, Int.mul_sub, _private.0.Nat.P, sub_sub, sub_add_eq_add_sub, Int.emod_def, Int.add_mul
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℕ
⊢ x.P y (x, 1, 0)

Tactic:
simp [P]

Premises used: _private.0.Nat.P
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℕ
⊢ x.P y (y, 0, 1)

Tactic:
simp [P]

Premises used: _private.0.Nat.P
-- Module: Mathlib.Data.Int.GCD
Goal:
x y : ℕ
⊢ 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])
-- Module: Mathlib.Data.Int.GCD
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
rwa₁ rwa₂ rwa₃ 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
⊢ (↑(x.gcd y) : ℤ) = (↑x : ℤ) * x.gcdA y + (↑y : ℤ) * x.gcdB y

Tactic:
rwa [xgcdAux_val, xgcd_val] at this

Premises used: Nat.xgcd_val, Nat.xgcdAux_val
-- Module: Mathlib.Data.Int.GCD
Goal:
k n : ℕ
hk : n.gcd k < k
⊢ Ne (α := ℤ) (↑k : ℤ) 0

Tactic:
have hk' := Int.ofNat_ne_zero.2 (Nat.zero_lt_of_lt hk).ne'
-- Module: Mathlib.Data.Int.GCD
Goal:
k n : ℕ
hk : n.gcd k < k
hk' : Ne (α := ℤ) (↑k : ℤ) 0
⊢ (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)
-- Module: Mathlib.Data.Int.GCD
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
⊢ 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

Premises used: Int.toNat_natCast, Int.add_mul_emod_self_left, Nat.mod_eq_of_lt, Int.natCast_mod
-- Module: Mathlib.Data.Int.GCD
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

Tactic:
⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩

Premises used: Int.ofNat_inj, Nat.cast, HMod.hMod, And.intro, Exists.intro, Iff.mp, Nat.gcdA, Int.toNat, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Int.GCD
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
refine_2 : Eq (α := ℤ) (↑(n * (n.gcdA k % (↑k : ℤ)).toNat % k) : ℤ) (↑((↑n : ℤ) * n.gcdA k % (↑k : ℤ)).toNat : ℤ)
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = n.gcd k

Tactic:
refine ⟨(n.gcdA k % k).toNat, ?_, (Int.ofNat_inj.1 ?_).trans key.symm⟩
-- Module: Mathlib.Data.Int.GCD
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 : ℤ) < (↑k : ℤ)
⊢ (n.gcdA k % (↑k : ℤ)).toNat < k

Tactic:
rw [Int.toNat_lt (Int.emod_nonneg _ hk')]

Premises used: Int.toNat_lt, Int.emod_nonneg
-- Module: Mathlib.Data.Int.GCD
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 : ℤ) < (↑k : ℤ)

Tactic:
Int.emod_lt _ hk'

Premises used: Int.natAbs, Int.emod_lt
-- Module: Mathlib.Data.Int.GCD
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 : ℤ) < (↑k : ℤ)

Tactic:
exact Int.emod_lt _ hk'

Premises used: Int.emod_lt
-- Module: Mathlib.Data.Int.GCD
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 : ℤ)
refine_2₆ refine_2₇ : (↑n : ℤ) * n.gcdA k % (↑k : ℤ) = (↑n : ℤ) * n.gcdA k % (↑k : ℤ)
⊢ Eq (α := ℤ) (↑(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]

Premises used: Int.toNat_of_nonneg, Int.natCast_mul, Int.mul_emod, Int.emod_emod, Int.natCast_mod, Int.emod_nonneg
-- Module: Mathlib.Data.Int.GCD
Goal:
k n : ℕ
hkn : n.Coprime k
hk : 1 < k
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = 1

Tactic:
simpa [hkn, hk] using exists_mul_mod_eq_gcd (k := k) (n := n)

Premises used: Nat.exists_mul_mod_eq_gcd
-- Module: Mathlib.Data.Int.GCD
Goal:
k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
⊢ k = 1 ∨ 1 < k

Tactic:
lia
-- Module: Mathlib.Data.Int.GCD
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
inr : ∀ (hk : 1 < k), ∃ (m : ℕ), m < k ∧ n * m % k = r % k
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = r % k

Tactic:
obtain rfl | hk : k = 1 ∨ 1 < k := by lia

Premises used: rfl
-- Module: Mathlib.Data.Int.GCD
Goal:
n r : ℕ
hkn : n.Coprime 1
hk : Ne (α := ℕ) 1 0
⊢ ∃ (m : ℕ), m < 1 ∧ n * m % 1 = r % 1

Tactic:
simp [mod_one]

Premises used: Nat.mod_one
-- Module: Mathlib.Data.Int.GCD
Goal:
k n r : ℕ
hkn : n.Coprime k
hk_1 : k ≠ 0
hk : 1 < k
inr : ∀ (m : ℕ) (hm : n * m % k = 1), ∃ (m : ℕ), m < k ∧ n * m % k = r % k
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = r % k

Tactic:
obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hkn hk

Premises used: Nat.exists_mul_mod_eq_one_of_coprime
-- Module: Mathlib.Data.Int.GCD
Goal:
k n r : ℕ
hkn : n.Coprime k
hk_1 : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ 0 < k

Tactic:
lia
-- Module: Mathlib.Data.Int.GCD
Goal:
k n r : ℕ
hkn : n.Coprime k
hk_1 : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
right : n * (m * r % k) % k = r % k
⊢ ∃ (m : ℕ), m < k ∧ n * m % k = r % k

Tactic:
use (m * r) % k, mod_lt _ (by lia)

Premises used: HMul.hMul, Nat.mod_lt