-- Mathlib/RingTheory/RingHom/Flat.lean
lemma ofLocalizationSpanTarget : OfLocalizationSpanTarget Flat

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
refine Module.flat_of_isLocalized_span _ _ s hsp _
  (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)

Proof state:
case h.h.e'_5
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
a✝ : ↑s
⊢ OreLocalization.instModuleOfIsScalarTower = Algebra.toModule

Tactic:
ext

Result:
case h.h.e'_5.smul.h.h
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
a✝ : ↑s
x✝¹ : R
x✝ : OreLocalization (Submonoid.powers ↑a✝) S
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

Proof state:
case h.h.e'_5.smul.h.h
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
a✝ : ↑s
x✝¹ : R
x✝ : OreLocalization (Submonoid.powers ↑a✝) S
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝

Tactic:
apply Algebra.smul_def

Result:
no goals

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)

Tactic:
dsimp only [RingHom.Flat] at h

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)

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

Tactic:
introv R hsp h

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ f.Flat

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)

Tactic:
convert h

Result:
case h.h.e'_5
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
a✝ : ↑s
⊢ OreLocalization.instModuleOfIsScalarTower = Algebra.toModule

Proof state:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ f.Flat

Tactic:
algebraize_only [f]

Result:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat