-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem xgcdAux_P (a b : R) {r r' : R} {s t s' t'} (p : P a b (r, s, t))
    (p' : P a b (r', s', t')) : P a b (xgcdAux r s t r' s' t')

Proof state:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux a✝ s t b✝ s' t')

Tactic:
rw [xgcdAux_rec h]

Result:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux (b✝ % a✝) (s' - b✝ / a✝ * s) (t' - b✝ / a✝ * t) a✝ s t)

Proof state:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * (s' - b✝ / a✝ * s) + b * (t' - b✝ / a✝ * 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]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : EuclideanDomain.P a b (r, s, t)
p' : EuclideanDomain.P a b (r', s', t')
⊢ EuclideanDomain.P a b (xgcdAux r s t r' s' t')

Tactic:
induction r, r' using GCD.induction generalizing s t s' t' with
| H0 n => simpa only [xgcd_zero_left]
| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine IH ?_ p
  unfold P at p p' ⊢
  dsimp
  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]

Result:
no goals

Proof state:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux (b✝ % a✝) (s' - b✝ / a✝ * s) (t' - b✝ / a✝ * t) a✝ s t)

Tactic:
refine IH ?_ p

Result:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t)

Proof state:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t)

Tactic:
unfold P at p p' ⊢

Result:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ match (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t) with
  | (r, s, t) => r = a * s + b * t

Proof state:
case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : EuclideanDomain.P a b (0, s, t)
p' : EuclideanDomain.P a b (n, s', t')
⊢ EuclideanDomain.P a b (xgcdAux 0 s t n s' t')

Tactic:
simpa only [xgcd_zero_left]

Result:
no goals

Proof state:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ match (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t) with
  | (r, s, t) => r = a * s + b * t

Tactic:
dsimp

Result:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * (s' - b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)