[STATEMENT]
lemma (in category) cat_is_inverse_is_inverse_the_inverse:
  assumes "is_inverse \<CC> g f"
  shows "is_inverse \<CC> (f\<inverse>\<^sub>C\<^bsub>\<CC>\<^esub>) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inverse \<CC> (f\<inverse>\<^sub>C\<^bsub>\<CC>\<^esub>) f
[PROOF STEP]
unfolding the_inverse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inverse \<CC> (THE g. is_inverse \<CC> g f) f
[PROOF STEP]
proof(rule theI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse \<CC> ?a f
 2. \<And>x. is_inverse \<CC> x f \<Longrightarrow> x = ?a
[PROOF STEP]
fix g'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse \<CC> ?a f
 2. \<And>x. is_inverse \<CC> x f \<Longrightarrow> x = ?a
[PROOF STEP]
assume "is_inverse \<CC> g' f"
[PROOF STATE]
proof (state)
this:
is_inverse \<CC> g' f

goal (2 subgoals):
 1. is_inverse \<CC> ?a f
 2. \<And>x. is_inverse \<CC> x f \<Longrightarrow> x = ?a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_inverse \<CC> g' f
[PROOF STEP]
show "g' = g"
[PROOF STATE]
proof (prove)
using this:
is_inverse \<CC> g' f

goal (1 subgoal):
 1. g' = g
[PROOF STEP]
by (meson cat_is_inverse_eq assms)
[PROOF STATE]
proof (state)
this:
g' = g

goal (1 subgoal):
 1. is_inverse \<CC> g f
[PROOF STEP]
qed (rule assms)