Lean4
/-- Tactic that, given `RingHom`s, adds the corresponding `Algebra` and (if possible)
`IsScalarTower` instances, as well as `Algebra` corresponding to `RingHom` properties available
as hypotheses.
Example: given `f : A →+* B` and `g : B →+* C`, and `hf : f.FiniteType`, `algebraize [f, g]` will
add the instances `Algebra A B`, `Algebra B C`, and `Algebra.FiniteType A B`.
See the `algebraize` tag for instructions on what properties can be added.
The tactic also comes with a configuration option `properties`. If set to `true` (default), the
tactic searches through the local context for `RingHom` properties that can be converted to
`Algebra` properties. The macro `algebraize_only` calls
`algebraize -properties`,
so in other words it only adds `Algebra` and `IsScalarTower` instances. -/
@[tactic_parser 1000]
public meta def tacticAlgebraize__ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.tacticAlgebraize__ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "algebraize " false✝) Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional Mathlib.Tactic.algebraizeTermSeq))
