no goals
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')
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]
no goals
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')
simpa only [xgcd_zero_left]
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)
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')
rw [xgcdAux_rec h]
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)
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)
refine' IH _ p
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
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)
unfold P at p p'⊢
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)
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
dsimp
no goals
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)
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]