-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem RingEquiv.isIntegral_iff {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra T S] (φ : R ≃+* T)
    (h : (algebraMap T S).comp φ.toRingHom = algebraMap R S) (a : S) :
    IsIntegral R a ↔ IsIntegral T a

Proof state:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (algebraMap R S) ((algebraMap T R) r) * ((algebraMap R S) t * s) =
    ((algebraMap R S).comp φ.symm.toRingHom) r * ((algebraMap R S) t * s)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
⊢ IsIntegral R a ↔ IsIntegral T a

Tactic:
constructor <;> intro ha

Result:
case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
⊢ IsIntegral T a

case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
⊢ IsIntegral R a

Proof state:
case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
⊢ IsIntegral R a

Tactic:
letI : Algebra T R := φ.symm.toRingHom.toAlgebra

Result:
case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
⊢ IsIntegral R a

Proof state:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, h', mul_assoc]

Result:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
r : T
t : R
s : S
⊢ (algebraMap R S) ((algebraMap T R) r) * ((algebraMap R S) t * s) =
    ((algebraMap R S).comp φ.symm.toRingHom) r * ((algebraMap R S) t * s)

Proof state:
case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
⊢ IsIntegral T a

Tactic:
letI : Algebra R T := φ.toRingHom.toAlgebra

Result:
case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
⊢ IsIntegral T a

Proof state:
case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this✝ : Algebra R T := φ.toRingHom.toAlgebra
this : IsScalarTower R T S :=
  {
    smul_assoc := fun r t s =>
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (Eq.trans
                (Eq.trans (congrArg (fun x => x • s) (Algebra.smul_def r t))
                  (Algebra.smul_def ((algebraMap R T) r * t) s))
                (Eq.trans (congrArg (fun x => x * s) (map_mul (algebraMap T S) ((algebraMap R T) r) t))
                  (mul_assoc ((algebraMap T S) ((algebraMap R T) r)) ((algebraMap T S) t) s))))
            (Eq.trans
              (Eq.trans (congrArg (HSMul.hSMul r) (Algebra.smul_def t s)) (Algebra.smul_def r ((algebraMap T S) t * s)))
              (congrArg (fun x => x r * ((algebraMap T S) t * s)) (Eq.symm h)))))
        (Eq.refl ((algebraMap T S) ((algebraMap R T) r) * ((algebraMap T S) t * s))) }
⊢ IsIntegral T a

Tactic:
exact IsIntegral.tower_top ha

Result:
no goals

Proof state:
case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this✝ : Algebra T R := φ.symm.toRingHom.toAlgebra
this : IsScalarTower T R S :=
  {
    smul_assoc := fun r t s =>
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (Eq.trans
                (Eq.trans (congrArg (fun x => x • s) (Algebra.smul_def r t))
                  (Algebra.smul_def ((algebraMap T R) r * t) s))
                (Eq.trans (congrArg (fun x => x * s) (map_mul (algebraMap R S) ((algebraMap T R) r) t))
                  (mul_assoc ((algebraMap R S) ((algebraMap T R) r)) ((algebraMap R S) t) s))))
            (Eq.trans
              (Eq.trans (congrArg (HSMul.hSMul r) (Algebra.smul_def t s)) (Algebra.smul_def r ((algebraMap R S) t * s)))
              (congrArg (fun x => x r * ((algebraMap R S) t * s)) h'))))
        (Eq.refl ((algebraMap R S) ((algebraMap T R) r) * ((algebraMap R S) t * s))) }
⊢ IsIntegral R a

Tactic:
exact IsIntegral.tower_top ha

Result:
no goals

Proof state:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
⊢ (r • t) • s = r • t • s

Tactic:
simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]

Result:
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral R a
this : Algebra R T := φ.toRingHom.toAlgebra
r : R
t : T
s : S
⊢ (algebraMap T S) ((algebraMap R T) r) * ((algebraMap T S) t * s) =
    ((algebraMap T S).comp φ.toRingHom) r * ((algebraMap T S) t * s)