-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma Hom.toAlgHom_comp_apply
    [Algebra R R''] [IsScalarTower R R' R''] [IsScalarTower R' R'' S'']
    [IsScalarTower R' S' S''] [IsScalarTower S S' S'']
    (f : Hom P P') (g : Hom P' P'') (x) :
    (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)

Proof state:
case h_C
R : Type u
S : Type v
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_4
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_1
S'' : Type u_3
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
r : R
⊢ (g.comp f).toAlgHom (C r) = g.toAlgHom (f.toAlgHom (C r))

Tactic:
simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_4
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_1
S'' : Type u_3
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : P.Ring
⊢ (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)

Tactic:
induction x using MvPolynomial.induction_on with
| h_C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
| h_add x y hx hy => simp only [map_add, hx, hy]
| h_X p i hp => simp only [map_mul, hp, toAlgHom_X, comp_val]; rfl

Result:
no goals

Proof state:
case h_X
R : Type u
S : Type v
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_4
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_1
S'' : Type u_3
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial P.vars R
i : P.vars
hp : (g.comp f).toAlgHom p = g.toAlgHom (f.toAlgHom p)
⊢ g.toAlgHom (f.toAlgHom p) * (aeval g.val) (f.val i) = g.toAlgHom (f.toAlgHom p) * g.toAlgHom (f.val i)

Tactic:
rfl

Result:
no goals

Proof state:
case h_add
R : Type u
S : Type v
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_4
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_1
S'' : Type u_3
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x y : MvPolynomial P.vars R
hx : (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)
hy : (g.comp f).toAlgHom y = g.toAlgHom (f.toAlgHom y)
⊢ (g.comp f).toAlgHom (x + y) = g.toAlgHom (f.toAlgHom (x + y))

Tactic:
simp only [map_add, hx, hy]

Result:
no goals

Proof state:
case h_X
R : Type u
S : Type v
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_4
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_1
S'' : Type u_3
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial P.vars R
i : P.vars
hp : (g.comp f).toAlgHom p = g.toAlgHom (f.toAlgHom p)
⊢ (g.comp f).toAlgHom (p * X i) = g.toAlgHom (f.toAlgHom (p * X i))

Tactic:
simp only [map_mul, hp, toAlgHom_X, comp_val]

Result:
case h_X
R : Type u
S : Type v
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_4
inst✝¹⁶ : CommRing R'
inst✝¹⁵ : CommRing S'
inst✝¹⁴ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_1
S'' : Type u_3
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Generators R'' S''
inst✝¹⁰ : Algebra R R'
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R' S''
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra S' S''
inst✝⁵ : Algebra S S''
inst✝⁴ : Algebra R R''
inst✝³ : IsScalarTower R R' R''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R' S' S''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
p : MvPolynomial P.vars R
i : P.vars
hp : (g.comp f).toAlgHom p = g.toAlgHom (f.toAlgHom p)
⊢ g.toAlgHom (f.toAlgHom p) * (aeval g.val) (f.val i) = g.toAlgHom (f.toAlgHom p) * g.toAlgHom (f.val i)