[GOAL]
n : ℕ
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
[PROOFSTEP]
have : sqrt (2 - sqrtTwoAddSeries 0 n) / (2 : ℝ) * (2 : ℝ) ^ (n + 2) < π :=
  by
  rw [← lt_div_iff, ← sin_pi_over_two_pow_succ]; apply sin_lt; apply div_pos pi_pos
  all_goals apply pow_pos; norm_num
[GOAL]
n : ℕ
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
[PROOFSTEP]
rw [← lt_div_iff, ← sin_pi_over_two_pow_succ]
[GOAL]
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) < π / 2 ^ (n + 2)
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply sin_lt
[GOAL]
case h
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
all_goals apply pow_pos; norm_num
[GOAL]
case h
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case h.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) < π
[PROOFSTEP]
apply lt_of_le_of_lt (le_of_eq _) this
[GOAL]
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2)
[PROOFSTEP]
rw [pow_succ _ (n + 1), ← mul_assoc, div_mul_cancel, mul_comm]
[GOAL]
case h
n : ℕ
this : sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ π < 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
have : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / (2 : ℝ) + (1 : ℝ) / ((2 : ℝ) ^ n) ^ 3 / 4) * (2 : ℝ) ^ (n + 2) :=
  by
  rw [← div_lt_iff, ← sin_pi_over_two_pow_succ]
  refine' lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _
  · apply div_pos pi_pos; apply pow_pos; norm_num
  · rw [div_le_iff']
    · refine' le_trans pi_le_four _
      simp only [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, mul_one]
      apply pow_le_pow; norm_num; apply le_add_of_nonneg_left; apply Nat.zero_le
    · apply pow_pos; norm_num
  apply add_le_add_left; rw [div_le_div_right]
  rw [le_div_iff, ← mul_pow]
  refine' le_trans _ (le_of_eq (one_pow 3)); apply pow_le_pow_of_le_left
  · apply le_of_lt; apply mul_pos; apply div_pos pi_pos; apply pow_pos; norm_num; apply pow_pos
    norm_num
  rw [← le_div_iff]
  refine' le_trans ((div_le_div_right _).mpr pi_le_four) _; apply pow_pos; norm_num
  rw [pow_succ, pow_succ, ← mul_assoc, ← div_div]
    -- Porting note: removed `convert le_rfl`
  all_goals (repeat' apply pow_pos); norm_num
[GOAL]
n : ℕ
⊢ π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
[PROOFSTEP]
rw [← div_lt_iff, ← sin_pi_over_two_pow_succ]
[GOAL]
n : ℕ
⊢ π / 2 ^ (n + 2) < sin (π / 2 ^ (n + 2)) + 1 / (2 ^ n) ^ 3 / 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
refine' lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _
[GOAL]
case refine'_1
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case refine'_1
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_1.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ 1
[PROOFSTEP]
rw [div_le_iff']
[GOAL]
case refine'_2
n : ℕ
⊢ π ≤ 2 ^ (n + 2) * 1
[PROOFSTEP]
refine' le_trans pi_le_four _
[GOAL]
case refine'_2
n : ℕ
⊢ 4 ≤ 2 ^ (n + 2) * 1
[PROOFSTEP]
simp only [show (4 : ℝ) = (2 : ℝ) ^ 2 by norm_num, mul_one]
[GOAL]
n : ℕ
⊢ 4 = 2 ^ 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
n : ℕ
⊢ 2 ^ 2 ≤ 2 ^ (n + 2)
[PROOFSTEP]
apply pow_le_pow
[GOAL]
case refine'_2.ha
n : ℕ
⊢ 1 ≤ 2
case refine'_2.h n : ℕ ⊢ 2 ≤ n + 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2.h
n : ℕ
⊢ 2 ≤ n + 2
[PROOFSTEP]
apply le_add_of_nonneg_left
[GOAL]
case refine'_2.h.h
n : ℕ
⊢ 0 ≤ n
[PROOFSTEP]
apply Nat.zero_le
[GOAL]
case refine'_2
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_2.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) + (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ sin (π / 2 ^ (n + 2)) + 1 / (2 ^ n) ^ 3 / 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply add_le_add_left
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 / 4 ≤ 1 / (2 ^ n) ^ 3 / 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [div_le_div_right]
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2)) ^ 3 ≤ 1 / (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [le_div_iff, ← mul_pow]
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2) * 2 ^ n) ^ 3 ≤ 1
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
refine' le_trans _ (le_of_eq (one_pow 3))
[GOAL]
case refine'_3.bc
n : ℕ
⊢ (π / 2 ^ (n + 2) * 2 ^ n) ^ 3 ≤ 1 ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_le_pow_of_le_left
[GOAL]
case refine'_3.bc.ha
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2) * 2 ^ n
[PROOFSTEP]
apply le_of_lt
[GOAL]
case refine'_3.bc.ha.a
n : ℕ
⊢ 0 < π / 2 ^ (n + 2) * 2 ^ n
[PROOFSTEP]
apply mul_pos
[GOAL]
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < π / 2 ^ (n + 2)
case refine'_3.bc.ha.a.hb n : ℕ ⊢ 0 < 2 ^ n
[PROOFSTEP]
apply div_pos pi_pos
[GOAL]
case refine'_3.bc.ha.a.ha
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case refine'_3.bc.ha.a.hb n : ℕ ⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.ha.a.ha.H
n : ℕ
⊢ 0 < 2
case refine'_3.bc.ha.a.hb n : ℕ ⊢ 0 < 2 ^ n
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.ha.a.hb
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.ha.a.hb.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ π / 2 ^ (n + 2) * 2 ^ n ≤ 1
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [← le_div_iff]
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
refine' le_trans ((div_le_div_right _).mpr pi_le_four) _
[GOAL]
case refine'_3.bc.hab.refine'_1
n : ℕ
⊢ 0 < 2 ^ (n + 2)
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.refine'_1.H
n : ℕ
⊢ 0 < 2
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / 2 ^ (n + 2) ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
rw [pow_succ, pow_succ, ← mul_assoc, ← div_div]
  -- Porting note: removed `convert le_rfl`
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
case refine'_3.bc
n : ℕ
⊢ 0 < 4
n : ℕ ⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
all_goals (repeat' apply pow_pos); norm_num
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.refine'_2
n : ℕ
⊢ 4 / (2 * 2) / 2 ^ n ≤ 1 / 2 ^ n
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc.hab
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.hab.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < (2 ^ n) ^ 3
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.H
n : ℕ
⊢ 0 < 2 ^ n
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.H.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc.H.H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
apply pow_pos
[GOAL]
case refine'_3.bc
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
repeat' apply pow_pos
[GOAL]
n : ℕ
⊢ 0 < 2 ^ (n + 2)
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply pow_pos
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ π < 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
apply lt_of_lt_of_le this (le_of_eq _)
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) =
    2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
rw [add_mul]
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) + 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) =
    2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ sqrt (2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) = 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n)
[PROOFSTEP]
rw [pow_succ _ (n + 1), ← mul_assoc, div_mul_cancel, mul_comm]
[GOAL]
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case e_a
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n
[PROOFSTEP]
rw [pow_succ, ← pow_mul, mul_comm n 2, pow_mul, show (2 : ℝ) ^ 2 = 4 by norm_num, pow_succ, pow_succ, ←
  mul_assoc (2 : ℝ), show (2 : ℝ) * 2 = 4 by norm_num, ← mul_assoc, div_mul_cancel, mul_comm ((2 : ℝ) ^ n), ← div_div,
  div_mul_cancel]
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 * 2 = 4
[PROOFSTEP]
norm_num
[GOAL]
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ n ≠ 0
case e_a.h n : ℕ this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) ⊢ 4 ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case e_a.h.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ≠ 0
case e_a.h n : ℕ this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) ⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case e_a.h
n : ℕ
this : π < (sqrt (2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a < π
[PROOFSTEP]
refine' lt_of_le_of_lt _ (pi_gt_sqrtTwoAddSeries n)
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ sqrt (2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)
[PROOFSTEP]
refine' (div_le_iff (pow_pos (by norm_num) _ : (0 : ℝ) < _)).mp (le_sqrt_of_sq_le _)
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n
[PROOFSTEP]
rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]
[GOAL]
n : ℕ
a : ℝ
h : sqrtTwoAddSeries (↑0 / ↑1) n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 = ↑0 / ↑1
[PROOFSTEP]
rw [Nat.cast_zero, zero_div]
[GOAL]
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrtTwoAddSeries (↑a / ↑b) (n + 1) ≤ z
[PROOFSTEP]
refine' le_trans _ hz
[GOAL]
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrtTwoAddSeries (↑a / ↑b) (n + 1) ≤ sqrtTwoAddSeries (↑c / ↑d) n
[PROOFSTEP]
rw [sqrtTwoAddSeries_succ]
[GOAL]
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrtTwoAddSeries (sqrt (2 + ↑a / ↑b)) n ≤ sqrtTwoAddSeries (↑c / ↑d) n
[PROOFSTEP]
apply sqrtTwoAddSeries_monotone_left
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
[PROOFSTEP]
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
[PROOFSTEP]
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ sqrt (2 + ↑a / ↑b) ≤ ↑c / ↑d
[PROOFSTEP]
rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hb'),
  div_le_div_iff hb' (pow_pos hd' _)]
[GOAL]
case h
c d a b n : ℕ
z : ℝ
hz : sqrtTwoAddSeries (↑c / ↑d) n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b
[PROOFSTEP]
exact_mod_cast h
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ π < a
[PROOFSTEP]
refine' lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) _
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 ^ (n + 1) * sqrt (2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n ≤ a
[PROOFSTEP]
rw [← le_sub_iff_add_le, ← le_div_iff', sqrt_le_left, sub_le_comm]
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n
[PROOFSTEP]
rwa [Nat.cast_zero, zero_div] at h
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)
[PROOFSTEP]
exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)
[GOAL]
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries (↑0 / ↑1) n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)
[PROOFSTEP]
exact pow_pos zero_lt_two _
[GOAL]
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ z ≤ sqrtTwoAddSeries (↑c / ↑d) (n + 1)
[PROOFSTEP]
apply le_trans hz
[GOAL]
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ sqrtTwoAddSeries (↑a / ↑b) n ≤ sqrtTwoAddSeries (↑c / ↑d) (n + 1)
[PROOFSTEP]
rw [sqrtTwoAddSeries_succ]
[GOAL]
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ sqrtTwoAddSeries (↑a / ↑b) n ≤ sqrtTwoAddSeries (sqrt (2 + ↑c / ↑d)) n
[PROOFSTEP]
apply sqrtTwoAddSeries_monotone_left
[GOAL]
case h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ ↑a / ↑b ≤ sqrt (2 + ↑c / ↑d)
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
[PROOFSTEP]
have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
[PROOFSTEP]
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
[PROOFSTEP]
rw [div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hd'), div_le_div_iff (pow_pos hb' _) hd']
[GOAL]
case h.h
a b c d n : ℕ
z : ℝ
hz : z ≤ sqrtTwoAddSeries (↑a / ↑b) n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ ↑a ^ 2 * ↑d ≤ (2 * ↑d + ↑c) * ↑b ^ 2
[PROOFSTEP]
exact_mod_cast h
[GOAL]
⊢ 3 < π
[PROOFSTEP]
pi_lower_bound [23 / 16]
[GOAL]
⊢ 3.14 < π
[PROOFSTEP]
pi_lower_bound [99 / 70, 874 / 473, 1940 / 989, 1447 / 727]
[GOAL]
⊢ π < 3.15
[PROOFSTEP]
pi_upper_bound [140 / 99, 279 / 151, 51 / 26, 412 / 207]
[GOAL]
⊢ 3.1415 < π
[PROOFSTEP]
pi_lower_bound [11482 / 8119, 5401 / 2923, 2348 / 1197, 11367 / 5711, 25705 / 12868, 23235 / 11621]
[GOAL]
⊢ π < 3.1416
[PROOFSTEP]
pi_upper_bound [4756 / 3363, 101211 / 54775, 505534 / 257719, 83289 / 41846, 411278 / 205887, 438142 / 219137,
  451504 / 225769, 265603 / 132804, 849938 / 424971]
[GOAL]
⊢ 3.141592 < π
[PROOFSTEP]
pi_lower_bound [11482 / 8119, 7792 / 4217, 54055 / 27557, 949247 / 476920, 3310126 / 1657059, 2635492 / 1318143,
  1580265 / 790192, 1221775 / 610899, 3612247 / 1806132, 849943 / 424972]
[GOAL]
⊢ π < 3.141593
[PROOFSTEP]
pi_upper_bound [27720 / 19601, 56935 / 30813, 49359 / 25163, 258754 / 130003, 113599 / 56868, 1101994 / 551163,
  8671537 / 4336095, 3877807 / 1938940, 52483813 / 26242030, 56946167 / 28473117, 23798415 / 11899211]


[GOAL]
u : XgcdType
⊢ v u = succ₂ (vp u)
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
⊢ (v u).fst = (succ₂ (vp u)).fst
[PROOFSTEP]
dsimp [v, vp, w, z, a, b, succ₂]
[GOAL]
case h₂
u : XgcdType
⊢ (v u).snd = (succ₂ (vp u)).snd
[PROOFSTEP]
dsimp [v, vp, w, z, a, b, succ₂]
[GOAL]
case h₁
u : XgcdType
⊢ succ u.wp * succ u.ap + u.x * succ u.bp = succ (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp)
[PROOFSTEP]
repeat' rw [Nat.succ_eq_add_one]; ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ succ u.wp * succ u.ap + u.x * succ u.bp = succ (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ (u.wp + 1) * succ u.ap + u.x * succ u.bp = succ (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ u.wp * succ u.ap + succ u.ap + u.x * succ u.bp = succ (u.wp + u.wp * u.ap + u.x + u.x * u.bp + u.ap)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ u.wp * (u.ap + 1) + (u.ap + 1) + u.x * succ u.bp = succ (u.wp + u.wp * u.ap + u.x + u.x * u.bp + u.ap)
[PROOFSTEP]
ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x * succ u.bp = succ (u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x * (u.bp + 1) = succ (u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp = succ (u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₁
u : XgcdType
⊢ 1 + u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp = u.wp + u.wp * u.ap + u.ap + u.x + u.x * u.bp + 1
[PROOFSTEP]
ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ u.y * succ u.ap + succ u.zp * succ u.bp = succ (u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp)
[PROOFSTEP]
repeat' rw [Nat.succ_eq_add_one]; ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ u.y * succ u.ap + succ u.zp * succ u.bp = succ (u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ u.y * (u.ap + 1) + succ u.zp * succ u.bp = succ (u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + succ u.zp * succ u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + (u.zp + 1) * succ u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + u.zp * succ u.bp + succ u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ u.y + u.y * u.ap + u.zp * (u.bp + 1) + (u.bp + 1) = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
ring_nf
[GOAL]
case h₂
u : XgcdType
⊢ 1 + u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp = succ (u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp)
[PROOFSTEP]
rw [Nat.succ_eq_add_one]
[GOAL]
case h₂
u : XgcdType
⊢ 1 + u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp = u.y + u.y * u.ap + u.zp + u.zp * u.bp + u.bp + 1
[PROOFSTEP]
ring_nf
[GOAL]
u : XgcdType
⊢ IsSpecial u ↔ IsSpecial' u
[PROOFSTEP]
dsimp [IsSpecial, IsSpecial']
[GOAL]
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ w u * z u = succPNat (u.x * u.y)
[PROOFSTEP]
let ⟨wp, x, y, zp, ap, bp⟩ := u
[GOAL]
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔
    w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
        z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      succPNat
        ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)
[PROOFSTEP]
constructor
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y →
    w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
        z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      succPNat
        ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)
[PROOFSTEP]
intro h
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
⊢ w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
        z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
      succPNat
        ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y) →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
[PROOFSTEP]
intro h
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
⊢ w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
      z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
    succPNat
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)
[PROOFSTEP]
simp [w, z, succPNat] at *
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  w { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } *
      z { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp } =
    succPNat
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
[PROOFSTEP]
simp [w, z, succPNat] at *
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ { val := succ wp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp) } *
      { val := succ zp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp) } =
    { val := succ (x * y),
      property :=
        (_ :
          0 <
            succ
              ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
                { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)) }
[PROOFSTEP]
simp only [← coe_inj, mul_coe, mk_coe] at *
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { val := succ wp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp) } *
      { val := succ zp, property := (_ : 0 < succ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp) } =
    { val := succ (x * y),
      property :=
        (_ :
          0 <
            succ
              ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
                { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y)) }
⊢ wp + zp + wp * zp = x * y
[PROOFSTEP]
simp only [← coe_inj, mul_coe, mk_coe] at *
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ succ wp * succ zp = succ (x * y)
[PROOFSTEP]
simp_all [← h, Nat.mul, Nat.succ_eq_add_one]
[GOAL]
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
[PROOFSTEP]
ring
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : succ wp * succ zp = succ (x * y)
⊢ wp + zp + wp * zp = x * y
[PROOFSTEP]
simp [Nat.succ_eq_add_one, Nat.mul_add, Nat.add_mul, ← Nat.add_assoc] at h
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y
[PROOFSTEP]
rw [← h]
[GOAL]
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp
[PROOFSTEP]
ring
  -- Porting note: Old code has been removed as it was much more longer.
[GOAL]
u : XgcdType
⊢ IsReduced (flip u) ↔ IsReduced u
[PROOFSTEP]
dsimp [IsReduced, flip]
[GOAL]
u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp
[PROOFSTEP]
constructor
[GOAL]
case mp
u : XgcdType
⊢ u.bp = u.ap → u.ap = u.bp
[PROOFSTEP]
intro h
[GOAL]
case mpr
u : XgcdType
⊢ u.ap = u.bp → u.bp = u.ap
[PROOFSTEP]
intro h
[GOAL]
case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp
[PROOFSTEP]
exact h.symm
[GOAL]
case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap
[PROOFSTEP]
exact h.symm
[GOAL]
u : XgcdType
⊢ IsSpecial (flip u) ↔ IsSpecial u
[PROOFSTEP]
dsimp [IsSpecial, flip]
[GOAL]
u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
[PROOFSTEP]
rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]
[GOAL]
u : XgcdType
⊢ v (flip u) = Prod.swap (v u)
[PROOFSTEP]
dsimp [v]
[GOAL]
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)) =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u))
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).fst =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).fst
[PROOFSTEP]
simp only
[GOAL]
case h₁
u : XgcdType
⊢ ↑(z u) * ↑(b u) + u.y * ↑(a u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
case h₂
u : XgcdType
⊢ (↑(z u) * ↑(b u) + u.y * ↑(a u), u.x * ↑(b u) + ↑(w u) * ↑(a u)).snd =
    (u.y * ↑(a u) + ↑(z u) * ↑(b u), ↑(w u) * ↑(a u) + u.x * ↑(b u)).snd
[PROOFSTEP]
simp only
[GOAL]
case h₂
u : XgcdType
⊢ u.x * ↑(b u) + ↑(w u) * ↑(a u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u = 0
⊢ q u = qp u + 1
[PROOFSTEP]
by_cases hq : u.q = 0
[GOAL]
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
⊢ q u = qp u + 1
[PROOFSTEP]
let h := u.rq_eq
[GOAL]
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
h : r u + (u.bp + 1) * q u = u.ap + 1 := rq_eq u
⊢ q u = qp u + 1
[PROOFSTEP]
rw [hr, hq, mul_zero, add_zero] at h
[GOAL]
case pos
u : XgcdType
hr : r u = 0
hq : q u = 0
h : 0 = u.ap + 1
⊢ q u = qp u + 1
[PROOFSTEP]
cases h
[GOAL]
case neg
u : XgcdType
hr : r u = 0
hq : ¬q u = 0
⊢ q u = qp u + 1
[PROOFSTEP]
exact (Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm
[GOAL]
u : XgcdType
a b : ℕ+
⊢ IsSpecial (start a b)
[PROOFSTEP]
dsimp [start, IsSpecial]
[GOAL]
u : XgcdType
a b : ℕ+
⊢ v (start a b) = (↑a, ↑b)
[PROOFSTEP]
dsimp [start, v, XgcdType.a, XgcdType.b, w, z]
[GOAL]
u : XgcdType
a b : ℕ+
⊢ (succ 0 * succ (↑a - 1) + 0 * succ (↑b - 1), 0 * succ (↑a - 1) + succ 0 * succ (↑b - 1)) = (↑a, ↑b)
[PROOFSTEP]
have : succ 0 = 1 := rfl
[GOAL]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ 0 * succ (↑a - 1) + 0 * succ (↑b - 1), 0 * succ (↑a - 1) + succ 0 * succ (↑b - 1)) = (↑a, ↑b)
[PROOFSTEP]
rw [this, one_mul, one_mul, zero_mul, zero_mul, zero_add, add_zero]
[GOAL]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (↑a - 1), succ (↑b - 1)) = (↑a, ↑b)
[PROOFSTEP]
rw [← Nat.pred_eq_sub_one, ← Nat.pred_eq_sub_one]
[GOAL]
u : XgcdType
a b : ℕ+
this : succ 0 = 1
⊢ (succ (pred ↑a), succ (pred ↑b)) = (↑a, ↑b)
[PROOFSTEP]
rw [Nat.succ_pred_eq_of_pos a.pos, Nat.succ_pred_eq_of_pos b.pos]
[GOAL]
u : XgcdType
⊢ IsReduced (finish u)
[PROOFSTEP]
dsimp [IsReduced]
[GOAL]
u : XgcdType
⊢ (finish u).ap = (finish u).bp
[PROOFSTEP]
rfl
[GOAL]
u : XgcdType
hs : IsSpecial u
⊢ IsSpecial (finish u)
[PROOFSTEP]
dsimp [IsSpecial, finish] at hs ⊢
[GOAL]
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * qp u + u.zp) + u.wp * (u.y * qp u + u.zp) = ((u.wp + 1) * qp u + u.x) * u.y
[PROOFSTEP]
rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]
[GOAL]
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * qp u + u.zp) + u.wp * (u.y * qp u + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * qp u * u.y
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u = 0
⊢ v (finish u) = v u
[PROOFSTEP]
let ha : u.r + u.b * u.q = u.a := u.rq_eq
[GOAL]
u : XgcdType
hr : r u = 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (finish u) = v u
[PROOFSTEP]
rw [hr, zero_add] at ha
[GOAL]
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ v (finish u) = v u
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).fst = (v u).fst
[PROOFSTEP]
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
have : u.wp + 1 = u.w := rfl
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ (u.wp + 1) * ↑(b u) + ((u.wp + 1) * qp u + u.x) * ↑(b u) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
rw [this, ← ha, u.qp_eq hr]
[GOAL]
case h₁
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
this : u.wp + 1 = ↑(w u)
⊢ ↑(w u) * ↑(b u) + (↑(w u) * qp u + u.x) * ↑(b u) = ↑(w u) * (↑(b u) * (qp u + 1)) + u.x * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ (v (finish u)).snd = (v u).snd
[PROOFSTEP]
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b
[GOAL]
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
rw [← ha, u.qp_eq hr]
[GOAL]
case h₂
u : XgcdType
hr : r u = 0
ha : ↑(b u) * q u = ↑(a u)
⊢ u.y * ↑(b u) + (u.y * qp u + ↑(z u)) * ↑(b u) = u.y * (↑(b u) * (qp u + 1)) + ↑(z u) * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u ≠ 0
⊢ sizeOf (step u) < sizeOf u
[PROOFSTEP]
change u.r - 1 < u.bp
[GOAL]
u : XgcdType
hr : r u ≠ 0
⊢ r u - 1 < u.bp
[PROOFSTEP]
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)
[GOAL]
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
⊢ r u - 1 < u.bp
[PROOFSTEP]
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
[GOAL]
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
h₁ : r u < u.bp + 1
⊢ r u - 1 < u.bp
[PROOFSTEP]
rw [← h₀] at h₁
[GOAL]
u : XgcdType
hr : r u ≠ 0
h₀ : r u - 1 + 1 = r u
h₁ : r u - 1 + 1 < u.bp + 1
⊢ r u - 1 < u.bp
[PROOFSTEP]
exact lt_of_succ_lt_succ h₁
[GOAL]
u : XgcdType
hs : IsSpecial u
⊢ IsSpecial (step u)
[PROOFSTEP]
dsimp [IsSpecial, step] at hs ⊢
[GOAL]
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * q u + u.zp + u.wp + (u.y * q u + u.zp) * u.wp = u.y * ((u.wp + 1) * q u + u.x)
[PROOFSTEP]
rw [mul_add, mul_comm u.y u.x, ← hs]
[GOAL]
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.y * q u + u.zp + u.wp + (u.y * q u + u.zp) * u.wp = u.y * ((u.wp + 1) * q u) + (u.wp + u.zp + u.wp * u.zp)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
hr : r u ≠ 0
⊢ v (step u) = Prod.swap (v u)
[PROOFSTEP]
let ha : u.r + u.b * u.q = u.a := u.rq_eq
[GOAL]
u : XgcdType
hr : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
⊢ v (step u) = Prod.swap (v u)
[PROOFSTEP]
let hr : u.r - 1 + 1 = u.r := (add_comm _ 1).trans (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr))
[GOAL]
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ v (step u) = Prod.swap (v u)
[PROOFSTEP]
ext
[GOAL]
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).fst = (Prod.swap (v u)).fst
[PROOFSTEP]
change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b
[GOAL]
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * (r u - 1 + 1) = u.y * ↑(a u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
rw [← ha, hr]
[GOAL]
case h₁
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * q u + ↑(z u)) * ↑(b u) + u.y * r u = u.y * (r u + ↑(b u) * q u) + ↑(z u) * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (v (step u)).snd = (Prod.swap (v u)).snd
[PROOFSTEP]
change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
[GOAL]
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * (r u - 1 + 1) = ↑(w u) * ↑(a u) + u.x * ↑(b u)
[PROOFSTEP]
rw [← ha, hr]
[GOAL]
case h₂
u : XgcdType
hr✝ : r u ≠ 0
ha : r u + ↑(b u) * q u = ↑(a u) := rq_eq u
hr : r u - 1 + 1 = r u := Eq.trans (add_comm (r u - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (↑(w u) * q u + u.x) * ↑(b u) + ↑(w u) * r u = ↑(w u) * (r u + ↑(b u) * q u) + u.x * ↑(b u)
[PROOFSTEP]
ring
[GOAL]
u : XgcdType
_h : ¬r u = 0
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (step u) u
[PROOFSTEP]
apply u.step_wf _h
[GOAL]
u✝ u : XgcdType
h : r u = 0
⊢ reduce u = finish u
[PROOFSTEP]
rw [reduce]
[GOAL]
u✝ u : XgcdType
h : r u = 0
⊢ (if x : r u = 0 then finish u else flip (reduce (step u))) = finish u
[PROOFSTEP]
exact if_pos h
[GOAL]
u✝ u : XgcdType
h : r u ≠ 0
⊢ reduce u = flip (reduce (step u))
[PROOFSTEP]
rw [reduce]
[GOAL]
u✝ u : XgcdType
h : r u ≠ 0
⊢ (if x : r u = 0 then finish u else flip (reduce (step u))) = flip (reduce (step u))
[PROOFSTEP]
exact if_neg h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (reduce x✝)
[PROOFSTEP]
rw [reduce_a h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ IsReduced (finish u)
[PROOFSTEP]
exact u.finish_isReduced
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
⊢ IsReduced (reduce x✝)
[PROOFSTEP]
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce x✝)
[PROOFSTEP]
rw [reduce_b h, flip_isReduced]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ IsReduced (reduce (step u))
[PROOFSTEP]
apply reduce_isReduced
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (reduce x✝)
[PROOFSTEP]
rw [reduce_a h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (finish u)
[PROOFSTEP]
exact u.finish_isSpecial hs
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
⊢ IsSpecial (reduce x✝)
[PROOFSTEP]
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (reduce x✝)
[PROOFSTEP]
rw [reduce_b h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
hs : IsSpecial x✝
this : sizeOf (step u) < sizeOf u
⊢ IsSpecial (flip (reduce (step u)))
[PROOFSTEP]
exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : r u = 0
⊢ v (reduce x✝) = v x✝
[PROOFSTEP]
rw [reduce_a h, finish_v u h]
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
⊢ v (reduce x✝) = v x✝
[PROOFSTEP]
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
[GOAL]
u✝ x✝ : XgcdType
u : XgcdType := x✝
h : ¬r u = 0
this : sizeOf (step u) < sizeOf u
⊢ v (reduce x✝) = v x✝
[PROOFSTEP]
rw [reduce_b h, flip_v, reduce_v (step u), step_v u h, Prod.swap_swap]
[GOAL]
a b : ℕ+
⊢ ↑(gcdA' a b) = ↑(gcdW a b) + gcdX a b
[PROOFSTEP]
dsimp [gcdA', gcdX, gcdW, XgcdType.w]
[GOAL]
a b : ℕ+
⊢ succ ((xgcd a b).wp + (xgcd a b).x) = succ (xgcd a b).wp + (xgcd a b).x
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.succ_eq_add_one, add_right_comm]
[GOAL]
a b : ℕ+
⊢ ↑(gcdB' a b) = gcdY a b + ↑(gcdZ a b)
[PROOFSTEP]
dsimp [gcdB', gcdY, gcdZ, XgcdType.z]
[GOAL]
a b : ℕ+
⊢ succ ((xgcd a b).y + (xgcd a b).zp) = (xgcd a b).y + succ (xgcd a b).zp
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.succ_eq_add_one, add_assoc]
[GOAL]
a b : ℕ+
⊢ let d := gcdD a b;
  let w := gcdW a b;
  let x := gcdX a b;
  let y := gcdY a b;
  let z := gcdZ a b;
  let a' := gcdA' a b;
  let b' := gcdB' a b;
  w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
intros d w x y z a' b'
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
let u := XgcdType.start a b
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
let ur := u.reduce
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have _ : d = ur.a := rfl
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hb : d = ur.b := u.reduce_isReduced'
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have ha' : (a' : ℕ) = w + x := gcdA'_coe a b
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hb' : (b' : ℕ) = y + z := gcdB'_coe a b
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hdet : w * z = succPNat (x * y) := u.reduce_isSpecial' rfl
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ w * z = succPNat (x * y) ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ w * z = succPNat (x * y)
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
exact hdet
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hdet' : (w * z : ℕ) = x * y + 1 := by rw [← mul_coe, hdet, succPNat_coe]
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
⊢ ↑w * ↑z = x * y + 1
[PROOFSTEP]
rw [← mul_coe, hdet, succPNat_coe]
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have _ : u.v = ⟨a, b⟩ := XgcdType.start_v a b
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
let hv : Prod.mk (w * d + x * ur.b : ℕ) (y * d + z * ur.b : ℕ) = ⟨a, b⟩ := u.reduce_v.trans (XgcdType.start_v a b)
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑w * ↑d + x * ↑(XgcdType.b ur), y * ↑d + ↑z * ↑(XgcdType.b ur)) = (↑a, ↑b) :=
  Eq.trans (XgcdType.reduce_v u) (XgcdType.start_v a b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
rw [← hb, ← add_mul, ← add_mul, ← ha', ← hb'] at hv
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hb'' : (b : ℕ) = b' * d := (congr_arg Prod.snd hv).symm
[GOAL]
case right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ a = a' * d
case right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d ∧ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
exact eq ha''
[GOAL]
case right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d ∧ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ b = b' * d
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
exact eq hb''
[GOAL]
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hza' : (z * a' : ℕ) = x * b' + 1 :=
  by
  rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
  ring
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ ↑z * ↑a' = x * ↑b' + 1
[PROOFSTEP]
rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ x * y + 1 + ↑z * x = x * y + x * ↑z + 1
[PROOFSTEP]
ring
[GOAL]
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
have hwb' : (w * b' : ℕ) = y * a' + 1 :=
  by
  rw [ha', hb', mul_add, mul_add, hdet']
  ring
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * ↑b' = y * ↑a' + 1
[PROOFSTEP]
rw [ha', hb', mul_add, mul_add, hdet']
[GOAL]
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ ↑w * y + (x * y + 1) = y * ↑w + y * x + 1
[PROOFSTEP]
ring
[GOAL]
case right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ z * a' = succPNat (x * ↑b') ∧ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ z * a' = succPNat (x * ↑b')
[PROOFSTEP]
apply eq
[GOAL]
case right.right.right.left.a
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = ↑(succPNat (x * ↑b'))
[PROOFSTEP]
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']
[GOAL]
case right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ w * b' = succPNat (y * ↑a') ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ w * b' = succPNat (y * ↑a')
[PROOFSTEP]
apply eq
[GOAL]
case right.right.right.right.left.a
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(w * b') = ↑(succPNat (y * ↑a'))
[PROOFSTEP]
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
[PROOFSTEP]
rw [ha'', hb'']
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * (↑a' * ↑d) = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
repeat' rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * (↑a' * ↑d) = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * (↑a' * ↑d) + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
rw [← @mul_assoc]
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
rw [hza', hwb']
[GOAL]
case right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ (x * ↑b' + 1) * ↑d = x * ↑b' * ↑d + ↑d ∧ (y * ↑a' + 1) * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
constructor
[GOAL]
case right.right.right.right.right.left
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ (x * ↑b' + 1) * ↑d = x * ↑b' * ↑d + ↑d
[PROOFSTEP]
ring
[GOAL]
case right.right.right.right.right.right
a b : ℕ+
d : ℕ+ := gcdD a b
w : ℕ+ := gcdW a b
x : ℕ := gcdX a b
y : ℕ := gcdY a b
z : ℕ+ := gcdZ a b
a' : ℕ+ := gcdA' a b
b' : ℕ+ := gcdB' a b
u : XgcdType := XgcdType.start a b
ur : XgcdType := XgcdType.reduce u
x✝¹ : d = XgcdType.a ur
hb : d = XgcdType.b ur
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = succPNat (x * y)
hdet' : ↑w * ↑z = x * y + 1
x✝ : XgcdType.v u = (↑a, ↑b)
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ (y * ↑a' + 1) * ↑d = y * ↑a' * ↑d + ↑d
[PROOFSTEP]
ring
[GOAL]
a b : ℕ+
⊢ gcdD a b = gcd a b
[PROOFSTEP]
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b = gcd a b
[PROOFSTEP]
apply dvd_antisymm
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ gcd a b
[PROOFSTEP]
apply dvd_gcd
[GOAL]
case intro.intro.intro.intro.intro.intro.a.hm
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ a
case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
[PROOFSTEP]
exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm
[GOAL]
case intro.intro.intro.intro.intro.intro.a.hn
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcdD a b ∣ b
[PROOFSTEP]
exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
have h₇ : (gcd a b : ℕ) ∣ gcdZ a b * a := (Nat.gcd_dvd_left a b).trans (dvd_mul_left _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
have h₈ : (gcd a b : ℕ) ∣ gcdX a b * b := (Nat.gcd_dvd_right a b).trans (dvd_mul_left _ _)
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ ↑(gcdZ a b) * ↑a
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
rw [h₅] at h₇
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ gcd a b ∣ gcdD a b
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro.a
a b : ℕ+
left✝² : gcdW a b * gcdZ a b = succPNat (gcdX a b * gcdY a b)
h₁ : a = gcdA' a b * gcdD a b
h₂ : b = gcdB' a b * gcdD a b
left✝¹ : gcdZ a b * gcdA' a b = succPNat (gcdX a b * ↑(gcdB' a b))
left✝ : gcdW a b * gcdB' a b = succPNat (gcdY a b * ↑(gcdA' a b))
h₅ : ↑(gcdZ a b) * ↑a = gcdX a b * ↑b + ↑(gcdD a b)
right✝ : ↑(gcdW a b) * ↑b = gcdY a b * ↑a + ↑(gcdD a b)
h₇ : ↑(gcd a b) ∣ gcdX a b * ↑b + ↑(gcdD a b)
h₈ : ↑(gcd a b) ∣ gcdX a b * ↑b
⊢ ↑(gcd a b) ∣ ↑(gcdD a b)
[PROOFSTEP]
exact (Nat.dvd_add_iff_right h₈).mpr h₇


[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b x, p { val := a, property := b }) ↔ ∃ h, p { val := n', property := h }
[PROOFSTEP]
simp_rw [mk_coe, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
[PROOFSTEP]
have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
[PROOFSTEP]
have n := Nat.findX this
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }
[PROOFSTEP]
refine' ⟨⟨n, _⟩, _, fun m hm pm => _⟩
[GOAL]
case refine'_1
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ 0 < ↑n
[PROOFSTEP]
obtain ⟨n', hn', -⟩ := n.prop.1
[GOAL]
case refine'_1.intro.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
⊢ 0 < ↑n
[PROOFSTEP]
rw [hn']
[GOAL]
case refine'_1.intro.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
⊢ 0 < ↑n'
[PROOFSTEP]
exact n'.prop
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ p { val := ↑n, property := (_ : 0 < ↑n) }
[PROOFSTEP]
obtain ⟨n', hn', pn'⟩ := n.prop.1
[GOAL]
case refine'_2.intro.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
pn' : p n'
⊢ p { val := ↑n, property := (_ : 0 < ↑n) }
[PROOFSTEP]
simpa [hn', Subtype.coe_eta] using pn'
[GOAL]
case refine'_3
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
m : ℕ+
hm : m < { val := ↑n, property := (_ : 0 < ↑n) }
pm : p m
⊢ False
[PROOFSTEP]
exact n.prop.2 m hm ⟨m, rfl, pm⟩
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ PNat.find h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n
[PROOFSTEP]
constructor
[GOAL]
case mp
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ PNat.find h = m → p m ∧ ∀ (n : ℕ+), n < m → ¬p n
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ+
⊢ p (PNat.find h) ∧ ∀ (n : ℕ+), n < PNat.find h → ¬p n
[PROOFSTEP]
exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩
[GOAL]
case mpr
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ (p m ∧ ∀ (n : ℕ+), n < m → ¬p n) → PNat.find h = m
[PROOFSTEP]
rintro ⟨hm, hlt⟩
[GOAL]
case mpr.intro
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
hm : p m
hlt : ∀ (n : ℕ+), n < m → ¬p n
⊢ PNat.find h = m
[PROOFSTEP]
exact le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n✝ m n : ℕ+
⊢ PNat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m
[PROOFSTEP]
simp only [exists_prop, ← lt_add_one_iff, find_lt_iff]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n✝ m n : ℕ+
⊢ n ≤ PNat.find h ↔ ∀ (m : ℕ+), m < n → ¬p m
[PROOFSTEP]
simp only [← not_lt, find_lt_iff, not_exists, not_and]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n✝ m n : ℕ+
⊢ n < PNat.find h ↔ ∀ (m : ℕ+), m ≤ n → ¬p m
[PROOFSTEP]
simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ PNat.find h = 1 ↔ p 1
[PROOFSTEP]
simp [find_eq_iff]
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n m : ℕ+
⊢ ¬1 < PNat.find h ↔ ¬¬p 1
[PROOFSTEP]
simp
[GOAL]
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n m : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
⊢ PNat.find h = PNat.find h₂ + 1
[PROOFSTEP]
refine' (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n => PNat.recOn n _ _⟩
[GOAL]
case refine'_1
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ 1 < PNat.find h₂ + 1 → ¬p 1
[PROOFSTEP]
simp [h1]
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n : ℕ+
⊢ ∀ (n : ℕ+), (n < PNat.find h₂ + 1 → ¬p n) → n + 1 < PNat.find h₂ + 1 → ¬p (n + 1)
[PROOFSTEP]
intro m _ hm
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m✝ : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : m + 1 < PNat.find h₂ + 1
⊢ ¬p (m + 1)
[PROOFSTEP]
simp only [add_lt_add_iff_right, lt_find_iff] at hm
[GOAL]
case refine'_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h✝ : ∃ n, p n
n✝ m✝ : ℕ+
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
n m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
⊢ ¬p (m + 1)
[PROOFSTEP]
exact hm _ le_rfl