lean2/tests/lean/583.lean.expected.out
2016-06-02 11:28:00 -07:00

14 lines
397 B
Text

583.lean:31:8: error: 1 unsolved subgoal
A : Type,
B : Type,
s1 : group A,
s2 : group B,
f : A → B,
Hom : is_hom f,
a : A,
P : f a⁻¹ * f a = 1
⊢ f a⁻¹ = (f a)⁻¹
583.lean:27:8: error: failed to add declaration 'group_hom.hom_map_inv' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ A B s1 s2 f Hom a,
?M_1 …