[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
⊢ ↑i 0 = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i 0)
[PROOFSTEP]
simp only [eval_zero, RingHom.map_zero, mul_zero, Polynomial.map_zero]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ DenomsClearable a b N (↑C r * X ^ n) i
[PROOFSTEP]
refine' ⟨r * a ^ n * b ^ (N - n), bi, bu, _⟩
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i (↑C r * X ^ n))
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * (↑i r * eval (↑i a * bi) X ^ n)
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, eval_X, mul_comm]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n) * (↑i r * ↑i a ^ n) = ↑i b ^ N * (↑i r * (↑i a * bi) ^ n)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le nN]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
[PROOFSTEP]
conv_lhs => rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
| ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n)
[PROOFSTEP]
rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
| ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n)
[PROOFSTEP]
rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
| ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n)
[PROOFSTEP]
rw [← mul_one (i a), ← bu]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * (↑i a * (bi * ↑i b)) ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
[PROOFSTEP]
simp [mul_assoc, mul_comm, mul_left_comm, pow_add, mul_pow]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i (Df + Dg) = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i (f + g))
[PROOFSTEP]
rw [RingHom.map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
[GOAL]
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f) + ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g) =
    ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f) + ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i g)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a.e_a
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ bg = bf
[PROOFSTEP]
refine' @inv_unique K _ (i b) bg bf _ _
[GOAL]
case e_a.e_a.e_a.e_a.refine'_1
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i b * bg = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
case e_a.e_a.e_a.e_a.refine'_2
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
bi : K
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * ↑i b = 1
Hf : ↑i Df = ↑i b ^ N * eval (↑i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * ↑i b = 1
Hg : ↑i Dg = ↑i b ^ N * eval (↑i a * bg) (Polynomial.map i g)
⊢ ↑i b * bf = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
obtain ⟨ev, bi, bu, hF⟩ :=
  denomsClearable_natDegree (b := b) (algebraMap ℤ K) f a
    (by
      rw [eq_intCast, one_div_mul_cancel]
      rw [Int.cast_ne_zero]
      exact b0.ne.symm)
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ?m.165182 * ↑(algebraMap ℤ K) b = 1
[PROOFSTEP]
rw [eq_intCast, one_div_mul_cancel]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ↑b ≠ 0
[PROOFSTEP]
rw [Int.cast_ne_zero]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0
[PROOFSTEP]
exact b0.ne.symm
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
obtain Fa := _root_.congr_arg abs hF
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |↑(algebraMap ℤ K) ev| =
    |↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa 
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = |↑b ^ natDegree f| * |eval (↑(algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
rw [abs_of_pos (pow_pos (Int.cast_pos.mpr b0) _ : 0 < (b : K) ^ _), one_div, eq_intCast] at Fa 
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ natDegree f * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
[PROOFSTEP]
rw [div_eq_mul_inv, ← Fa, ← Int.cast_abs, ← Int.cast_one, Int.cast_le]
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |ev|
[PROOFSTEP]
refine' Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab _))
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) ev =
    ↑(algebraMap ℤ K) b ^ natDegree f * eval (↑(algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF 
[GOAL]
case intro.intro.intro
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
hF :
  ↑(algebraMap ℤ K) b ^ natDegree f = 0 ∨
    eval (↑(algebraMap ℤ K) a * (↑(algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
cases' hF with hF hF
[GOAL]
case intro.intro.intro.inl
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : ↑(algebraMap ℤ K) b ^ natDegree f = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (pow_eq_zero hF)))).elim
[GOAL]
case intro.intro.intro.inr
K : Type u_1
inst✝ : LinearOrderedField K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * ↑(algebraMap ℤ K) b = 1
Fa : |↑ev| = ↑b ^ natDegree f * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : eval (↑(algebraMap ℤ K) a * (↑(algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
[PROOFSTEP]
rwa [div_eq_mul_inv]
