awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a
have inr : a * b * d / a = b * d
Tactic: refine ⟨d, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d
have inr : a * (b * d) / a = b * d
Tactic: rw [mul_assoc, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
inr : a * (b * d) / a = b * d
⊢ a * b * d / a = b * d
have inr₁ : b * d = b * d
Tactic: rw [mul_assoc, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ gcd a 0 = a
have rw : (if a0 : a = 0 then 0
  else
    have x : 0 % a ≺ a := sorry;
    gcd (0 % a) a) =
  a
Tactic: rw [gcd]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ (if a0 : a = 0 then 0
    else
      have x : 0 % a ≺ a := ⋯;
      gcd (0 % a) a) =
    a
have pos : ∀ (h : a = 0), 0 = a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
pos : ∀ (h : a = 0), 0 = a
⊢ (if a0 : a = 0 then 0
    else
      have x : 0 % a ≺ a := ⋯;
      gcd (0 % a) a) =
    a
have neg : ∀ (h : ¬a = 0),
  (have x : 0 % a ≺ a := sorry;
    gcd (0 % a) a) =
    a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ gcd a b = gcd (b % a) a
have rw : (if a0 : a = 0 then b
  else
    have x := sorry;
    gcd (b % a) a) =
  gcd (b % a) a
Tactic: rw [gcd]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a
have pos : ∀ (h : a = 0), b = gcd (b % a) a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
pos : ∀ (h : a = 0), b = gcd (b % a) a
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a
have neg : ∀ (h : ¬a = 0),
  (have x := sorry;
    gcd (b % a) a) =
    gcd (b % a) a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a
have pos : ∀ (h : a = 0), b = gcd (b % a) a
Tactic: split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
pos : ∀ (h : a = 0), b = gcd (b % a) a
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a
have neg : ∀ (h : ¬a = 0),
  (have x := sorry;
    gcd (b % a) a) =
    gcd (b % a) a
Tactic: split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b_1 b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b
have rw : b ∣ 0 ∧ b ∣ b
Tactic: rw [gcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 a b : R
h : a ≠ 0
h_1 : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
have rw : gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
Tactic: rw [gcd_val]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a_1 b_1 c a b : R
h : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd a b
have rw : c ∣ gcd (b % a) a
Tactic: rw [gcd_val]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : gcd a b = a
⊢ a ∣ b
have rw : gcd a b ∣ b
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd a b = a
have rw : gcd (b % a) a = a
Tactic: rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : a ∣ b
rw : gcd (b % a) a = a
⊢ gcd a b = a
have rw₁ : gcd 0 a = a
Tactic: rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
h : a ∣ b
rw : gcd (b % a) a = a
rw₁ : gcd 0 a = a
⊢ gcd a b = a
have rw₂ : a = a
Tactic: rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y x_1 s t s' t' : R
⊢ (xgcdAux 0 s t x_1 s' t').1 = gcd 0 x_1
have rw : (x_1, s', t').1 = gcd 0 x_1
Tactic: rw [xgcd_zero_left, gcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y x_1 s t s' t' : R
rw : (x_1, s', t').1 = gcd 0 x_1
⊢ (xgcdAux 0 s t x_1 s' t').1 = gcd 0 x_1
have rw₁ : (x_1, s', t').1 = x_1
Tactic: rw [xgcd_zero_left, gcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x_1 y_1 x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').1 = gcd x y
have simp : gcd (y % x) x = gcd x y
Tactic: simp only [xgcdAux_rec h, IH]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x_1 y_1 x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').1 = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y
have rw : gcd x y = gcd x y
Tactic: rw [← gcd_val]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
have rw : xgcdAux x 1 0 y 0 1 = (gcd x y, (xgcdAux x 1 0 y 0 1).2)
Tactic: rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
rw : xgcdAux x 1 0 y 0 1 = (gcd x y, (xgcdAux x 1 0 y 0 1).2)
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
have rw₁ : xgcdAux x 1 0 y 0 1 = ((xgcdAux x 1 0 y 0 1).1, (xgcdAux x 1 0 y 0 1).2)
Tactic: rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p : P a b (a_1, s, t)
p' : P a b (b_1, s', t')
⊢ P a b (xgcdAux a_1 s t b_1 s' t')
have H1 : P a b (xgcdAux (b_1 % a_1) (s' - b_1 / a_1 * s) (t' - b_1 / a_1 * t) a_1 s t)
Tactic: rw [xgcdAux_rec h]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p : P a b (a_1, s, t)
p' : P a b (b_1, s', t')
⊢ P a b (xgcdAux (b_1 % a_1) (s' - b_1 / a_1 * s) (t' - b_1 / a_1 * t) a_1 s t)
have H1 : P a b (b_1 % a_1, s' - b_1 / a_1 * s, t' - b_1 / a_1 * t)
Tactic: refine IH ?_ p
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₈ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (t * (b_1 / a_1)))
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
H1₈ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (t * (b_1 / a_1)))
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₉ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * t * (b_1 / a_1))
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
H1₈ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (t * (b_1 / a_1)))
H1₉ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * t * (b_1 / a_1))
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₁₀ : b_1 % a_1 = b_1 - (a * s + b * t) * (b_1 / a_1)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
H1₈ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (t * (b_1 / a_1)))
H1₉ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * t * (b_1 / a_1))
H1₁₀ : b_1 % a_1 = b_1 - (a * s + b * t) * (b_1 / a_1)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₁₁ : b_1 % a_1 = b_1 - a_1 * (b_1 / a_1)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b a_1 b_1 : R
h : a_1 ≠ 0
IH :
  ∀ {s t s' t' : R} (p : P a b (b_1 % a_1, s, t)) (p' : P a b (a_1, s', t')), P a b (xgcdAux (b_1 % a_1) s t a_1 s' t')
s t s' t' : R
p :
  match (motive := R × R × R → Prop) (a_1, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (motive := R × R × R → Prop) (b_1, s', t') with
  | (r, s, t) => r = a * s + b * t
H1 : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
H1₁ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + (b * t' - b * (b_1 / a_1 * t))
H1₂ : b_1 % a_1 = a * s' - a * (b_1 / a_1 * s) + b * t' - b * (b_1 / a_1 * t)
H1₃ : b_1 % a_1 = a * s' + b * t' - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₄ : b_1 % a_1 = b_1 - a * (b_1 / a_1 * s) - b * (b_1 / a_1 * t)
H1₅ : b_1 % a_1 = b_1 - (a * (b_1 / a_1 * s) + b * (b_1 / a_1 * t))
H1₆ : b_1 % a_1 = b_1 - (a * (s * (b_1 / a_1)) + b * (b_1 / a_1 * t))
H1₇ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (b_1 / a_1 * t))
H1₈ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * (t * (b_1 / a_1)))
H1₉ : b_1 % a_1 = b_1 - (a * s * (b_1 / a_1) + b * t * (b_1 / a_1))
H1₁₀ : b_1 % a_1 = b_1 - (a * s + b * t) * (b_1 / a_1)
H1₁₁ : b_1 % a_1 = b_1 - a_1 * (b_1 / a_1)
⊢ b_1 % a_1 = a * (s' - b_1 / a_1 * s) + b * (t' - b_1 / a_1 * t)
have H1₁₂ : b_1 - a_1 * (b_1 / a_1) = b_1 - a_1 * (b_1 / a_1)
Tactic: rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]