[GOAL]
⊢ StableUnderComposition @Finite
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Finite f
hg : Finite g
⊢ Finite (comp g f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
⊢ RespectsIso @Finite
[PROOFSTEP]
apply finite_stableUnderComposition.respectsIso
[GOAL]
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Finite (RingEquiv.toRingHom e)
[PROOFSTEP]
intros
[GOAL]
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e✝ : R✝ ≃+* S✝
⊢ Finite (RingEquiv.toRingHom e✝)
[PROOFSTEP]
exact Finite.of_surjective _ (RingEquiv.toEquiv _).surjective
[GOAL]
⊢ StableUnderBaseChange @Finite
[PROOFSTEP]
refine StableUnderBaseChange.mk _ finite_respectsIso ?_
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Finite (algebraMap R T) → Finite includeLeftRingHom
[PROOFSTEP]
classical
introv h
replace h : Module.Finite R T := by rw [RingHom.Finite] at h ; convert h; ext; intros; simp_rw [Algebra.smul_def]; rfl
suffices Module.Finite S (S ⊗[R] T) by rw [RingHom.Finite]; convert this; congr; ext; intros;
  simp_rw [Algebra.smul_def]; rfl
exact inferInstance
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Finite (algebraMap R T) → Finite includeLeftRingHom
[PROOFSTEP]
introv h
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Finite (algebraMap R T)
⊢ Finite includeLeftRingHom
[PROOFSTEP]
replace h : Module.Finite R T := by rw [RingHom.Finite] at h ; convert h; ext; intros; simp_rw [Algebra.smul_def]; rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Finite (algebraMap R T)
⊢ Module.Finite R T
[PROOFSTEP]
rw [RingHom.Finite] at h 
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Module.Finite R T
[PROOFSTEP]
convert h
[GOAL]
case h.e'_5.h.e'_5
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ inst✝ = toAlgebra (algebraMap R T)
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
r✝ : R
x✝ : T
⊢ (let_fun I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
intros
[GOAL]
case h.e'_5.h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
r✝ : R
x✝ : T
⊢ (let_fun I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
r✝ : R
x✝ : T
⊢ ↑(algebraMap R T) r✝ * x✝ = r✝ • x✝
[PROOFSTEP]
rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Finite includeLeftRingHom
[PROOFSTEP]
suffices Module.Finite S (S ⊗[R] T) by rw [RingHom.Finite]; convert this; congr; ext; intros;
  simp_rw [Algebra.smul_def]; rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
⊢ Finite includeLeftRingHom
[PROOFSTEP]
rw [RingHom.Finite]
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
⊢ Module.Finite S (S ⊗[R] T)
[PROOFSTEP]
convert this
[GOAL]
case h.e'_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
⊢ Algebra.toModule = leftModule
[PROOFSTEP]
congr
[GOAL]
case h.e'_5.h.h.e_5.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
⊢ toAlgebra includeLeftRingHom = leftAlgebra
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.h.e_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := toAlgebra includeLeftRingHom;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
intros
[GOAL]
case h.e'_5.h.h.e_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := toAlgebra includeLeftRingHom;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h.h.e_5.h.h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
this : Module.Finite S (S ⊗[R] T)
e_4✝ :
  NonUnitalNonAssocSemiring.toAddCommMonoid =
    instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule
r✝ : S
x✝ : S ⊗[R] T
⊢ r✝ • x✝ = ↑(algebraMap S (S ⊗[R] T)) r✝ * x✝
[PROOFSTEP]
rfl
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Module.Finite S (S ⊗[R] T)
[PROOFSTEP]
exact inferInstance
