-- Mathlib/RingTheory/RingHom/Integral.lean
theorem isIntegral_isStableUnderBaseChange : IsStableUnderBaseChange fun f => f.IsIntegral

Proof state:
⊢ ∀ ⦃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], (algebraMap R T).IsIntegral → includeLeftRingHom.IsIntegral

Tactic:
introv h x

Result:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ includeLeftRingHom.IsIntegralElem x

Proof state:
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 : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ includeLeftRingHom.IsIntegralElem 0

Tactic:
apply isIntegral_zero

Result:
no goals

Proof state:
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 : (algebraMap R T).IsIntegral
x✝ x y : S ⊗[R] T
hx : includeLeftRingHom.IsIntegralElem x
hy : includeLeftRingHom.IsIntegralElem y
⊢ includeLeftRingHom.IsIntegralElem (x + y)

Tactic:
exact IsIntegral.add hx hy

Result:
no goals

Proof state:
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 : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ ∀ (x y : S ⊗[R] T),
    includeLeftRingHom.IsIntegralElem x →
      includeLeftRingHom.IsIntegralElem y → includeLeftRingHom.IsIntegralElem (x + y)

Tactic:
intro x y hx hy

Result:
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 : (algebraMap R T).IsIntegral
x✝ x y : S ⊗[R] T
hx : includeLeftRingHom.IsIntegralElem x
hy : includeLeftRingHom.IsIntegralElem y
⊢ includeLeftRingHom.IsIntegralElem (x + y)

Proof state:
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 : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ ∀ (x : S) (y : T), includeLeftRingHom.IsIntegralElem (x ⊗ₜ[R] y)

Tactic:
intro x y

Result:
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 : (algebraMap R T).IsIntegral
x✝ : S ⊗[R] T
x : S
y : T
⊢ includeLeftRingHom.IsIntegralElem (x ⊗ₜ[R] y)

Proof state:
⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral

Tactic:
refine IsStableUnderBaseChange.mk _ isIntegral_respectsIso ?_

Result:
⊢ ∀ ⦃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], (algebraMap R T).IsIntegral → includeLeftRingHom.IsIntegral

Proof state:
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 : (algebraMap R T).IsIntegral
x✝ : S ⊗[R] T
x : S
y : T
⊢ includeLeftRingHom.IsIntegralElem (x ⊗ₜ[R] y)

Tactic:
exact IsIntegral.tmul x (h y)

Result:
no goals

Proof state:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ includeLeftRingHom.IsIntegralElem x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_

Result:
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 : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ includeLeftRingHom.IsIntegralElem 0

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 : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ ∀ (x : S) (y : T), includeLeftRingHom.IsIntegralElem (x ⊗ₜ[R] y)

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 : (algebraMap R T).IsIntegral
x : S ⊗[R] T
⊢ ∀ (x y : S ⊗[R] T),
    includeLeftRingHom.IsIntegralElem x →
      includeLeftRingHom.IsIntegralElem y → includeLeftRingHom.IsIntegralElem (x + y)