partial def Lean.Meta.Grind.mkEqCongrProof (lhs rhs : Expr) : GoalM Expr

partial def Lean.Meta.Grind.mkEqCongrSymmProof (lhs rhs : Expr) : GoalM Expr

@[export lean_grind_mk_eq_proof]

def Lean.Meta.Grind.mkEqProofImpl (a b : Expr) : GoalM Expr

Returns a proof that a = b. It assumes a and b are in the same equivalence class.

Equations

• One or more equations did not get rendered due to their size.

@[export lean_grind_mk_heq_proof]

def Lean.Meta.Grind.mkHEqProofImpl (a b : Expr) : GoalM Expr

Equations

• Lean.Meta.Grind.mkHEqProofImpl a b = Lean.Meta.Grind.mkEqProofCore✝ a b true