case h
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ RingHom.Finite (algebraMap R A)
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ Algebra.IsIntegral R A
apply RingHom.Finite.to_isIntegral
case h
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ Module.Finite R A
case h
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ RingHom.Finite (algebraMap R A)
rw [RingHom.Finite]
case h.e'_5.h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ RingHom.toAlgebra (algebraMap R A) = inst✝¹
case h
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ Module.Finite R A
convert h
case h.e'_5.h.e'_5.h
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
r✝ : R
x✝ : A
⊢ (let_fun I := RingHom.toAlgebra (algebraMap R A);
    r✝ • x✝) =
    r✝ • x✝
case h.e'_5.h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
⊢ RingHom.toAlgebra (algebraMap R A) = inst✝¹
ext
no goals
case h.e'_5.h.e'_5.h
R : Type u_1
A : Type u_2
B : Type ?u.630412
S : Type ?u.630415
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Module.Finite R A
r✝ : R
x✝ : A
⊢ (let_fun I := RingHom.toAlgebra (algebraMap R A);
    r✝ • x✝) =
    r✝ • x✝
exact (Algebra.smul_def _ _).symm