[STATEMENT]
lemma circline_set_conjugate_circline [simp]:
  shows "circline_set (conjugate_circline H) = conjugate ` circline_set H" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circline_set (conjugate_circline H) = conjugate ` circline_set H
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> circline_set (conjugate_circline H) \<Longrightarrow> x \<in> conjugate ` circline_set H
 2. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> circline_set (conjugate_circline H) \<Longrightarrow> x \<in> conjugate ` circline_set H
 2. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
assume "z \<in> ?lhs"
[PROOF STATE]
proof (state)
this:
z \<in> circline_set (conjugate_circline H)

goal (2 subgoals):
 1. \<And>x. x \<in> circline_set (conjugate_circline H) \<Longrightarrow> x \<in> conjugate ` circline_set H
 2. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
show "z \<in> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> conjugate ` circline_set H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = conjugate ?x
 2. ?x \<in> circline_set H
[PROOF STEP]
show "z = conjugate (conjugate z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = conjugate (conjugate z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z = conjugate (conjugate z)

goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
show "conjugate z \<in> circline_set H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
using \<open>z \<in> circline_set (conjugate_circline H)\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (conjugate_circline H)

goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
using conjugate_circline_set'[of "conjugate_circline H"]
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (conjugate_circline H)
conjugate ` circline_set (conjugate_circline H) \<subseteq> circline_set (conjugate_circline (conjugate_circline H))

goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
conjugate z \<in> circline_set H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> conjugate ` circline_set H

goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
assume "z \<in> circline_set H"
[PROOF STATE]
proof (state)
this:
z \<in> circline_set H

goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
thus "conjugate z \<in> circline_set (conjugate_circline H)"
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set H

goal (1 subgoal):
 1. conjugate z \<in> circline_set (conjugate_circline H)
[PROOF STEP]
using conjugate_circline_set'[of H]
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set H
conjugate ` circline_set H \<subseteq> circline_set (conjugate_circline H)

goal (1 subgoal):
 1. conjugate z \<in> circline_set (conjugate_circline H)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
conjugate z \<in> circline_set (conjugate_circline H)

goal:
No subgoals!
[PROOF STEP]
qed