-- Mathlib/RingTheory/RingHom/Flat.lean
lemma ofLocalizationPrime : OfLocalizationPrime Flat

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
⊢ Module.Flat R (Localization.AtPrime P)

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 S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Proof state:
⊢ OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] => Flat

Tactic:
introv R h

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
⊢ f.Flat

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
rw [RingHom.Flat]

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Module.Flat R S

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
⊢ f.Flat

Tactic:
algebraize_only [f]

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
exact Module.Flat.trans R (Localization.AtPrime <| Ideal.comap f P) (Localization.AtPrime P)

Result:
no goals

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (P : Ideal S) [inst : P.IsMaximal], Module.Flat R (Localization.AtPrime P)

Tactic:
intro P _

Result:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
⊢ Module.Flat R (Localization.AtPrime P)

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
replace h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) := h ..

Result:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ Module.Flat R S

Tactic:
apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P)
  (fun P ↦ Algebra.linearMap S _)

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (P : Ideal S) [inst : P.IsMaximal], Module.Flat R (Localization.AtPrime P)

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
⊢ Module.Flat R (Localization.AtPrime P)

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

Result:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
⊢ Module.Flat R (Localization.AtPrime P)