If e is an application of the form f a where f is an injective function
in (← get).inj.fns, asserts f⁻¹ (f a) = a
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.Grind.mkInjEq e = pure ()
If e is an application of the form f a where f is an injective function
in (← get).inj.fns, asserts f⁻¹ (f a) = a