Lean4
/-- Given an expression `f` of type `RingHom A B` where `A` and `B` are commutative semirings,
this function adds the instance `Algebra A B` to the context (if it does not already exist).
This function also requires the type of `f`, given by the parameter `ft`. The reason this is done
(even though `ft` can be inferred from `f`) is to avoid recomputing `ft` in the `algebraize` tactic,
as when `algebraize` calls `addAlgebraInstanceFromRingHom` it has already computed `ft`. -/
def addAlgebraInstanceFromRingHom (f ft : Expr) : TacticM Unit :=
withMainContext do
let (_, l) := ft.getAppFnArgs
let alg ←
mkAppOptM ``Algebra
#[l[0]!, l[1]!, none, none]
-- If the instance already exists, we do not do anything
unless (← synthInstance? alg).isSome do
liftMetaTactic fun mvarid => do
let nm ← mkFreshBinderNameForTactic `algInst
let mvar ← mvarid.define nm alg (← mkAppM ``RingHom.toAlgebra #[f])
let (_, mvar) ← mvar.intro1P
return [mvar]
