case refine_1
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    ↑(toFunAlgHom R A) (invFun R A p) = p →
      ↑(toFunAlgHom R A) (invFun R A q) = q → ↑(toFunAlgHom R A) (invFun R A (p + q)) = p + q

case refine_2
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), ↑(toFunAlgHom R A) (invFun R A (↑(monomial n) a)) = ↑(monomial n) a
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ↑(toFunAlgHom R A) (invFun R A x) = x
refine Polynomial.induction_on' x ?_ ?_
case refine_1
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A[X]
hp : ↑(toFunAlgHom R A) (invFun R A p) = p
hq : ↑(toFunAlgHom R A) (invFun R A q) = q
⊢ ↑(toFunAlgHom R A) (invFun R A (p + q)) = p + q
case refine_1
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    ↑(toFunAlgHom R A) (invFun R A p) = p →
      ↑(toFunAlgHom R A) (invFun R A q) = q → ↑(toFunAlgHom R A) (invFun R A (p + q)) = p + q
intro p q hp hq
no goals
case refine_1
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A[X]
hp : ↑(toFunAlgHom R A) (invFun R A p) = p
hq : ↑(toFunAlgHom R A) (invFun R A q) = q
⊢ ↑(toFunAlgHom R A) (invFun R A (p + q)) = p + q
simp only [invFun_add, AlgHom.map_add, hp, hq]
case refine_2
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ ↑(toFunAlgHom R A) (invFun R A (↑(monomial n) a)) = ↑(monomial n) a
case refine_2
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), ↑(toFunAlgHom R A) (invFun R A (↑(monomial n) a)) = ↑(monomial n) a
intro n a
no goals
case refine_2
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ ↑(toFunAlgHom R A) (invFun R A (↑(monomial n) a)) = ↑(monomial n) a
rw [invFun_monomial, Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_pow,
    one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
    X_pow_eq_monomial, sum_monomial_index] <;>
  simp