[STATEMENT]
lemma (in Category) IsoCompDef:
  assumes 1: "f \<approx>> g" and 2: "ciso f" and 3: "ciso g"
  shows "(Cinv g) \<approx>> (Cinv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cinv g \<approx>> Cinv f
[PROOF STEP]
proof(rule CompDefinedI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Cinv g \<in> mor
 2. Cinv f \<in> mor
 3. cod Cinv g = dom Cinv f
[PROOF STEP]
show "Cinv g \<in> mor" and "Cinv f \<in> mor"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cinv g \<in> mor &&& Cinv f \<in> mor
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<approx>> g
ciso f
ciso g

goal (1 subgoal):
 1. Cinv g \<in> mor &&& Cinv f \<in> mor
[PROOF STEP]
by (auto simp add: InvDomCod)
[PROOF STATE]
proof (state)
this:
Cinv g \<in> mor
Cinv f \<in> mor

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
have "cod (Cinv g) = dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod Cinv g = dom g
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
ciso g

goal (1 subgoal):
 1. cod Cinv g = dom g
[PROOF STEP]
by (simp add: InvDomCod)
[PROOF STATE]
proof (state)
this:
cod Cinv g = dom g

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cod Cinv g = dom g

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
have "... = cod f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = cod f
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
f \<approx>> g

goal (1 subgoal):
 1. dom g = cod f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom g = cod f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dom g = cod f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
have "... = dom (Cinv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod f = dom Cinv f
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
ciso f

goal (1 subgoal):
 1. cod f = dom Cinv f
[PROOF STEP]
by (simp add: InvDomCod)
[PROOF STATE]
proof (state)
this:
cod f = dom Cinv f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cod Cinv g = dom Cinv f
[PROOF STEP]
show "cod (Cinv g) = dom (Cinv f)"
[PROOF STATE]
proof (prove)
using this:
cod Cinv g = dom Cinv f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cod Cinv g = dom Cinv f

goal:
No subgoals!
[PROOF STEP]
qed