Lean4
/-- Given an expression `g.comp f` which is the composition of two `RingHom`s, this function adds
the instance `IsScalarTower A B C` to the context (if it does not already exist). -/
def addIsScalarTowerInstanceFromRingHomComp (fn : Expr) : TacticM Unit :=
withMainContext do
let (_, l) := fn.getAppFnArgs
let tower ←
mkAppOptM ``IsScalarTower
#[l[0]!, l[1]!, l[2]!, none, none, none]
-- If the instance already exists, we do not do anything
unless (← synthInstance? tower).isSome do
liftMetaTactic fun mvarid => do
let nm ← mkFreshBinderNameForTactic `scalarTowerInst
let h ←
mkFreshExprMVar
(←
mkAppM ``Eq
#[← mkAppOptM ``algebraMap #[l[0]!, l[2]!, none, none, none],
←
mkAppM ``RingHom.comp
#[← mkAppOptM ``algebraMap #[l[1]!, l[2]!, none, none, none],
← mkAppOptM ``algebraMap #[l[0]!, l[1]!, none, none, none]]])
-- Note: this could fail, but then `algebraize` will just continue, and won't add this instance
h.mvarId!.refl
let val ←
mkAppOptM ``IsScalarTower.of_algebraMap_eq' #[l[0]!, l[1]!, l[2]!, none, none, none, none, none, none, h]
let mvar ← mvarid.define nm tower val
let (_, mvar) ← mvar.intro1P
return [mvar]
