R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
⊢ RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) ↔
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
⊢ RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) ↔
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
let g := Ideal.Quotient.mk (I.comap f)
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this :
  RingHom.comp (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) g = RingHom.comp (Ideal.Quotient.mk I) f
⊢ RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) ↔
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
⊢ RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) ↔
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f :=
  Ideal.quotientMap_comp_mk le_rfl
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this :
  RingHom.comp (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) g = RingHom.comp (Ideal.Quotient.mk I) f
h : RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this :
  RingHom.comp (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) g = RingHom.comp (Ideal.Quotient.mk I) f
⊢ RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) ↔
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
refine' ⟨fun h => _, fun h => RingHom.isIntegral_tower_top_of_isIntegral g _ (this ▸ h)⟩
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this :
  RingHom.comp (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) g = RingHom.comp (Ideal.Quotient.mk I) f
h : RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))
⊢ RingHom.IsIntegral g
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this :
  RingHom.comp (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) g = RingHom.comp (Ideal.Quotient.mk I) f
h : RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)
refine' this ▸ RingHom.isIntegral_trans g (Ideal.quotientMap I f le_rfl) _ h
no goals
R : Type u_2
A : Type ?u.1589122
B : Type ?u.1589125
S : Type u_1
T : Type ?u.1589131
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g✝ : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this :
  RingHom.comp (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) g = RingHom.comp (Ideal.Quotient.mk I) f
h : RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))
⊢ RingHom.IsIntegral g
exact RingHom.isIntegral_of_surjective g Ideal.Quotient.mk_surjective