[GOAL]
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => IsIntegral f
[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 : IsIntegral f
hg : IsIntegral g
⊢ IsIntegral (comp g f)
[PROOFSTEP]
exact RingHom.isIntegral_trans _ _ hf hg
[GOAL]
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f => IsIntegral f
[PROOFSTEP]
apply isIntegral_stableUnderComposition.respectsIso
[GOAL]
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), IsIntegral (RingEquiv.toRingHom e)
[PROOFSTEP]
introv x
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ IsIntegralElem (RingEquiv.toRingHom e) x
[PROOFSTEP]
rw [← e.apply_symm_apply x]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ IsIntegralElem (RingEquiv.toRingHom e) (↑e (↑(RingEquiv.symm e) x))
[PROOFSTEP]
apply RingHom.is_integral_map
[GOAL]
⊢ StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => IsIntegral f
[PROOFSTEP]
refine' StableUnderBaseChange.mk _ isIntegral_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], IsIntegral (algebraMap R T) → IsIntegral includeLeftRingHom
[PROOFSTEP]
introv h x
[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 : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ IsIntegralElem includeLeftRingHom x
[PROOFSTEP]
refine' TensorProduct.induction_on x _ _ _
[GOAL]
case refine'_1
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ IsIntegralElem includeLeftRingHom 0
[PROOFSTEP]
apply isIntegral_zero
[GOAL]
case refine'_2
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ ∀ (x : S) (y : T), IsIntegralElem includeLeftRingHom (x ⊗ₜ[R] y)
[PROOFSTEP]
intro x y
[GOAL]
case refine'_2
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x✝ : S ⊗[R] T
x : S
y : T
⊢ IsIntegralElem includeLeftRingHom (x ⊗ₜ[R] y)
[PROOFSTEP]
exact IsIntegral.tmul x (h y)
[GOAL]
case refine'_3
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ ∀ (x y : S ⊗[R] T),
    IsIntegralElem includeLeftRingHom x →
      IsIntegralElem includeLeftRingHom y → IsIntegralElem includeLeftRingHom (x + y)
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine'_3
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x✝ x y : S ⊗[R] T
hx : IsIntegralElem includeLeftRingHom x
hy : IsIntegralElem includeLeftRingHom y
⊢ IsIntegralElem includeLeftRingHom (x + y)
[PROOFSTEP]
exact isIntegral_add hx hy
