Tactic for RingHom Properties

Mathlib/RingTheory/RingHom/Flat.lean defines the property P := RingHom.Flat saying that a ring hom is flat, and proves properties about P such as P containing id, closed under comp, respects iso, and stable under base change.

I think the proofs of these are all rather standard and formulaic, e.g. the fact that flatness is stable under base change is already encoded in the theorem Module.Flat.baseChange [Flat R M] : Flat S (S ⊗[R] M).

I propose a tactic that will automate such proofs, so that the file will be able to be replaced with:

/-- A ring homomorphism `f : R →+* S` is flat if `S` is flat as an `R` module. -/
add_algebraize (mk_iff := true) RingHom.Flat Module.Flat

namespace RingHom.Flat

variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

/-- The identity of a ring is flat. -/
add_ring_hom_prop id Module.Flat.self -- generates ContainsIdentities too

/-- Composition of flat ring homomorphisms is flat. -/
add_ring_hom_prop comp Module.Flat.trans -- generates StableUnderComposition too

add_ring_hom_prop isStableUnderBaseChange Module.Flat.baseChange
add_ring_hom_prop holdsForLocalizationAway IsLocalization.flat
add_ring_hom_prop ofLocalizationSpanTarget Module.flat_of_isLocalized_span

/-- Bijective ring maps are flat. -/
@[ring_hom_prop respectsIso]
lemma of_bijective {f : R →+* S} (hf : Function.Bijective f) : Flat f := by sorry

end RingHom.Flat

Start by reading Mathlib/RingTheory/RingHom/Flat.lean and the referenced Module.Flat.baseChange theorem in Mathlib/RingTheory/Flat/Stability.lean. Study the proposed add_ring_hom_prop and add_algebraize declarations in the issue, then determine whether the listed flatness properties can be generated. Done means the repetitive proofs are replaced by the proposed declarations and the file remains valid.