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

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_4
S' : Type u_1
inst✝²² : CommRing R'
inst✝²¹ : CommRing S'
inst✝²⁰ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_2
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 S'
inst✝⁹ : IsScalarTower R S S'
inst✝⁸ : Algebra R R''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : IsScalarTower R S S''
inst✝⁴ : IsScalarTower R' R'' S''
inst✝³ : IsScalarTower R' S' S''
inst✝² : IsScalarTower S S' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
⊢ (f.comp g).toExtensionHom = f.toExtensionHom.comp g.toExtensionHom

Tactic:
ext

Result:
case toRingHom.a
R : Type u
S : Type v
inst✝²⁵ : CommRing R
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
P : Generators R S
R' : Type u_4
S' : Type u_1
inst✝²² : CommRing R'
inst✝²¹ : CommRing S'
inst✝²⁰ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_2
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 S'
inst✝⁹ : IsScalarTower R S S'
inst✝⁸ : Algebra R R''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : IsScalarTower R S S''
inst✝⁴ : IsScalarTower R' R'' S''
inst✝³ : IsScalarTower R' S' S''
inst✝² : IsScalarTower S S' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
x✝ : P.toExtension.Ring
⊢ (f.comp g).toExtensionHom.toRingHom x✝ = (f.toExtensionHom.comp g.toExtensionHom).toRingHom x✝

Proof state:
case toRingHom.a
R : Type u
S : Type v
inst✝²⁵ : CommRing R
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
P : Generators R S
R' : Type u_4
S' : Type u_1
inst✝²² : CommRing R'
inst✝²¹ : CommRing S'
inst✝²⁰ : Algebra R' S'
P' : Generators R' S'
R'' : Type u_2
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 S'
inst✝⁹ : IsScalarTower R S S'
inst✝⁸ : Algebra R R''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : IsScalarTower R S S''
inst✝⁴ : IsScalarTower R' R'' S''
inst✝³ : IsScalarTower R' S' S''
inst✝² : IsScalarTower S S' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower R R' S'
f : P'.Hom P''
g : P.Hom P'
x✝ : P.toExtension.Ring
⊢ (f.comp g).toExtensionHom.toRingHom x✝ = (f.toExtensionHom.comp g.toExtensionHom).toRingHom x✝

Tactic:
simp

Result:
no goals