-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem isIntegral_quotientMap_iff {I : Ideal S} :
    (Ideal.quotientMap I f le_rfl).IsIntegral ↔
      ((Ideal.Quotient.mk I).comp f : R →+* S ⧸ I).IsIntegral

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f :=
  Ideal.quotientMap_comp_mk le_rfl

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
h : (Ideal.quotientMap I f ⋯).IsIntegral
⊢ g.IsIntegral

Tactic:
exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

Result:
no goals

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
h : (Ideal.quotientMap I f ⋯).IsIntegral
⊢ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
h : (Ideal.quotientMap I f ⋯).IsIntegral
⊢ g.IsIntegral

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
let g := Ideal.Quotient.mk (I.comap f)

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
h : (Ideal.quotientMap I f ⋯).IsIntegral
⊢ ((Ideal.Quotient.mk I).comp f).IsIntegral