-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma aeval_one_tmul (f : σ → S) (p : MvPolynomial σ R) :
    (aeval fun x ↦ (1 ⊗ₜ[R] f x : N ⊗[R] S)) p = 1 ⊗ₜ[R] (aeval f) p

Proof state:
case h_add
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p q : MvPolynomial σ R
hp : (aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
hq : (aeval fun x => 1 ⊗ₜ[R] f x) q = 1 ⊗ₜ[R] (aeval f) q
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) (p + q) = 1 ⊗ₜ[R] (aeval f) (p + q)

Tactic:
simp [hp, hq, tmul_add]

Result:
no goals

Proof state:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p

Tactic:
induction' p using MvPolynomial.induction_on with a p q hp hq p i h

Result:
case h_C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) (C a) = 1 ⊗ₜ[R] (aeval f) (C a)

case h_add
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p q : MvPolynomial σ R
hp : (aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
hq : (aeval fun x => 1 ⊗ₜ[R] f x) q = 1 ⊗ₜ[R] (aeval f) q
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) (p + q) = 1 ⊗ₜ[R] (aeval f) (p + q)

case h_X
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
i : σ
h : (aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) (p * X i) = 1 ⊗ₜ[R] (aeval f) (p * X i)

Proof state:
case h_C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) (C a) = 1 ⊗ₜ[R] (aeval f) (C a)

Tactic:
simp only [map_C, algHom_C, Algebra.TensorProduct.algebraMap_apply,
  RingHomCompTriple.comp_apply]

Result:
case h_C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ (algebraMap R N) a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) a

Proof state:
case h_X
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
i : σ
h : (aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p
⊢ (aeval fun x => 1 ⊗ₜ[R] f x) (p * X i) = 1 ⊗ₜ[R] (aeval f) (p * X i)

Tactic:
simp [h]

Result:
no goals

Proof state:
case h_C
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
a : R
⊢ (algebraMap R N) a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) a

Tactic:
rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]

Result:
no goals