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)
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))
rw [RingHom.map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
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
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)
congr
no goals
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
refine' @inv_unique K _ (i b) bg bf _ _ <;> rwa [mul_comm]