Commit 2025-06-19 05:50 5cdffe15

feat(Tactic/Algebraize): Allow the algebraize tactic to use lemmas which don't (directly) mention RingHom (#24661) This PR allows the algebraize tactic to be applied in more cases. Specifically, in cases where the assumption is not (directly) about RingHom, it should still be able to apply lemmas. Written at the suggestion of @chrisflav , with the following example usecase:

import Mathlib
open AlgebraicGeometry
attribute [algebraize flat_of_flat] Flat -- pretend this is added where `AlgebraicGeometry.Flat` is defined
lemma flat_of_flat {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Flat (Spec.map (CommRingCat.ofHom f))) : @Module.Flat R S _ _ f.toAlgebra.toModule := by
  have : f.Flat := sorry -- supposedly, this is true. ask christian.
  algebraize [f]
  assumption
set_option tactic.hygienic false -- allow the tactic to produce accessible names for testing
example {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Flat (Spec.map (CommRingCat.ofHom f))) : True := by
  algebraize [f]
  guard_hyp algebraizeInst : Module.Flat R S -- used to fail, succeeds now
  trivial

the key changes that makes this possible are the following:

• a different way of making lemma/type applications, creating a term which can be added to the context
• a different way of checking that the previously mentioned term actually relevant w/r/t the arguments provided to the tactic The previous check was ad-hoc and flimsy, making requirements of the precise order and the types of the arguments of lemmas or definitions, which resulted in the lemma being applicable in limited cases only. Now we still have some requirements, but these are less stringent.