-- Mathlib/RingTheory/RingHom/Flat.lean
lemma localRingHom {f : R →+* S} (hf : f.Flat)
    (P : Ideal S) [P.IsPrime] (Q : Ideal R) [Q.IsPrime] (hQP : Q = Ideal.comap f P) :
    (Localization.localRingHom Q P f hQP).Flat

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
exact Module.Flat.trans R S (Localization.AtPrime P)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Tactic:
have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Tactic:
rw [RingHom.Flat, Module.flat_iff_of_isLocalization
  (S := (Localization.AtPrime (Ideal.comap f P))) (p := (Ideal.comap f P).primeCompl)]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
Q : Ideal R
inst✝ : Q.IsPrime
hQP : Q = Ideal.comap f P
⊢ (Localization.localRingHom Q P f hQP).Flat

Tactic:
subst hQP

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Tactic:
algebraize [f, Localization.localRingHom (Ideal.comap f P) P f rfl]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat