-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
@[simp]
lemma algebraTensorAlgEquiv_symm_monomial (m : σ →₀ ℕ) (a : A) :
    (algebraTensorAlgEquiv R A).symm (monomial m a) = a ⊗ₜ monomial m 1

Proof state:
case h0
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
⊢ (algebraTensorAlgEquiv R A).symm ((monomial 0) a) = a ⊗ₜ[R] (monomial 0) 1

Tactic:
simp [algebraTensorAlgEquiv]

Result:
no goals

Proof state:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ a ⊗ₜ[R] (monomial f) 1 * 1 ⊗ₜ[R] (X i ^ n) = (a * 1) ⊗ₜ[R] ((monomial f) 1 * X i ^ n)

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul]

Result:
no goals

Proof state:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial (Finsupp.single i n + f)) a) = a ⊗ₜ[R] (monomial (Finsupp.single i n + f)) 1

Tactic:
simp only [add_comm, monomial_add_single, _root_.map_mul, map_pow, aeval_X,
  Algebra.TensorProduct.tmul_pow, one_pow, hfa]

Result:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ a ⊗ₜ[R] (monomial f) 1 * 1 ⊗ₜ[R] (X i ^ n) = a ⊗ₜ[R] ((monomial f) 1 * X i ^ n)

Proof state:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (algebraTensorAlgEquiv R A).symm ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ (algebraTensorAlgEquiv R A).symm ((monomial (Finsupp.single i n + f)) a) =
    a ⊗ₜ[R] (monomial (Finsupp.single i n + f)) 1

Tactic:
simp only [algebraTensorAlgEquiv, AlgEquiv.ofAlgHom_symm_apply] at hfa ⊢

Result:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial (Finsupp.single i n + f)) a) = a ⊗ₜ[R] (monomial (Finsupp.single i n + f)) 1

Proof state:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ a ⊗ₜ[R] (monomial f) 1 * 1 ⊗ₜ[R] (X i ^ n) = a ⊗ₜ[R] ((monomial f) 1 * X i ^ n)

Tactic:
nth_rw 2 [← mul_one a]

Result:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (aeval fun s => 1 ⊗ₜ[R] X s) ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ a ⊗ₜ[R] (monomial f) 1 * 1 ⊗ₜ[R] (X i ^ n) = (a * 1) ⊗ₜ[R] ((monomial f) 1 * X i ^ n)

Proof state:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support →
      b ≠ 0 →
        (algebraTensorAlgEquiv R A).symm ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1 →
          (algebraTensorAlgEquiv R A).symm ((monomial (Finsupp.single a_1 b + f)) a) =
            a ⊗ₜ[R] (monomial (Finsupp.single a_1 b + f)) 1

Tactic:
intro i n f _ _ hfa

Result:
case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
a✝¹ : i ∉ f.support
a✝ : n ≠ 0
hfa : (algebraTensorAlgEquiv R A).symm ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1
⊢ (algebraTensorAlgEquiv R A).symm ((monomial (Finsupp.single i n + f)) a) =
    a ⊗ₜ[R] (monomial (Finsupp.single i n + f)) 1

Proof state:
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
⊢ (algebraTensorAlgEquiv R A).symm ((monomial m) a) = a ⊗ₜ[R] (monomial m) 1

Tactic:
apply @Finsupp.induction σ ℕ _ _ m

Result:
case h0
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
⊢ (algebraTensorAlgEquiv R A).symm ((monomial 0) a) = a ⊗ₜ[R] (monomial 0) 1

case ha
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
m : σ →₀ ℕ
a : A
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support →
      b ≠ 0 →
        (algebraTensorAlgEquiv R A).symm ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1 →
          (algebraTensorAlgEquiv R A).symm ((monomial (Finsupp.single a_1 b + f)) a) =
            a ⊗ₜ[R] (monomial (Finsupp.single a_1 b + f)) 1