-- Mathlib/RingTheory/Generators.lean
lemma ofComp_kerCompPreimage (Q : Generators S T) (P : Generators R S) (x : Q.ker) :
    (Q.ofComp P).toAlgHom (kerCompPreimage Q P x) = x

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
⊢ (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ∑ v ∈ support ↑x, (monomial v) (coeff v ↑x)

Tactic:
rw [kerCompPreimage, map_finsupp_sum, Finsupp.sum]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
⊢ ∑ a ∈ (↑x).support,
      (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x a)) * (monomial (Finsupp.mapDomain Sum.inl a)) 1) =
    ∑ v ∈ support ↑x, (monomial v) (coeff v ↑x)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x j)) * (monomial (Finsupp.mapDomain Sum.inl j)) 1) =
    (monomial j) (coeff j ↑x)

Tactic:
simp only [AlgHom.toLinearMap_apply, _root_.map_mul, Hom.toAlgHom_monomial]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x j))) *
      1 • (Finsupp.mapDomain Sum.inl j).prod fun x1 x2 => (Q.ofComp P).val x1 ^ x2) =
    (monomial j) (coeff j ↑x)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
⊢ (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ↑x

Tactic:
conv_rhs => rw [← x.1.support_sum_monomial_coeff]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
⊢ (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ∑ v ∈ support ↑x, (monomial v) (coeff v ↑x)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i => C (P.val i)) (P.σ (↑x j)) * j.prod fun a b => X a ^ b) = C (coeff j ↑x) * j.prod fun n e => X n ^ e

Tactic:
congr 1

Result:
case e_a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (aeval fun i => C (P.val i)) (P.σ (↑x j)) = C (coeff j ↑x)

Proof state:
case e_a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (algebraMap S Q.Ring) (↑x j) = (algebraMap S (MvPolynomial Q.vars S)) (coeff j ↑x)

Tactic:
simp [coeff]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x j))) * j.prod fun a b => (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

Tactic:
rw [rename, ← AlgHom.comp_apply, comp_aeval]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i => (Q.ofComp P).toAlgHom ((X ∘ Sum.inr) i)) (P.σ (↑x j)) *
      j.prod fun a b => (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x j))) *
      1 • (Finsupp.mapDomain Sum.inl j).prod fun x1 x2 => (Q.ofComp P).val x1 ^ x2) =
    (monomial j) (coeff j ↑x)

Tactic:
rw [one_smul, Finsupp.prod_mapDomain_index_inj Sum.inl_injective]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x j))) * j.prod fun a b => (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

Proof state:
case e_a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (aeval fun i => C (P.val i)) (P.σ (↑x j)) = C (coeff j ↑x)

Tactic:
rw [aeval_def, IsScalarTower.algebraMap_eq R S, ← MvPolynomial.algebraMap_eq,
  ← coe_eval₂Hom, ← map_aeval, P.aeval_val_σ]

Result:
case e_a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (algebraMap S Q.Ring) (↑x j) = (algebraMap S (MvPolynomial Q.vars S)) (coeff j ↑x)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
⊢ ∑ a ∈ (↑x).support,
      (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x a)) * (monomial (Finsupp.mapDomain Sum.inl a)) 1) =
    ∑ v ∈ support ↑x, (monomial v) (coeff v ↑x)

Tactic:
refine Finset.sum_congr rfl fun j _ ↦ ?_

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (Q.ofComp P).toAlgHom ((rename Sum.inr) (P.σ (↑x j)) * (monomial (Finsupp.mapDomain Sum.inl j)) 1) =
    (monomial j) (coeff j ↑x)