case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A (↑(toFunAlgHom R A) 0) = 0

case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A (↑(toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y

case refine_3
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A (↑(toFunAlgHom R A) x) = x →
      invFun R A (↑(toFunAlgHom R A) y) = y → invFun R A (↑(toFunAlgHom R A) (x + y)) = x + y
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A (↑(toFunAlgHom R A) x) = x
refine TensorProduct.induction_on x ?_ ?_ ?_
no goals
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A (↑(toFunAlgHom R A) 0) = 0
simp [invFun]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ invFun R A (↑(toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A (↑(toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y
intro a p
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (↑(toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ invFun R A (↑(toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
dsimp only [invFun]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (sum p fun n a_1 => eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (↑(monomial n) (a * ↑(algebraMap R A) a_1))) = a ⊗ₜ[R] p
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (↑(toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
rw [toFunAlgHom_apply_tmul, eval₂_sum]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun a => coeff p a • X ^ a) = a ⊗ₜ[R] p
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (sum p fun n a_1 => eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (↑(monomial n) (a * ↑(algebraMap R A) a_1))) = a ⊗ₜ[R] p
simp_rw [eval₂_monomial, AlgHom.coe_toRingHom, Algebra.TensorProduct.tmul_pow, one_pow,
  Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one,
  one_mul, ← Algebra.commutes, ← Algebra.smul_def, smul_tmul, sum_def, ← tmul_sum]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun a => coeff p a • X ^ a) = a ⊗ₜ[R] sum p fun n a => ↑C a * X ^ n
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun a => coeff p a • X ^ a) = a ⊗ₜ[R] p
conv_rhs => rw [← sum_C_mul_X_pow_eq p]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun x => ↑(algebraMap R R[X]) (coeff p x) * X ^ x) =
    a ⊗ₜ[R] sum p fun n a => ↑C a * X ^ n
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun a => coeff p a • X ^ a) = a ⊗ₜ[R] sum p fun n a => ↑C a * X ^ n
simp only [Algebra.smul_def]
no goals
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun x => ↑(algebraMap R R[X]) (coeff p x) * X ^ x) =
    a ⊗ₜ[R] sum p fun n a => ↑C a * X ^ n
rfl
case refine_3
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A ⊗[R] R[X]
hp : invFun R A (↑(toFunAlgHom R A) p) = p
hq : invFun R A (↑(toFunAlgHom R A) q) = q
⊢ invFun R A (↑(toFunAlgHom R A) (p + q)) = p + q
case refine_3
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A (↑(toFunAlgHom R A) x) = x →
      invFun R A (↑(toFunAlgHom R A) y) = y → invFun R A (↑(toFunAlgHom R A) (x + y)) = x + y
intro p q hp hq
no goals
case refine_3
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A ⊗[R] R[X]
hp : invFun R A (↑(toFunAlgHom R A) p) = p
hq : invFun R A (↑(toFunAlgHom R A) q) = q
⊢ invFun R A (↑(toFunAlgHom R A) (p + q)) = p + q
simp only [AlgHom.map_add, invFun_add, hp, hq]