R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : RingHom.Finite (algebraMap R A)
⊢ Module.Finite R A
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
⊢ Module.Finite R A
have :=
  h.to_finite
    (by
      rw [RingHom.FiniteType]
      convert h'
      refine IsScalarTower.Algebra.ext (algebraMap R A).toAlgebra _ fun r x => ?_
      exact (Algebra.smul_def _ _).symm)
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : Module.Finite R A
⊢ Module.Finite R A
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : RingHom.Finite (algebraMap R A)
⊢ Module.Finite R A
rw [RingHom.Finite] at this
case h.e'_5.h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : Module.Finite R A
⊢ inst✝¹ = RingHom.toAlgebra (algebraMap R A)
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : Module.Finite R A
⊢ Module.Finite R A
convert this
case h.e'_5.h.e'_5.h
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : Module.Finite R A
r✝ : R
x✝ : A
⊢ (let_fun I := inst✝¹;
    r✝ • x✝) =
    r✝ • x✝
case h.e'_5.h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : Module.Finite R A
⊢ inst✝¹ = RingHom.toAlgebra (algebraMap R A)
ext
no goals
case h.e'_5.h.e'_5.h
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
this : Module.Finite R A
r✝ : R
x✝ : A
⊢ (let_fun I := inst✝¹;
    r✝ • x✝) =
    r✝ • x✝
exact Algebra.smul_def _ _
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
⊢ FiniteType R A
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
⊢ RingHom.FiniteType (algebraMap R A)
rw [RingHom.FiniteType]
case h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
⊢ RingHom.toAlgebra (algebraMap R A) = inst✝¹
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
⊢ FiniteType R A
convert h'
case h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
r : R
x : A
⊢ (let_fun I := RingHom.toAlgebra (algebraMap R A);
    r • x) =
    r • x
case h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
⊢ RingHom.toAlgebra (algebraMap R A) = inst✝¹
refine IsScalarTower.Algebra.ext (algebraMap R A).toAlgebra _ fun r x => ?_
no goals
case h.e'_5
R : Type u_1
A : Type u_2
B : Type ?u.621954
S : Type ?u.621957
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : Algebra.IsIntegral R A
h' : FiniteType R A
r : R
x : A
⊢ (let_fun I := RingHom.toAlgebra (algebraMap R A);
    r • x) =
    r • x
exact (Algebra.smul_def _ _).symm