[STATEMENT]
lemma gcd_mult_unit1: 
  assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
have "gcd (b * a) c dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (b * a) c dvd b
[PROOF STEP]
using assms dvd_mult_unit_iff
[PROOF STATE]
proof (prove)
using this:
is_unit a
is_unit ?b \<Longrightarrow> (?a dvd ?c * ?b) = (?a dvd ?c)

goal (1 subgoal):
 1. gcd (b * a) c dvd b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gcd (b * a) c dvd b

goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gcd (b * a) c dvd b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gcd (b * a) c dvd b

goal (1 subgoal):
 1. gcd (b * a) c = gcd b c
[PROOF STEP]
by (rule gcdI) simp_all
[PROOF STATE]
proof (state)
this:
gcd (b * a) c = gcd b c

goal:
No subgoals!
[PROOF STEP]
qed