[STATEMENT]
lemma Lcm_fin_eq_Lcm [simp]:
  "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A
[PROOF STEP]
by induct simp_all