-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem left_inv (x : A ⊗ R[X]) : invFun R A ((toFunAlgHom R A) x) = x

Proof state:
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

Tactic:
dsimp only [invFun]

Result:
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

Proof state:
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

Tactic:
intro p q hp hq

Result:
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

Proof state:
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

Tactic:
intro a p

Result:
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

Proof state:
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

Tactic:
rw [toFunAlgHom_apply_tmul, eval₂_sum]

Result:
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]
⊢ (p.sum fun n a_1 => eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((monomial n) (a * (algebraMap R A) a_1))) = a ⊗ₜ[R] p

Proof state:
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]
⊢ (p.sum fun n a_1 => eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((monomial n) (a * (algebraMap R A) a_1))) = a ⊗ₜ[R] p

Tactic:
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]

Result:
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] ∑ a ∈ p.support, p.coeff a • X ^ a = a ⊗ₜ[R] p

Proof state:
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

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_

Result:
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

Proof state:
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

Tactic:
simp [invFun]

Result:
no goals

Proof state:
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

Tactic:
simp only [map_add, invFun_add, hp, hq]

Result:
no goals

Proof state:
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] ∑ x ∈ p.support, (algebraMap R R[X]) (p.coeff x) * X ^ x = a ⊗ₜ[R] p.sum fun n a => C a * X ^ n

Tactic:
rfl

Result:
no goals

Proof state:
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] ∑ a ∈ p.support, p.coeff a • X ^ a = a ⊗ₜ[R] p

Tactic:
conv_rhs => rw [← sum_C_mul_X_pow_eq p]

Result:
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] ∑ a ∈ p.support, p.coeff a • X ^ a = a ⊗ₜ[R] p.sum fun n a => C a * X ^ n

Proof state:
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] ∑ a ∈ p.support, p.coeff a • X ^ a = a ⊗ₜ[R] p.sum fun n a => C a * X ^ n

Tactic:
simp only [Algebra.smul_def]

Result:
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] ∑ x ∈ p.support, (algebraMap R R[X]) (p.coeff x) * X ^ x = a ⊗ₜ[R] p.sum fun n a => C a * X ^ n