Helpers to invoke functions involving algebra at tactic time

This file provides instances on x y : Q($α) such that x + y = q($x + $y).

@[implicit_reducible]

def Expr.instOne {u : Lean.Level} (α : Q(Type u)) : Q(One «$α») → One Q(«$α»)

Produce a One instance for Q($α) such that 1 : Q($α) is q(1 : $α).

@[implicit_reducible]

def Expr.instZero {u : Lean.Level} (α : Q(Type u)) : Q(Zero «$α») → Zero Q(«$α»)

Produce a Zero instance for Q($α) such that 0 : Q($α) is q(0 : $α).

@[implicit_reducible]

def Expr.instMul {u : Lean.Level} (α : Q(Type u)) : Q(Mul «$α») → Mul Q(«$α»)

Produce a Mul instance for Q($α) such that x * y : Q($α) is q($x * $y).

@[implicit_reducible]

def Expr.instAdd {u : Lean.Level} (α : Q(Type u)) : Q(Add «$α») → Add Q(«$α»)

Produce an Add instance for Q($α) such that x + y : Q($α) is q($x + $y).